Re: {Pre,Post}conditions and side effects

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

"Bob Duff" <bobduff@theworld.com> wrote in message 
news:87egml511m.fsf@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.

Of course. That's essentially what I've ("we've", really, Isaac created a 
lot of the tracing stuff in Janus/Ada) been doing for years. I just hadn't 
thought of trying to use it directly in the assertions. We'd use a function 
call, though, rather than a constant:

    ... with Dynamic_Predicate => (if JTrace.Trace(Current_Unit) then 
Is_Sorted(...))

When compiled for testing, JTrace.Trace is a function call which returns 
true or false based on the selections from a tracing menu that pops up when 
the tracing options are used. When compiled for production use, Trace is an 
array with all of the elements set to False. (At least that was the idea, I 
don't think we ever used it that way.)

The downside here is a bit more noise, but the upsides are obvious (Stefan 
explained them in gory detail). One probably could design something shorter 
with the same effect (that would cut the noise).

                                     Randy.



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