On Sun, Oct 19, 2025 at 5:44 PM Andrzej Krzemienski <akrzemi1_at_[hidden]>
wrote:

> 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:
>>
>>>
>>> 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.
>

But as long as you take into account that it is possible, and code
appropriately, you will never be bitten if it does happen.

The problem only happens if you assume that either your predicate won't
ever be called (ignore), or if it is called, then all previous predicates
in the function passed (enforce or quick_enforce), and assume that no one
accidentally reorders your assertions (which can be hard to detect if they
are opaque). So the problem only happens if you assume that `observe`
doesn't exist.


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

It does as long as you don't violate the preconditions of your tests when
your tests are performed in isolation.

I don't think it's reasonable to deny the ability for anyone to use this
`observe` because it is possible to use it incorrectly. Especially when it
is fairly straightforward to say "don't violate preconditions inside the
predicate".


>
>> 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,
>

It more than likely doesn't now, but I didn't want to say for sure that it
doesn't now, but suspected that it didn't.

Assuming it doesn't, then it could maybe be made to. I don't know what the
cost would be though. This was mostly forward-looking at possible future
solutions to make it easier to write your original predicates.

Again, if you write your predicates that they don't internally have any
precondition violations in isolation, then you don't have to worry about
previous predicates not terminating.


> 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()`.
>

As long as the precondition is visible, and thus can be called caller-side
with the selected semantic, then that's okay. Again, this is forward
looking so likely not for the current conditions.


> 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);
> ```
>

For "this would not cover", are you talking about automatic handling of
violating the precondition in the predicate itself? Just want to be sure.

What is `array`? I'm assuming it's a class member or global, and that
`size()` knows how to compute that size. The precondition of `*p` is `p`,
the precondition of array access is that it's in bounds. If `array` is
something that can have its own preconditions (vector, array), then great.
If not, such as a native array, then language preconditions, which have
been discussed recently, come into play. If none of those are true, and
the precondition can't be on the array access itself, then you do need to
test it as part of the predicate.

I would say that this is a case where you should write the test once with
decomposed tests and then reuse it, especially if you want both contract
checking and input validation.

```
inline bool canAccessArrayWith(int *p)
  pre(p)
  pre(p && *p >= 0)
  pre(p && *p < size(array))
{
  return p && *p >= 0 && *p < size(array)
}

void f(int *p) pre(canAccessArrayWith(p) && array[*p] > 0)
{
  if(!canAccessArrayWith(p)) {
    throw something;
  }
  if (not (array[*p] > 0)) {
    throw something;
  }
  do stuff here
}
```