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.

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.

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