From: sgb@erlang.praxis.co.uk (Stephen Bull)
Subject: Re: others clause
Date: 1996/09/02
Date: 1996-09-02T00:00:00+00:00 [thread overview]
Message-ID: <ytcu3thqfy3.fsf@erlang.praxis.co.uk> (raw)
In-Reply-To: INFO-ADA%96082914113458@LISTSERV.NODAK.EDU
In article <50d4fc$elf@fozzie.sun3.iaf.nl> geert@fozzie.sun3.iaf.nl
(Geert Bosch) writes:
> One of the features I'm really missing in Ada is a syntax to
> specify assertions, pre- and post-conditions and invariants for
> code and interfaces. Compilers wouldn't have to check these
> conditions, except some simple cases like static expressions,
> but they (or external programs) *could* check them and moreover
> compilers could use them for optimizations.
The SPARK language is a secure subset of Ada augmented by an set of annotations
which allow such checks to be made by the support tool the SPARK Examiner.
SPARK is developed and supported by Praxis Critical Systems.
For more information please refer to our web pages:
http://www.praxis.co.uk/technols/spark/sp_lang.htm
--
-----------------------------------------------------------------------------
Stephen Bull Praxis Critical Systems 20 Manvers Street BATH BA1 1PX UK
+1225 444700 (switchboard) +1225 739286 (direct) +1225 739281 (fax)
-----------------------------------------------------------------------------
--
-----------------------------------------------------------------------------
Stephen Bull Praxis Critical Systems 20 Manvers Street BATH BA1 1PX UK
+1225 444700 (switchboard) +1225 739286 (direct) +1225 739281 (fax)
-----------------------------------------------------------------------------
prev parent reply other threads:[~1996-09-02 0:00 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
1996-08-29 0:00 others clause Chris Sparks
1996-08-30 0:00 ` Mike Bishop
1996-08-31 0:00 ` Robert A Duff
1996-09-02 0:00 ` Geert Bosch
1996-09-03 0:00 ` Robert Dewar
1996-09-02 0:00 ` Brian Rogoff
1996-09-03 0:00 ` Adam Beneschan
1996-08-31 0:00 ` Robert Dewar
1996-09-02 0:00 ` Stephen Bull [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