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: Andrzej Krzemienski <akrzemi1_at_[hidden]>
Date: Wed, 22 Sep 2021 20:47:50 +0200
śr., 22 wrz 2021 o 20:27 Aaron Ballman <aaron_at_[hidden]> napisał(a):

> On Wed, Sep 22, 2021 at 2:07 PM Andrzej Krzemienski via Liaison
> <liaison_at_[hidden]> wrote:
> > śr., 22 wrz 2021 o 17:29 Peter Brett via Liaison <
> liaison_at_[hidden]> napisał(a):
> >>
> >> > -----Original Message-----
> >> > From: SG21 <sg21-bounces_at_[hidden]> On Behalf Of Jens Maurer
> via SG21
> >> > Sent: 22 September 2021 16:06
> >> > To: liaison_at_[hidden]
> >> > Minimum Contract Support: either Ignore or Check_and_abort
> >> >
> >> > On 22/09/2021 12.19, Andrzej Krzemienski via Liaison wrote:
> >> >
> >> > > The current contracts proposal (P2388R2
> >> > <https://urldefense.com/v3/__http://www.open-
> >> >
> std.org/jtc1/sc22/wg21/docs/papers/2021/p2388r2.html__;!!EHscmS1ygiU1lA!RvxF
> >> > HnEDatbou6x94lL_6CSCp42OlaEaFUXvIXw8V0M2VJfLBbtJ1bN6rL59lA$ >) 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.
> >>
> >> I like this approach *a lot*. It makes sure that the contract is very
> clearly
> >> not an attribute, even to the casual reader, and it is more evident
> that the
> >> contract is an important part of the function's interface.
> >>
> >> I've had more than one person say to me, "Oh, attributes aren't
> important when
> >> I just want to know how to call a function and I like the '[[...]]'
> because it
> >> makes it easy for me to skip over them when reading." So, I think
> there's
> >> value in contracts that don't look like attributes.
> >>
> >> I wonder where I can find a compiler expert who knows how to hack this
> >> alternative contract syntax into a compiler's frontend...
> >
> >
> > Ok, so I hear now a second concern about the [[pre: x]] syntax.
> >
> > The first one was that a compiler that incorrectly treats everything
> inside [[...]] as an attribute can omit the parsing of the contract
> annotation.
> >
> > The second concern here is that we send the wrong message to the
> programmer: that function contracts are not important, because things in
> [[]] are unimportant in terms of correctness.
> >
> > Is that a fair summary?
>
> There's a third concern in the same vicinity related to the use of
> [[]]. We've spent a decade teaching programmers that the positional
> placement of [[]] matters as to how it is interpreted by the compiler.
>
> void func(int i) [[attr]]; // attribute appertains to the function type
> void func(int i) [[contract:]]; // no impression that this impacts the
> type, but not certain either
>
> So if contracts don't behave like type attributes (which the standard
> doesn't currently make use of), it negates a lot of the educational
> effort on how to properly use attributes. Even though the standard
> doesn't use type attributes, users can use them with vendor specific
> attributes. For example, function type attributes are known to impact
> things like type checking; e.g., https://godbolt.org/z/3YzGb897f


Thank you. This is new information to me.
Although, I must say that this third concern looks least concerning to me.
To the extent that I understand the term "appertains to function type", I
would say
that the list of preconditions and postconditions do appertain to function
type.
They do not affect the type: I mean the mangling, and the fact that you can
cast a function with preconditions to a function pointer without
preconditions, but "conceptually" it affects the type:

int f(int i) [[pre: i != 0]];

Function f is not just any function int->int, but it is one of those that
do not take 0 as the correct input.

Regards,
&rzej;



>
> ~Aaron
>
>
> >
> > Personally, I think that `noreturn` in declaration:
> >
> > [[noreturn]] int f(int i);
> >
> > Also expresses the function's contract, and is important, because it
> affects what usages of the function are correct or not. Even if the
> compiler "ignores" it.
> >
> > Regards,
> > &rzej;
> >
> >>
> >> Peter
> >>
> >> _______________________________________________
> >> Liaison mailing list
> >> Liaison_at_[hidden]
> >> Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/liaison
> >> Link to this post: http://lists.isocpp.org/liaison/2021/09/0768.php
> >
> > _______________________________________________
> > Liaison mailing list
> > Liaison_at_[hidden]
> > Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/liaison
> > Link to this post: http://lists.isocpp.org/liaison/2021/09/0774.php
>

Received on 2021-09-22 13:48:16