Re: {Pre,Post}conditions and side effects

["Randy Brukardt" <randy@rrsoftware.com>]

<Stefan.Lucks@uni-weimar.de> wrote in message 
news:alpine.DEB.2.11.1505071103310.14859@debian...
...
>> I don't believe that checks in Ada (of any kind) should ever be turned 
>> off.
>
>Here, I heavily disagree. Often, checking relevant properties is much to
>expensive to perform the checks them in production code.
>
>A simple example is binary search over a sorted array. The precondition
>requires the array to be sorted. If the compiler succeeds in optimising
>the test away, it is equivalent to a static program verifier proving the
>precondition holds when the binary search is called.

Exactly! That's the entire idea; the compiler *should* be doing these 
optimizations, indeed one major branch of static program verification comes 
from enhancing compiler optimizer technology (CodePeer is an example of 
that). I think that technology should simply have stayed in the compiler.

>If the compiler fails to optimise the check away, the execution time goes 
>up
>from logarithmic to linear. If you can live with that, you don't need 
>binary search!

If the compiler fails to optimize the check away, your program is wrong in 
some sense, and you should have gotten an error or warning (depending on the 
compiler mode and exception contracts) to that effect. You ought to fix your 
program (probably by adding an appropriate predicate) so that the check 
*can* be eliminated (or pushed to somewhere where the cost is irrelevant).

>Turning off the checks just hides the problem. There is no value to that, 
>IMHO.
>The semantic of a plain precondition is essentially:
>
>   * If I a True, the postcondition will hold.
>     Never call the subprogram if I am false!!!
>     Otherwise, the subprogram might do anything.

"anything" => erroneous.

>This is a precondition in the "Design by Contract" sense.

Ada 2012 does not have these sorts of preconditions. (We've discussed it 
numerous times.) The theory is that adding a precondition NEVER makes a 
program less safe. Ergo, preconditions can be ignored, but violating an 
ignored precondition is not erroneous in the sense that violating a 
suppressed check is. There's a reason that we didn't call this "suppressing" 
preconditions! Thus, there is no circumstance where the "subprogram might do 
anything".

I've thought a bit about having some additional Assertion_Policy "suppress" 
that would allow the semantics you describe above, but we haven't talked 
about that at the language level.

> A typical example for this would be "the array is sorted" when calling
> binary search. If you call a binary search routine with an unsorted array,
> you will likely get false results. And you deserve the blame!

That's not "anything". That's a well-defined (but useless) result. Be 
careful about your terminology!

> The semantic of a precondition with something like "else raise
> This_Exception" is
>
>   * If I am True, the postcondition will hold
>     when the subprogram terminates.
>     If I am False, the subprogram will not do anything,
>     except for raising This_Exception.

This the meaning of all Ada 2012 preconditions. "This_Exception" just 
defaults to "Assertion_Error".

Anyway, the Assertion_Policy can be changed locally, and the policy in 
effect at the point of the declaration determines what policy is used for 
calls. Plus the policy can be set separately for different kinds of 
assertions. Thus, you can get the effect you want with the existing 
policies, so long as you don't try to write two different kinds of 
assertions on the same subprogram.

Note that there is some debate about the value of the fine-grained policy 
setting, it's unclear that GNAT implements it correctly. If some of their 
customers showed concern about the correct implementation of those rules, 
that certainly would change.

                                        Randy.