Re: On contracts and implementations

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

"Peter C. Chapin" <PChapin@vtc.vsc.edu> wrote in message 
news:ieWdnXSAKPXPAEPMRVn_vwA@giganews.com...
...
> I think the litmus test for contract code vs "ordinary" code is that the 
> contracts should be removable without changing the functional behavior of 
> the program. This means that any checks of errors arising from the 
> execution environment, such as missing files or bad user input, can't be 
> in contracts.
>
> It is important to be able to remove contracts for performance reasons. 
> I'm not talking about the constant time overhead of extra range checks. 
> I'm talking about major performance costs.
>
> For example a binary search function might reasonably have a pre- 
> condition that states the input array is sorted. Checking that contract 
> requires O(n) time and is thus asymptotically slower than the function 
> itself. One might be able to tolerate that during testing on small data 
> sets. Furthermore it would be useful to be able to prove that nowhere is 
> the function called with an unsorted array. However, it is unlikely that 
> the deployed program could tolerate the slow down in asymptotic running 
> time. On a full sized data set we might be talking about a 1,000,000x 
> reduction in speed!

I understand your point, but I think it's short-sighted to think about 
removing the contracts. If you do so, then the contracts can't be used to 
"hoist" what otherwise have to be checks in the code (as in Text_IO, the 
containers, and many other packages). Turning off these checks in 
language-defined code is a complete non-starter, the result would not meet 
the language specifications (and would introduce erroneousness where none 
currently exists).

Secondly, as compiler's proof abilities increase, most of these contract 
assertions will disappear. The compiler will be able to prove that they 
always will succeed, and thus no check will be made.

After all, this is the case with existing constraints and exclusions. 
Compilers work overtime to eliminate unnecessary checks, and tend to remove 
60-80% of the checks. It's rare that I see an explicit range check when I 
examine generated code these days. The same should happen to assertion 
checks (but only if they are well-written, using globals annotations and/or 
expression functions).

To look further at your example, I agree that evaluating Is_Sorted could be 
prohibitively expensive. But how did that object *get* sorted? One presumes 
that it was explicitly sorted somewhere, in which case that routine has an 
Is_Sorted postcondition. If the compiler can tie those together, there 
certainly is no need to reevaluate the Is_Sorted on a following 
precondition. Similarly, the compiler may have been able to prove that the 
Is_Sorted postcondition is always true. In that case, that won't be executed 
either. So you still will have the safety of checks on, and *still* have no 
actual overhead.

Now, obviously, these things won't always be next to each other; the array 
might have been a parameter. But in that case you can use a predicate to 
ensure that that parameter Is_Sorted, pushing the optimization to another 
level.

To summarize, I expect these to become much like range checks. You'll 
sometimes have to suppress them, but it will be pretty rare, and often you 
can add some subtypes in appropriate places to remove the checks rather than 
actually suppressing them (the latter being more dangerous).

                                                      Randy.