On Thu, 5 Jun 2025 at 02:15, Tom Honermann <tom@honermann.net> wrote:

Relying on a hypothetical assume semantic doesn't help, especially
because using that makes it not the same program, the compiled-altered
program
has different semantics.

The semantics are only different, discounting side effects of contract
predicate evaluation, if an assume semantic is violated.

Which itself means that the semantics are different. They are
different in exactly the same way
as

switch (foo) {
case 1: bar1();break;
case 2: bar2(); break;
case 3: bar3(); break;
default: std::unreachable();
}
code_that_follows();

and

switch (foo) {
case 1: bar1();break;
case 2: bar2(); break;
case 3: bar3(); break;
}
code_that_follows();

are different.

And then, when there is a contract annotation that doesn't change the
well-defined/undefined behavior sets of a program, and an annotation
that does,
they *should* be different, in source code.

Thank you very much for this discussion. It crystallized the above.

You are welcome, but I don't think we've reached a conclusion here.

The semantic difference you describe seems just as applicable to the ignore and observe contract semantics with the std::unreachable() portion corresponding to code that is only reached when a contract is violated. SG21 discussions occasionally considered requiring a "continuable" annotation for the observe semantic, but it never got much support because the ignore semantic exists. Do you believe we should require an in-source annotation for the observe semantic?

I view contract semantics as a choose-your-own-adventure-story for the behavior of contract violations:

• quick-enforce: always well-defined, program terminates.
• enforce: always well-defined, program terminates unless the violation handler throws, calls longjmp(), etc...
• observe: library UB (which may lead to core language UB) unless the violation handler throws, calls longjmp(), etc...
• ignore: library UB (which may lead to core language UB).
• assume: always core language UB.
  

Tom.