From: r_c_chapman@my-deja.com
Subject: ANNOUNCE: v5 SPARK tools now available
Date: 2000/08/30
Date: 2000-08-30T00:00:00+00:00 [thread overview]
Message-ID: <8oj2mr$9pu$1@nnrp1.deja.com> (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.
reply other threads:[~2000-08-30 0:00 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox