Hi Gašper,

I really like this approach. The examples make it really clear that there’s more going on than “some funny attributes”.

There’s only one thing that I find a bit weird, and that is the fact that if the check-expression-seq appeared anywhere else in the program, it would be a sequence of statements.

Did you consider:

correctness-specifier-body:
{ conditional-expression }

or:

correctness-specifier-body:
{ return conditional-expression; }

as alternatives? I feel like either of these would mean that the body of a correctness specifier would look “more like normal C++ code”.

Best regards,

                      Peter

From: SG21 <sg21-bounces_at_[hidden]> On Behalf Of Gašper Ažman via SG21
Sent: 26 September 2021 17:33
To: sg21_at_lists.isocpp.org
Cc: Gašper Ažman <gasper.azman_at_[hidden]m>; Tom Honermann <tom_at_[hidden]>; WG14/WG21 liaison mailing list <liaison_at_[hidden]>
Subject: Re: [isocpp-sg21] [wg14/wg21 liaison] Telecon to review P2388R1 Minimum Contract Support: either Ignore or Check_and_abort

EXTERNAL MAIL
First draft (lots of typos but i ran out of time today):

https://isocpp.org/files/papers/D2461R0<https://urldefense.com/v3/__https:/isocpp.org/files/papers/D2461R0__;!!EHscmS1ygiU1lA!U4UPgyU0uFfxopfpZHfWRjitcrzazbqtUgcL1g3bBKjKQr3QUtbA213gWbtvAA$>

Looking for coauthors, use-cases, and critique.

The main innovation i think it's the evaluation time split between captures and bodies of post conditions, which solves a ton of problems.


G

On Sun, Sep 26, 2021, 17:28 Caleb Sunstrum via SG21 <sg21_at_[hidden]<mailto:sg21_at_[hidden]>> wrote:
I don't have anything useful to add, other than:

I agree that this seems a better syntax space that will afford us much greater flexibility and accuracy with any future extensions to Contracts beyond the MVP, and the only downside I can see is that it's potentially difficult as a reader to discern where the function body actually begins.

That downside seems a reasonable price to pay for the improved (IMO) syntax.

/Caleb

P.S. I felt it necessary to voice my support for the proposal of the alternate syntax so that there's encouragement for a proper paper to be written to propose it :)


On Sat, Sep 25, 2021 at 6:31 AM Tom Honermann via SG21 <sg21_at_[hidden]<mailto:sg21_at_[hidden]>> wrote:
On 9/22/21 3:40 PM, Gašper Ažman via SG21 wrote:
Personally I'm not married to the current grammar, but we do need a plausible alternative, and we need it soon.

An alternative syntax needs to have:
- an obvious terminator (a comma is not that, especially for assert)
- somewhere to do the preamble (pre:, post r:, assert: )
- not be current valid syntax.

Thinking out loud here, but could braces work?

auto f(auto const x, int const y) noexcept -> void
    requires integral<decltype(x)>
    pre {
         x > 0;
         y > x;
    }
    pre(axiom) {
        {x % 2 == 0};
    }
    post(audit, new) [r=return, x, y] { // seems like lambda-like captures fit in
        {r % x == 0};
        {r % y == 0};
    }
{
/* function body */
   assert {
      { x > 0 };
   };
}

That looks pretty much like the grammar for the "requires" expression except with runtime values. Hm.....

From reading the discussion, this seems to solve some real concerns:

  * Per Ville's observation, it offers a solution for the concerns about non-const parameters.
  * It avoids the concern about the syntax looking like an attribute while not technically being one.

Additional benefits (in my opinion)

  * The syntax is reminiscent of function-try-blocks (though, since they are so rarely used, that probably has little appeal for non-enthusiasts).
  * It borrows from Concepts in a meaningful way. One could argue that
  pre { x > 0; }
is the run-time equivalent of:
  requires { requires x > 0; }
Perhaps it would be worthwhile to extend the requires clause directly to encapsulate Contract declarations; that would avoid the need for context sensitive pre and post keywords.
  * Extension points are clear and won't require new potentially context sensitive keywords to introduce new contract categories like axiom and audit.

What are the cons?

  * This is new syntax relative to what has been discussed for Contracts in the past; prior education is lost (this may be a good thing if what gets standardized deviates significantly from semantics associated in prior efforts).
  * Others?

With regard to function-try-blocks, I would expect that try would have to follow any contract declarations.

void x::f(int x)
  pre { x > 0; }
try : member(x) {}
catch (...) {}

Tom.

On Wed, Sep 22, 2021 at 5:48 PM Aaron Ballman via SG21 <sg21_at_[hidden]<mailto:sg21_at_[hidden]>> wrote:
On Wed, Sep 22, 2021 at 11:06 AM Jens Maurer via SG21
<sg21_at_[hidden]<mailto:sg21_at_[hidden]>> wrote:
>
> On 22/09/2021 12.19, Andrzej Krzemienski via Liaison wrote:
> >
> >
> > śr., 22 wrz 2021 o 09:42 Ville Voutilainen via Liaison <liaison_at_[hidden]<mailto:liaison_at_[hidden]> <mailto:liaison_at_[hidden]<mailto:liaison_at_[hidden]>>> napisał(a):
> >
> > On Wed, 22 Sept 2021 at 00:02, Jens Maurer via Liaison
> > <liaison_at_[hidden]<mailto:liaison_at_[hidden]> <mailto:liaison_at_[hidden]<mailto:liaison_at_[hidden]>>> wrote:
> > > (Personally, I think contracts should be a first-level
> > > language feature that should not be hidden inside an
> > > attribute-looking syntax atrocity. At least in C++,
> > > the space where they are does allow for context-sensitive
> > > keywords without much hassle; cf. override and final.)
> >
> > Well, yeah.. if we were to entertain a contract declaration preceding
> > the decl-specifier,
> > so that it could do forward-lookup for the parameters, then the case
> > for an attribute-like
> > syntax would be relatively strong. If the contract declaration has to
> > appear where context-sensitive
> > keywords appear, then why not use a context-sensitive keyword?
> >
> >
> > The current contracts proposal (P2388R2 <http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2021/p2388r2.html<https://urldefense.com/v3/__http:/www.open-std.org/jtc1/sc22/wg21/docs/papers/2021/p2388r2.html__;!!EHscmS1ygiU1lA!U4UPgyU0uFfxopfpZHfWRjitcrzazbqtUgcL1g3bBKjKQr3QUtbA211nUxqtPA$>>) as well as C++20 contracts offer(ed) three new annotations:
> > * preconditions and postconditions that appear in function declarations,
>
> ... in a place where we have good experience with context-sensitive
> keywords.
>
> > * an assertion that appears in the function body.
> >
> > This third kind is in the position of a regular statement inside a block scope, so a context-sensitive keyword will not work; unless we were to drop these assertions or treat them in a different, irregular way.
>
> Well, we could do
>
> pre: conditional-expression
> post identifier: conditional-expression
> assert: conditional-expression // in a block
>
> and the only potential conflict would be with a user-defined label "assert".
>
> (The colon should be a pretty good disambiguator for pre and post;
> if that's not enough, we can require a logical-or-expression and/or
> add a comma to separate contracts in declarations.)
>
> > Also a natural future extension of the currently proposed contracts is class invariants, which would also appear as a declaration in class-scope, so no room for context-sensitive keywords.
>
> With the colon, I'm not seeing a serious problem.

This sort of syntax would alleviate my personal concerns with the
proposed syntax.

In terms of whether this would be palatable to WG14, it's a bit less
clear. C has no context sensitive keywords and I have no memory of
WG14 discussions to add any, so I don't have much experience to draw
from. However, I think context sensitive keywords are a reasonable
idea worth seriously exploring as it seems at least plausible (we have
plenty of implementation and usage experience with override and final
in C++ that we can point to as prior art that's mildly C related, but
if anyone knows of a context-sensitive keyword in a C implementation,
that would strengthen the case in WG14 greatly).

~Aaron

>
> Jens
>
> _______________________________________________
> SG21 mailing list
> SG21_at_[hidden]<mailto:SG21_at_[hidden]p.org>
> Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/sg21<https://urldefense.com/v3/__https:/lists.isocpp.org/mailman/listinfo.cgi/sg21__;!!EHscmS1ygiU1lA!U4UPgyU0uFfxopfpZHfWRjitcrzazbqtUgcL1g3bBKjKQr3QUtbA210QyawOcQ$>
> Link to this post: http://lists.isocpp.org/sg21/2021/09/1212.php<https://urldefense.com/v3/__http:/lists.isocpp.org/sg21/2021/09/1212.php__;!!EHscmS1ygiU1lA!U4UPgyU0uFfxopfpZHfWRjitcrzazbqtUgcL1g3bBKjKQr3QUtbA213fUQOoMQ$>
_______________________________________________
SG21 mailing list
SG21_at_[hidden]<mailto:SG21_at_lists.isocpp.org>
Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/sg21<https://urldefense.com/v3/__https:/lists.isocpp.org/mailman/listinfo.cgi/sg21__;!!EHscmS1ygiU1lA!U4UPgyU0uFfxopfpZHfWRjitcrzazbqtUgcL1g3bBKjKQr3QUtbA210QyawOcQ$>
Link to this post: http://lists.isocpp.org/sg21/2021/09/1216.php<https://urldefense.com/v3/__http:/lists.isocpp.org/sg21/2021/09/1216.php__;!!EHscmS1ygiU1lA!U4UPgyU0uFfxopfpZHfWRjitcrzazbqtUgcL1g3bBKjKQr3QUtbA213tMLsn7w$>


_______________________________________________

SG21 mailing list

SG21_at_[hidden]<mailto:SG21_at_[hidden]>

Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/sg21<https://urldefense.com/v3/__https:/lists.isocpp.org/mailman/listinfo.cgi/sg21__;!!EHscmS1ygiU1lA!U4UPgyU0uFfxopfpZHfWRjitcrzazbqtUgcL1g3bBKjKQr3QUtbA210QyawOcQ$>

Link to this post: http://lists.isocpp.org/sg21/2021/09/1234.php<https://urldefense.com/v3/__http:/lists.isocpp.org/sg21/2021/09/1234.php__;!!EHscmS1ygiU1lA!U4UPgyU0uFfxopfpZHfWRjitcrzazbqtUgcL1g3bBKjKQr3QUtbA211WNJzi9w$>


_______________________________________________
SG21 mailing list
SG21_at_[hidden]rg<mailto:SG21_at_[hidden]>
Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/sg21<https://urldefense.com/v3/__https:/lists.isocpp.org/mailman/listinfo.cgi/sg21__;!!EHscmS1ygiU1lA!U4UPgyU0uFfxopfpZHfWRjitcrzazbqtUgcL1g3bBKjKQr3QUtbA210QyawOcQ$>
Link to this post: http://lists.isocpp.org/sg21/2021/09/1296.php<https://urldefense.com/v3/__http:/lists.isocpp.org/sg21/2021/09/1296.php__;!!EHscmS1ygiU1lA!U4UPgyU0uFfxopfpZHfWRjitcrzazbqtUgcL1g3bBKjKQr3QUtbA212Xxo8h6w$>
_______________________________________________
SG21 mailing list
SG21_at_[hidden].org<mailto:SG21_at_[hidden]>
Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/sg21<https://urldefense.com/v3/__https:/lists.isocpp.org/mailman/listinfo.cgi/sg21__;!!EHscmS1ygiU1lA!U4UPgyU0uFfxopfpZHfWRjitcrzazbqtUgcL1g3bBKjKQr3QUtbA210QyawOcQ$>
Link to this post: http://lists.isocpp.org/sg21/2021/09/1297.php<https://urldefense.com/v3/__http:/lists.isocpp.org/sg21/2021/09/1297.php__;!!EHscmS1ygiU1lA!U4UPgyU0uFfxopfpZHfWRjitcrzazbqtUgcL1g3bBKjKQr3QUtbA212DK5IaFg$>