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,
	MSGID_RANDY autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: f43e6,d34a19636b6d3981,start
X-Google-Attributes: gidf43e6,public
X-Google-Thread: 115aec,d34a19636b6d3981,start
X-Google-Attributes: gid115aec,public
X-Google-Thread: 103376,d34a19636b6d3981,start
X-Google-Attributes: gid103376,public
From: r_c_chapman@my-deja.com
Subject: ANNOUNCE: v5 SPARK tools now available
Date: 2000/08/30
Message-ID: <8oj2mr$9pu$1@nnrp1.deja.com>#1/1
X-Deja-AN: 664316505
X-Http-Proxy: 1.0 PROXY,
 1.0 x72.deja.com:80 (Squid/1.1.22) for client 193.114.91.187
Organization: Deja.com - Before you buy.
X-Article-Creation-Date: Wed Aug 30 13:37:35 2000 GMT
X-MyDeja-Info: XMYDJUIDr_c_chapman
Newsgroups: comp.lang.ada,comp.software-eng,comp.realtime
X-Http-User-Agent: Mozilla/4.73 [en] (WinNT; U)
Date: 2000-08-30T00:00:00+00:00
List-Id: <comp.lang.ada>

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.