C++ Logo

liaison

Advanced search

Re: [wg14/wg21 liaison] [isocpp-sg21] Telecon to review P2388R1 Minimum Contract Support: either Ignore or Check_and_abort

From: Gašper Ažman <gasper.azman_at_[hidden]>
Date: Sun, 26 Sep 2021 17:32:57 +0100
First draft (lots of typos but i ran out of time today):

https://isocpp.org/files/papers/D2461R0

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]>
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]> 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]> wrote:
>>
>>> On Wed, Sep 22, 2021 at 11:06 AM Jens Maurer via SG21
>>> <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]>> napisał(a):
>>> > >
>>> > > On Wed, 22 Sept 2021 at 00:02, Jens Maurer via Liaison
>>> > > <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>)
>>> 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]
>>> > Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/sg21
>>> > Link to this post: http://lists.isocpp.org/sg21/2021/09/1212.php
>>> _______________________________________________
>>> SG21 mailing list
>>> SG21_at_[hidden]
>>> Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/sg21
>>> Link to this post: http://lists.isocpp.org/sg21/2021/09/1216.php
>>>
>>
>> _______________________________________________
>> SG21 mailing listSG21_at_[hidden]
>> Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/sg21
>> Link to this post: http://lists.isocpp.org/sg21/2021/09/1234.php
>>
>>
>> _______________________________________________
>> SG21 mailing list
>> SG21_at_[hidden]
>> Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/sg21
>> Link to this post: http://lists.isocpp.org/sg21/2021/09/1296.php
>>
> _______________________________________________
> SG21 mailing list
> SG21_at_[hidden]
> Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/sg21
> Link to this post: http://lists.isocpp.org/sg21/2021/09/1297.php
>

Received on 2021-09-26 11:33:10