Date: Fri, 17 Oct 2025 21:15:04 +0300
On Fri, 17 Oct 2025 at 14:02, JOSE DANIEL GARCIA SANCHEZ
<josedaniel.garcia_at_[hidden]> wrote:
>
> Yes.
>
> That is a particular case of NB comment ES-047
>
> Here is a non-pointer example:
>
> double f(double x, double y)
> pre(y!=0)
> pre(x/y > 0);
>
> Or
>
> double g(double x)
> pre(x>0)
> pre(std::sqrt(x) < 100.0);
>
> The logical conjunction of preconditions might be a solution for 2 pre-conditions. But as the number of preconditions increases that solution is increasingly bad.
>
> Consider:
>
> template <typename T, typename Q, typename R>
> double h(T * pt, Q * pq, R * pr)
> pre(pt != nullptr)
> pre(pr != nullptr)
> pre(pr != nullptr)
> pre(*pt + *pq + *pr > 0);
>
> versus
>
> template <typename T, typename Q, typename R>
> double h(T * pt, Q * pq, R * pr)
> pre(pt != nullptr && pr != nullptr && pr != nullptr && *pt + *pq + *pr > 0);
>
> The conjucted form is worse both from the teachability point of view and the maintainabilit point of view. However the first option leads today to UB.
The conjunct form also doesn't do the same thing as the
non-conjunct-form-evaluated-with-enforce.
<josedaniel.garcia_at_[hidden]> wrote:
>
> Yes.
>
> That is a particular case of NB comment ES-047
>
> Here is a non-pointer example:
>
> double f(double x, double y)
> pre(y!=0)
> pre(x/y > 0);
>
> Or
>
> double g(double x)
> pre(x>0)
> pre(std::sqrt(x) < 100.0);
>
> The logical conjunction of preconditions might be a solution for 2 pre-conditions. But as the number of preconditions increases that solution is increasingly bad.
>
> Consider:
>
> template <typename T, typename Q, typename R>
> double h(T * pt, Q * pq, R * pr)
> pre(pt != nullptr)
> pre(pr != nullptr)
> pre(pr != nullptr)
> pre(*pt + *pq + *pr > 0);
>
> versus
>
> template <typename T, typename Q, typename R>
> double h(T * pt, Q * pq, R * pr)
> pre(pt != nullptr && pr != nullptr && pr != nullptr && *pt + *pq + *pr > 0);
>
> The conjucted form is worse both from the teachability point of view and the maintainabilit point of view. However the first option leads today to UB.
The conjunct form also doesn't do the same thing as the
non-conjunct-form-evaluated-with-enforce.
Received on 2025-10-17 18:15:19
