On Tue, 23 Dec 2014, Jean François Martinez wrote:

> Most of the time you don't write pre/postonditions/invariants involving 
> (with functions called) tens of thousands of programming lines and 
> gazillions of CPU cycles

I think, actually, it is fairly common for assertions to require 
"gazillions" of CPU cycles. In fact, it is easy to come up with examples 
where the pre- and postconditions take far longer to execute than the 
subprogram to which they are attached.

A simple example that I love because it is so simple yet so telling is 
binary search of an array. A reasonable precondition is that the array it 
is given is sorted. It might look like

     Pre => (for all I in A'First .. A'Last - 1 => (A(I) <= A(I + 1)))

This takes O(n) time to evaluate. Yet binary search is an O(log(n)) 
algorithm. For large arrays the precondition might take many thousands or 
even millions of times longer to execute than the subprogram itself.

I don't think there is anything particularly unusual about this example. 
Here's another case: suppose you had a procedure that added an item to 
some kind of balanced binary tree. The postcondition might assert that the 
tree is still balanced in whatever sense is appropriate... probably an 
O(n) operation. Yet the insertion procedure is probably O(log(n)). It's 
easy to imagine many examples.

For this reason I assume that in most cases programs must be deployed with 
assertions disabled or else there is little chance the program will be 
able to meet its performance goals. Thus putting anything resembling 
essential program logic in an assertion is, of course, just wrong. 
Forbidding assertions with side effects might be nice, but the programmer 
still has to be careful with them anyway.

Peter