niedz., 19 paź 2025 o 23:01 Greg Marr <gregm_at_[hidden]> napisał(a):

> On Sun, Oct 19, 2025 at 10:47 AM Andrzej Krzemienski via SG21 <
> sg21_at_[hidden]> wrote:
>
>> For people annotating their interface with contract assertions:
>>
>> 1. Decompose your contract into tiniest possible bits, and represent each
>> one with a separate assertion
>>
>
> That's good advice.
>
>
>> , but order them so that assertion A which protects the assertion B comes
>> before A.
>>
>
> FYI, the A at the end should be B.
>
> However, that's bad advice currently, because assertions don't by
> themselves "protect" anything, especially if they are ignored, which can
> happen on an assertion-by-assertion basis according to the current state of
> the CD.
>
> Remember that contract assertions are supposed to be ghost code. Don't
> assume that any particular assertion has protected you from anything, as it
> may have been ignored or observed. They are only "protection" if you are
> using a terminating semantic, and thus you are only "protected" because
> your code is not even executed because the process has terminated.
>
> I would propose this updated guidance:
>
> 1. Decompose your contract into the tiniest possible bits, and represent
> each one with a separate assertion.
> 2. Order your decomposed preconditions so that if assertion A is also a
> precondition of assertion B, then A by itself comes before B, so that A is
> reported by itself first if reporting is enabled.
> 3. If testing precondition B itself has preconditions, test those
> preconditions first in the same assertion expression so your test of B
> doesn't violate its own preconditions.
>
> ```void utilize(Tool& tool)
>>
> pre (tool.isConfigured())
>> pre (tool.configuration().hasCoordinates()
>> pre (matches(tool.configuration().coordinates(), refCoords))
>> {
>> if (not tool.isConfigured())
>> throw StopServerTransaction();
>> if (not tool.configuration().hasCoordinates())
>> throw StopServerTransaction();
>> if (not matches(tool.configuration().coordinates(), refCoords))
>> throw StopServerTransaction();
>>
>> // now do the work ...
>> }
>> ```
>>
>
> Following the guidance above, make the assertions match the actual flow of
> the function, where `tool.configuration().hasCoordinates()` is never
> checked if `tool.isConfigured()` is not true, don't eliminate the implicit
> short circuits represented by the throw statements:
>
> ```
> void utilize(Tool& tool)
> pre (tool.isConfigured())
> pre (tool.isConfigured() && tool.configuration().hasCoordinates()
> pre (tool.isConfigured() && tool.configuration().hasCoordinates() &&
> matches(tool.configuration().coordinates(), refCoords))
> ```
>
> This has the same effect as the `BOOST_REQUIRE` before, but you can't
> blindly replace `BOOST_REQUIRE` with `pre` because the semantics of the two
> are different.
>

Indeed, you are correct. But...


>
> The body of this function has no UB and protects nicely against bad input.
>> Contract assertions don't break that as long as they are ignored or
>> enforced, but *a new* UB is introduced when assertions are observed.
>>
>
> Only if your contract assertions themselves don't protect nicely against
> bad input, and instead improperly rely on something else to have protected
> them, even though that something else that they are relying on for
> protection is explicitly NOT guaranteed to protect them. If your
> assertions also protect nicely against bad input, then there will be no UB.
>
>
>> But again, this does not sound as a grave problem once one starts to
>> think about the global mode "observe" as a thing as dangerous as
>> reinterpret_cast: we all know we should avoid it,
>>
>
> It can also happen if the semantic of the first `pre` is `ignore` and the
> semantic of the second `pre` is `enforce`, which is explicitly allowed by
> the current state. So it's not a problem with `observe` per se, but rather
> a problem with assuming that the preconditions of your assertion haven't
> been violated just because there was another `pre` on the same function
> that tested them.
>

Again, you are technically correct, but while this is allowed to happen, I
am sufficiently confident that the compiler would never do that: apply
different semantics to different assertions in the same "sequence" as long
as there are no labels or attributes present in either.

>
> I agree that having to repeat the preconditions isn't ideal, so a nice
> post-C++26 expansion would be to allow assertion chaining.
>

I would take a different path, and demand of the CD that the decomposition
into smaller predicates should just work by default.


> For example, a label could be used to group assertions such that violation
> of a single assertion in that group should be considered as an immediate
> violation of all subsequent assertions in the same group without having to
> test them, and that stops evaluation for that group. Reporting could be
> done for each in observe mode, or it could just skip the rest.
>
> While writing this, I thought of another possibility, and I wonder if it's
> already the case. If `Tool::configuration()` has a precondition of
> `isConfigured()`, then does the assertion expression
> `tool.configuration().hasCoordinates()` fail as soon as
> `tool.configuration()` is called if caller-side checking is enabled, and
> thus `.hasCoordinates()` is never called, even with the `observe`
> semantic? I don't remember seeing anything that would do that. That might
> be another way to deal with this.
>

Calling preconditions on functions called in the predicate nests much like
the funcion calls nest, so if all TUs were compiled with the same ignore or
enforce semantic, this would work as you expect. This would *not* work when
`observe` comes into play, and also, as you mentioned, where semantics are
mixed. And in this case they would more likely mix, as the "precondition on
precondition" (isConfigured()) may be compiled in a different TU then the
precondition `tool.configuration().hasCoordinates()`.

Also, this would not cover similar cases where built-in operations are used:

```
void f(int*p)
  pre (p)
  pre (*p >= 0)
  pre (*p < size(array))
  pre (array[*p] > 0);
```

Regards,
&rzej;