Re: Ada and Design By Contract

[volkert@nivoba.de (Volkert)]

> To keept this thread under some sort of control, I suggest we agree a 
> clear distinction between contracts enforced at run time (by the 
> evaluation of checks and, typically, the raising of exceptions if the 
> contract is vilated) and contracts enforced statically, prior to 
> execuation (typically using proof technology).
I know Spark and i like it, but my question is more in the direction
of Eiffel-like Assertion mechanisms (runtime monitoring/checking).


> There have been some proposals for run-time assertions in Ada 0Y 
> although many participants in the review process have found them 
> wanting.  
Can you/someone give me a pointer to it ...i found only
a paper from Ehud Lamm from the last Ada-Europe Meeting.

> The big problem here is that the really interesting 
> contractual claims may involve items not visible at the point where the 
> contract is being checked (unless the code is rewritten with reduced 
> abstraction to make them visible).
I see not the problem. Can you give a short example.

Volkert