On Wed, Sep 22, 2021 at 2:47 PM Andrzej Krzemienski via Liaison
<liaison_at_[hidden]> wrote:
> ś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.

The reason I bring it up is because of the history of how we got [[]]
in the first place. There was tons of prior art with __attribute__,
but that would "slide" the attribute to whatever construct made the
most sense based on the attribute. This turned out to have a lot of
negative qualities in practice, so [[]] was very deliberate about the
positions of attributes and what they mean. Contracts seem to play a
bit fast and loose with that positional information, and as someone
who maintains a few attribute implementations, this stuff is already
hard enough without muddying the waters further.

> 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.

If it doesn't impact the type system, I don't see why it would
appertain to the function type in any meaningful way. To me, this acts
like a declaration attribute written in the wrong location.

My recollections of the early discussion of contracts was that [[]] as
an attribute was chosen as the syntax to explore, but there was a lot
of pain coming from the fact that we wanted a declaration attribute
but they have no way to refer to the names of parameters. There was
discussion of making the contract attributes appertain to the function
type instead and to changing the semantics of function type attributes
to instead apperain to the declaration, but at some point we morphed
into the current syntax that sidesteps the issues with the workaround
to the original issue.

~Aaron

>
> 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
>
> _______________________________________________
> 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/0780.php