Hi Everyone,
This thread has become long, spread into many fibers, and departed from the
original question. It looks like the thing being discussed now is "instead
of feature F1 solving problem P1, let's provide feature F2 solving problem
F2". But let me go back to Harald's question.

pt., 17 paź 2025 o 12:03 Harald Achitz via SG21 <sg21_at_[hidden]>
napisał(a):

>
> On the internet I saw someone saying
>
> void fun(Foo* ptr) pre (ptr!=nullpter), pre(ptr->hasData()) { ... }
>
> might be a problem (for the second pre) and should be written like this
>
> void fun(Foo* ptr) pre (ptr!=nullpter && ptr->hasData()){ ... }
>
> is that true?


When it comes to developing the contract assertions feature every little
decision along the way has been highly controversial. The same is the case
for your question.

One of the goals of the feature was to reflect and enable what is the
current programming practice. Apparently, people have developed many
different -- often incompatible with one another -- practices, but
certainly one of them is to decompose the property that you are asserting
into the tiniest possible bits, as in:

```
BOOST_REQUIRE(tool.isConfigured());
BOOST_REQUIRE(tool.configuration().hasCoordinates());
BOOST_REQUIRE(matches(tool.configuration().coordinates(), refCoords));
```

The reason to do that is that if it -- God forbid -- reports a violation, I
immediately get high-quality information as to *which part* of the
assertion was violated: this reduces the time of looking for and
eliminating the bug. In a way this is part of the "shift left" movement.

I could certainly squeeze them all into a one big "wide-contract"
predicate, but this would complicate the bug detection and removal process.
The current tools, such as `BOOST_REQUIRE` from the Boost.Test library
here, or the good old C-style `assert()` do enable this technique: this is
because they *do not* have an equivalent of the "observe" semantic.

If the contract assertions that we are about to deliver do not allow me to
express my contracts in this decomposed way, it would be a regression for
people employing the above practice. Even if it came with an advice, "have
all your contract predicates have a wide contract", because the above
pattern is so prevalent, people would be using it anyway, even if
unconsciously. But I think that P2900 as proposed *does* enable this "tiny
predicates" practice. I strongly object to giving the advice "make all your
contract predicates wide". The advice I will be giving and following
instead is this:

For people annotating their interface with contract assertions:

1. Decompose your contract into tiniest possible bits, and represent each
one with a separate assertion, but order them so that assertion A which
protects the assertion B comes before A.

For people who assemble the entire program and decide which evaluation
semantic is used and where -- which are likely a different group of people
-- the advice depends on your experience level:

1. For the beginners: do not use the "observe" semantic.
2. For experienced programmers: still do not use the "observe" semantic.
3. For John Lakos: do what you think is best for your product, bearing in
mind that people decompose their assertions like indicated above.

It should be noted, though, that the "observe" semantic is more bug-prone
than how it is advertised by its proponents. The statement that "the
`observe` semantic exposing UB in contract assertions is no worse than UB
that the protected function most probably already has in its body" is
correct only because it is using an ambiguous qualifier "most probably". In
general, and according to the model, there is no requirement or expectation
that the predicate exposed in the precondition assertion is also exploited
in the function body. The goal of a precondition, in the most general case,
is to make sure that the postcondition of the function is satisfied. Paper
wg21.link/P3582 gives an example of such a case. The paper also proposes an
alternate meaning of mode "observe" devoid of the potential "new UB"
problem.

We also know that there are programs, not that rare, that have been
battle-tested in production for years that work according to specification,
even though they are composed of components that don't work according to
their specification. Starting declaring and observing contract assertions
in those cases may introduce new paths that have never been there. Imagine
this case:

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

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.

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, but there come situations
where it is the only thing that can save the day. Note that P2900, or CD,
never mandates the existence of a global compiler option "observe". It
recommends that there is a global option "enforce" by default, and that
there is the ability to switch to mode "ignore". Compiler authors can
choose to offer the third translation mode with a descriptive name, such as
"unsafe-observe".

Regards,
&rzej;