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: f43e6,b761e94375940f9f,start X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,b761e94375940f9f,start X-Google-Attributes: gid103376,public X-Google-Thread: 115aec,b761e94375940f9f,start X-Google-Attributes: gid115aec,public X-Google-Thread: 108717,b761e94375940f9f,start X-Google-Attributes: gid108717,public X-Google-ArrivalTime: 2002-07-11 00:57:54 PST Path: archiver1.google.com!postnews1.google.com!not-for-mail From: rod@praxis-cs.co.uk (Rod Chapman) Newsgroups: comp.lang.ada,comp.realtime,comp.programming,comp.software-eng Subject: ANNOUNCE: SPARK toolset 6.1 now available Date: 11 Jul 2002 00:57:54 -0700 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 1026374274 29123 127.0.0.1 (11 Jul 2002 07:57:54 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: 11 Jul 2002 07:57:54 GMT Xref: archiver1.google.com comp.lang.ada:27002 comp.realtime:5809 comp.programming:34866 comp.software-eng:11985 Date: 2002-07-11T07:57:54+00:00 List-Id: Praxis Critical Systems is pleased to announce the immediate availability of release 6.1 of the SPARK language and the SPARK toolset. Commercial supported customers will receive their upgrades within the next few weeks. Tool partners and academic users will be upgraded following that. A new release for readers of John Barnes' "SPARK Book" will be available soon. The full release note is available on-line at www.sparkada.com The full definition of SPARK ("The SPARK Report") is also available to interested parties upon request. Release 6.1 of the SPARK language adds: - A useful subset of Ada95's tagged types are now permitted in SPARK95. Inheritance and extension of tagged types are allowed, as is the overriding of basic operations. Dispatching operations are not permitted. - A new "type assertion" annotation can be used to specify the predefined base type from which an integer type declaration is derived. A complementary configuration-file mechanism allows a user to specify the details of packages Standard and System for a particular implementation. When used together, these facilities greatly improve the Simplifier's ability to discharge run-time exceptions verification conditions arising from Overflow_Check in both SPARK83 and SPARK95. - Both full-range and constrained subtypes of modular types are now permitted in SPARK95. There are also significant enhancements to the Examiner, Simplifier and Checker with this release. Highlights include: - When the configuration file mechanism is used to specify packages Standard and System, the Examiner can check a number of additional static semantic rules of Ada. This also improves VC generation and simplification where the ranges of the predefined base types are required. - Simplifier version 2.04 ships on Windows and Solaris platforms with this release. This includes improved proof tactics for enumerated inequalities, common SPARK idioms such as a "for" loop over an enumerated range, and simplification of quantified expressions. The performance of the simplifier has also been greatly improved on large VCs. - Checker 1.47 ships on Windows and Solaris with this release. This includes extended rule families for dealing with modular arithmetic, bitwise operators and enumerated types. This release re-inforces SPARK's position as the leading language subset and static analysis technology for the construction of high-integrity, critical 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.