From: dewar@merv.cs.nyu.edu (Robert Dewar)
Subject: Re: Critical code, Ada, Eiffel, Ariane etc.
Date: 1997/08/19
Date: 1997-08-19T00:00:00+00:00 [thread overview]
Message-ID: <dewar.871993666@merv> (raw)
In-Reply-To: 5t9no5$7ut@erlang.praxis-cs.co.uk
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.
prev parent reply other threads:[~1997-08-19 0:00 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
1997-08-12 0:00 Critical code, Ada, Eiffel, Ariane etc Peter Amey
1997-08-12 0:00 ` Ken Garlington
1997-08-13 0:00 ` Jon S Anthony
1997-08-13 0:00 ` Brian Rogoff
1997-08-18 0:00 ` Gavin Finnie
1997-08-19 0:00 ` Robert Dewar [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox