Re: On contracts and implementations

["Peter C. Chapin" <PChapin@vtc.vsc.edu>]

On 07/11/2013 05:35 AM, G.B. wrote:

> There is a claim that contracts of Ada 2012 are part of the
> implementation. They are not.

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!

Peter