On Mon, 20 Sept 2021 at 17:36, John Spicer via SG21
<sg21_at_[hidden]> wrote:
>
> The contracts syntax is intentionally “attribute-like” but “not actually an attribute”, which allows a compiler to treat those differently.
>
> But the syntax difference is very subtle and a different that a compiler that does not support attributes would be unlikely to check for.
>
> As an example:
>
> [[something x]]
> [[something(x)]]
>
> The first is an invalid attribute but we could potentially decide to make it a contract, while the second is a valid attribute.
>
> So, C++ is saying that the syntax of the stuff inside “[[ ]]” matters in the contract vs. attribute decision.
>
> I believe that is intentional so that older C++ compilers that support attribute but not contracts will probably ignore them.
>
> I think that also means that unless a C compiler does syntax checking on unrecognized attributes, there should not be an issue.

But the whole point of choosing an attribute-like but
not-exactly-attribute syntax is to have the contract declaration
be ill-formed if the compiler doesn't understand it. The contract
declaration refers to language constructs declared
in the program, and it's desirable to have the compiler syntax-check
them even if they're not evaluated by the
program. The rationale for that is that if checking is enabled, the
contracts are well-formed, but also that even
if checking is disabled, the contracts are still well-formed to have
any hope for other tools being able to make any
sense of them. Consider

[[pre: greater_than_zero(x)]] // you must have a convertible_to_bool
greater_than(convertible_from_int) function in your program
void f(int x);

[[precondition,the,value,of,x,is,greater,than,zero]] // no particular
requirement that you have anything in your program
void f(int x);

Yes, the second example is rather concocted. But its purpose is to
illustrate what we could get if we go for
an attribute syntax that the compiler can happily ignore. Now we have
a contracty declaration that is no contract
at all, and a static checking tool has no chance of knowing that it is
a contract declaration. A compiler could
balanced-token ignore it and fail to tell the programmer that what was
intended to be a contract declaration
is no such thing.

Perhaps we should explain this better in our Contracts proposal, in
its rationale part. :)