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.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 115aec,328f48d6a5cc9748,start X-Google-Attributes: gid115aec,public X-Google-Thread: 103376,328f48d6a5cc9748,start X-Google-Attributes: gid103376,public X-Google-Thread: f43e6,328f48d6a5cc9748,start X-Google-Attributes: gidf43e6,public X-Google-ArrivalTime: 2001-11-28 10:13:43 PST Path: archiver1.google.com!postnews1.google.com!not-for-mail From: rod@praxis-cs.co.uk (Rod Chapman) Newsgroups: comp.lang.ada,comp.software-eng,comp.realtime Subject: ANN: SPARK Toolset Release 6.0 now available Date: 28 Nov 2001 10:13:43 -0800 Organization: http://groups.google.com/ Message-ID: NNTP-Posting-Host: 213.155.153.242 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Trace: posting.google.com 1006971223 9824 127.0.0.1 (28 Nov 2001 18:13:43 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: 28 Nov 2001 18:13:43 GMT Xref: archiver1.google.com comp.lang.ada:17120 comp.software-eng:7601 comp.realtime:4410 Date: 2001-11-28T18:13:43+00:00 List-Id: Praxis Critical Systems is pleased to announce the immediate availability of release 6.0 of the SPARK language and the SPARK toolset. Commercial supported customers will receive their upgrades within the next few days. Tool partners and academic users will be upgraded following that. A new edition of the "SPARK Book" by John Barnes is also planned. Release 6.0 adds significant functionality over previous releases, including: Support for "external variables" - these allow the automated modelling of volatile input and output "streams" to and from a SPARK program. Our "INFORMED" design approach has been updated to illustrate the use of external variables. Modular types with binary modulus are supported in SPARK95 mode. Bit-wise logical operators are permitted for such types. A new "derives null from ..." annotation form allows the declaration of procedures which take parameters, but have no observable effect on any state within the SPARK boundary of a program. This is particularly useful in the construction of data-logging packages, testpoints, diagnostic code and so on. VC-Generation in much improved. In particular, fewer hypotheses are generated for most VCs, resulting in faster simplification of those VCs. SPADE Simplifier version 2.00 ships on Windows and Solaris platforms with this release. This includes improved proof tactics for modular expressions, bit-wise logical operators, and inequalities involving enumerated types. The new Simplifier behaves identically on Windows and Solaris. A new tool called "SPARKSimp" is supplied on Windows and Solaris. This is a "make" style tool for the Simplifier which assists in the proof of large programs. This release re-inforces SPARK's position as the leading language subset and static analysis technology for the construction of high-integrity software. Please email us for more information at sparkinfo@praxis-cs.co.uk or see www.sparkada.com 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.