Re: Critical code, Ada, Eiffel, Ariane etc.

[gavin@praxis-cs.co.uk (Gavin Finnie)]

In article <Pine.SGI.3.95.970813191536.1634A-100000@shellx.best.com>,
Brian Rogoff  <bpr@shellx.best.com> wrote:

>	I looked at the Praxis web page, and noticed that generic units are 
>excluded from the Spark subset. What are the reasons for this choice? 

SPARK has so far totally excluded generics on the grounds of complexity, in
terms of defining a formal model of generics, the additional static analysis
and proof work required, and the effect on human understanding of the source
code (and hence the potential for errors) when generics are used.

However, we recognise that the controlled use of simple generics can assist in
creating re-usable abstractions that can make code easier to structure,
understand and reason about. Also, certain flaws in Ada 83's contract
model have been fixed in Ada 95. We are therefore considering providing limited
support for generics in a future version of SPARK.

Gavin Finnie

Praxis Critical Systems Ltd                Tel (+44) 01225-466991
20 Manvers Street                          Fax (+44) 01225-469006
Bath BA1 1PX
UK