From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,4835289e9b0eb32d
X-Google-Attributes: gid103376,public
From: dewar@merv.cs.nyu.edu (Robert Dewar)
Subject: Re: Critical code, Ada, Eiffel, Ariane etc.
Date: 1997/08/19
Message-ID: <dewar.871993666@merv>#1/1
X-Deja-AN: 267948663
References: <Pine.SUN.3.91.970812160036.17653A-100000@erlang.praxis-cs.co.uk>
 <Pine.SGI.3.95.970813191536.1634A-100000@shellx.best.com>
 <5t9no5$7ut@erlang.praxis-cs.co.uk>
Organization: New York University
Newsgroups: comp.lang.ada
Date: 1997-08-19T00:00:00+00:00
List-Id: <comp.lang.ada>


Gavin says

<<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.>>

Another issue here is complexity in the SPARK examiner itself. Certainly
the SPARK examiner can handle any language construct, since it can certainly
become equivalent to an Ada 95 compiler (indeed we are looking at the issue
of implementing a pragma Restrictions (SPARK) or somesuch in GNAT).

But the examiner is much more than a syntax checker, and part of the 
integrity of the SPARK approach involves keeping the examiner small
and much simpler than a full compiler. So an issue like the addition of
generics has to be considered from this point of view as well.