Re: Ada and Design By Contract

[Peter Amey <peter.amey@praxis-cs.co.uk>]

Volkert wrote:
> Some time ago in c.l.a. was a discussion on 
> adding Assertions (preconditions, postconditions
> and invatiants) to Ada 95. 
> 
> - what is the current status? 
> - who is working on this topic
> - who is interested in Dbc for Ada
> 
> 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).

As Lutz has pointed out in an earlier reply, SPARK certainly provides 
the latter and has done for some years.

There have been some proposals for run-time assertions in Ada 0Y 
although many participants in the review process have found them 
wanting.  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).

Peter