* ANNOUNCE: v5 SPARK tools now available
@ 2000-08-30 0:00 r_c_chapman
0 siblings, 0 replies; only message in thread
From: r_c_chapman @ 2000-08-30 0:00 UTC (permalink / raw)
Praxis Critical Systems is pleased to announce
the immediate availability of release 5 of
the SPARK language and the SPARK Examiner
toolset.
This release is available free-of-charge
to academic institutions for teaching and non-commercial
research purposes. Full support for this release will
be available to a single point-of-contact per
institution.
SPARK remains the only widely-used, unambigous programming
language that supports formal development methods such
as B and Z, while being used in large, real-world
projects such as EuroFighter, Lockheed C130J, SHOLIS,
and the MULTOS CA.
To accompany release 5, a second printing of the textbook
"High Integrity Ada - The SPARK Approach" by John Barnes
is in production.
Release 5 adds significant functionality over
previous releases, including:
Support for proof of programs involving abstract state;
Support for explicit quantifiers in predicates;
Improved generation of proof rules for enumerated types;
Generation of output files in HTML;
Command-line selectable annotation character;
Revised SPARK_IO package complying with the INFORMED design approach.
Please email us for more information at
mailto:sparkinfo@praxis-cs.co.uk
or see our web-site:
http://www.praxis-cs.co.uk/
Yours,
The SPARK Team
Praxis Critical Systems
Note: The SPARK programming language is not sponsored
by or affiliated with SPARC International Inc and is
not based on SPARC(tm) architecture.
Sent via Deja.com http://www.deja.com/
Before you buy.
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2000-08-30 0:00 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2000-08-30 0:00 ANNOUNCE: v5 SPARK tools now available r_c_chapman
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox