C++ Logo

liaison

Advanced search

Re: [wg14/wg21 liaison] P2961R1 syntax for Contracts: viable for C?

From: Timur Doumler <cpp_at_[hidden]>
Date: Fri, 6 Oct 2023 16:22:06 +0300
Hi everyone,

Thanks again for all your feedback on this thread, this is immensely helpful input.

So far, the discussion has exclusively focused on `pre` and `post`, which are part of a function declaration, but we also have a third type of contract, `assert` which is a statement or expression inside a function body.

The P2935 (attribute-like) syntax spells them as follows,

void f() {
  int i = get_i();
  [[ assert: i >= 0 ]]; // this is a contract assert
  // ...
}

The P2961 syntax would really, really like to spell them as follows:

void f() {
  int i = get_i();
  assert (i >= 0); // this is a contract assert
  // ...
}

But of course we can't use `assert` because that already has a meaning today (the `assert` macro from "assert.h") and that meaning cannot be made incompatible with contract asserts. In particular, macro assert is token-ignored if NDEBUG is defined, whereas contact asserts are never, and can never be, token-ignored – you can switch the contract semantic to "unchecked" so that the expression is not evaluated at runtime, but it still needs to be parsed – and therefore it still needs to be correct code, and so existing code like this can never work with Contracts:

#ifndef NDEBUG
  DebugThingy dbg;
#endif

void f() {
  assert(dbg.checkSomething()); // OK with macro, syntax error with contract if NDEBUG not defined
  // ...
}

Long story short, we decided that if we want to adopt the P2961 syntax, we cannot use the keyword "assert" because we cannot replace the existing assert macro by Contracts due to the differences in semantics and the resulting code breakage. So we grudgingly realised that if we decide to go down the P2961 route, we need to pick a different keyword which is not "assert". Two candidate keywords are currently under discussion:

 contract_assert
 
and

  assertexpr

Does any of this raise any concerns with C? If we want a Contracts facility in C compatible with C++, we need to deal with assertions as well, not just pre and post. Does this change anyone's opinion on whether you'd prefer the C++ committee to adopt the P2935 (attribute-like) syntax or the P2961 syntax?

Cheers,
Timur

> On 5 Oct 2023, at 18:09, Aaron Ballman <aaron_at_[hidden]> wrote:
>
> On Thu, Oct 5, 2023 at 7:58 AM Timur Doumler via Liaison
> <liaison_at_[hidden] <mailto:liaison_at_[hidden]>> wrote:
>>
>> Hello SG22,
>>
>> In SG21 (Contracts), we have been discussing the syntax for preconditions, postconditions, and assertions which will be part of the new Contracts facility we're designing for C++26. We currently have two syntax proposals on the table – we have not yet decided which one we prefer.
>>
>> One is the attribute-like syntax which you might have already seen (see P2935R3). With this syntax, a function declaration with a precondition and a postcondition looks like this:
>>
>> int f(int i)
>> [[ pre: i >= 0 ]]
>> [[ post r: r > i ]];
>>
>> The other is a newer proposal that seeks to eliminate the various issues with attribute-like syntax we discovered (see P2961R1, which I am co-authoring together with Jens Maurer, in Cc). The P2961R1 syntax looks like this:
>>
>> void f(int i)
>> pre (i >= 0)
>> post (r: r > i);
>>
>> At the last SG21 telecon, the question has been raised whether the P2961R1 syntax would be compatible with C, in case C wishes to standardise a Contracts facility consistent with the C++ one. As the main paper author of P2961R1, I was directed to ask WG14 about their opinion and report back to SG21.
>>
>> However, I have been informed by Ville (in Cc) that WG14 is currently doing a ballot, that the WG14 Convener is adamant about having as little as possible technical discussion during a ballot, and that discussing a future proposal on the WG14 reflector would therefore be inappropriate at this time.
>>
>> So, if you don't mind, I'm going to try my luck with SG22 instead. Do any of you folks have any desire to standardise Contracts for C, to have a syntax for this that looks like the C++ one, and do you have any technical concerns about the syntax proposed in P2961R1?
>>
>> Any and all feedback would be greatly appreciated.
>
> Thank you for reaching out!
>
> I am personally *very* motivated to see Contracts get into C; I think
> the functionality is incredibly important for a whole host of reasons
> that I probably don't need to convince you of. :-D I really appreciate
> all efforts to come up with syntax & semantics that can work for both
> C and C++ because I would love to get to a day where the OS headers
> and C standard library headers can provide contracts that the STL can
> take advantage of as well. Getting as much of the source code stack to
> support contracts as possible seems like a good goal to strive for.
>
> The syntax that looks like `[[ pre: expr ]]` is a problem in C
> currently. [[ always introduces an attribute specifier list currently,
> and we have an allowance for implementations to eat balanced tokens
> between the double square brackets. While it may be possible to change
> this rule, it should be noted that the rule was introduced at the
> request of several implementers of C and the decision was recently
> reaffirmed by the committee during NB comment resolution for C23, so I
> would expect that to be contentious. IMO, even in C++ only, claiming
> that it's not an attribute because of the presence of a single colon
> is not compelling rationale to me -- users already understand that
> anything between [[]] is an attribute and trying to change that to be
> "could be an attribute or it could be something entirely different
> from attributes" is going to be confusing and cause problems in
> practice.
>
> The syntax that looks like `pre (i >= 0)` is slightly problematic in C
> in that it's using an unreserved identifier. However, I think that's
> pretty easy to work around by introducing it as `_Pre` in C and
> providing something like a `<stdcontracts.h>` with a macro so you can
> get the `pre` spelling in header code shared between C and C++. Then,
> 10+ years later, we can deprecate the ugly reserved keyword in C use
> and start using the prettier keyword. (We did this in C23 with
> numerous earlier-C keywords like `_Bool`, `_Alignas`, `_Thread_local`,
> etc.) C doesn't really have the notion of conditional keywords, so I
> don't think that will be an option for us (especially because we'd
> still have to worry about macros named `pre`:
> https://sourcegraph.com/search?q=context:global+%28%23define+pre%29%5B+%5Ct%5D%2B&patternType=regexp&case=yes&sm=1&groupBy=repo
> and https://sourcegraph.com/search?q=context:global+%28%23define+post%29%5B+%5Ct%5D%2B&patternType=regexp&case=yes&sm=1&groupBy=repo
> show there are such uses in the wild).
>
> Because contracts are not intended to be an optional feature an
> implementation can support at its discretion, I greatly prefer the
> syntactic direction from P2961R1 over the syntax from P2935R3. Even in
> C++, I think it's a superior way to surface the functionality because
> it doesn't attempt to redefine existing syntax for new,
> similar-but-not-actually-the-same kinds of functionality.
>
> ~Aaron
>
>>
>> Thanks,
>> Timur
>> _______________________________________________
>> Liaison mailing list
>> Liaison_at_[hidden] <mailto:Liaison_at_[hidden]>
>> Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/liaison
>> Searchable archives: http://lists.isocpp.org/liaison/2023/10/index.php


Received on 2023-10-06 13:22:09