Re: {Pre,Post}conditions and side effects

[Bob Duff <bobduff@theworld.com>]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> I can see that are some cases where the properties are too expensive to 
> verify at runtime. It would be nice if there was a way to turn off those 
> (AND ONLY THOSE) properties. But Ada doesn't have that sort of granularity, 

Sure it does.  If Is_Sorted is too slow for production use, you can say:

    ... with Predicate => (if Slow_Mode then Is_Sorted(...))

and set the Slow_Mode flag to True for testing.  Also set it to True
when running proof tools.

Alternatively, you can say something like:

    function Sort(X: My_Array) return My_Array with
        Post => (if X'Length <= 20 then Is_Sorted(Sort'Result));

Now calls to Sort can be O(log N) instead of O(N).  And if Sort doesn't
do anything special for arrays longer than 20, the postcondition is
likely to catch any bugs in Sort.

> Correct. If it hurts, don't write that. :-) I don't begin to believe that 
> all program properties can be proved.

Yes, that's obviously true.  Here's a property of GNAT:

    Compared to most compilers (for any language), GNAT usually gives
    better error messages.

Anybody who has used GNAT and a lot of other compilers knows that
property is true.  But nobody can prove it in a mathematical sense,
because there's no way to formalize it.

- Bob