Date: Tue, 3 Jun 2025 23:09:03 +0300
On Tue, 3 Jun 2025 at 19:24, Tom Honermann <tom_at_[hidden]> wrote:
> I think something like the following suffices for what was proposed.
>
> double compute_sqrt(double arg) pre (arg > 0.0); inline double sqrt(double arg) { if (arg < -0.0) return std::numeric_limits<double>:: quiet_NaN(); if (arg == 0.0 /* or is +/- infinity or is a NaN*/) return arg; return compute_sqrt(arg); } double get_definite_positive_value() post(r: r >= 0.0); double f() { double d = get_definite_positive_value(); return sqrt(d); }
>
> I understand that this doesn't address (some of) what the proposer wanted since it requires that the checks to be optimized away are exposed in the TU where the call is made. However, that constraint is also present in the technical specifications of the proposal.
When does that make a program containing those pre/post run faster
than a program that doesn't contain them?
> I think something like the following suffices for what was proposed.
>
> double compute_sqrt(double arg) pre (arg > 0.0); inline double sqrt(double arg) { if (arg < -0.0) return std::numeric_limits<double>:: quiet_NaN(); if (arg == 0.0 /* or is +/- infinity or is a NaN*/) return arg; return compute_sqrt(arg); } double get_definite_positive_value() post(r: r >= 0.0); double f() { double d = get_definite_positive_value(); return sqrt(d); }
>
> I understand that this doesn't address (some of) what the proposer wanted since it requires that the checks to be optimized away are exposed in the TU where the call is made. However, that constraint is also present in the technical specifications of the proposal.
When does that make a program containing those pre/post run faster
than a program that doesn't contain them?
Received on 2025-06-03 20:09:16