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-Thread: 103376,11ea67b34f896b17,start X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!postnews.google.com!c13g2000cwb.googlegroups.com!not-for-mail From: "Rod Chapman" Newsgroups: comp.lang.ada Subject: ANN: SPARK Release 7.2 Date: 10 Jan 2005 09:30:54 -0800 Organization: http://groups.google.com Message-ID: <1105378254.831885.84070@c13g2000cwb.googlegroups.com> NNTP-Posting-Host: 217.205.167.130 Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" X-Trace: posting.google.com 1105378258 9551 127.0.0.1 (10 Jan 2005 17:30:58 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Mon, 10 Jan 2005 17:30:58 +0000 (UTC) User-Agent: G2/0.2 Complaints-To: groups-abuse@google.com Injection-Info: c13g2000cwb.googlegroups.com; posting-host=217.205.167.130; posting-account=EhC47gwAAABJYiJ7JUJjwDyYMTWH1OKq Xref: g2news1.google.com comp.lang.ada:7612 Date: 2005-01-10T09:30:54-08:00 List-Id: We're pleased to announce the immediate availability of Release 7.2 of the SPARK Language and Toolset. This release incorporates several significant improvements. Full details are available in the Release Note, which is available from www.sparkada.com. For readers of the SPARK Textbook, upgrade packages are also available from www.sparkada.com including the new language definition, manuals and demonstration tools for IA32/Windows and IA32/Linux. These upgrade packages are also available from the "SPARK Book" page of www.sparkada.com as usual. Supported professional customers are being sent upgrades now. Academic users and tool-partners will receive their upgrades shortly. Some technical highlights of this release include: Language: Full-range record subtypes are now supported. Rules for passing array elements as "in out" parameters have been relaxed (this significantly eases the construction of iterator algorithms.) String constants that are constrained by their initializing expression are allowed. Finally, instantiation and use of Unchecked_Conversion is permitted. Examiner: Flow analyser more accurately models "for" loops that have a static range. New VC Generator model of "for" loops correctly models all loops, including those with a dynamic range where variables controlling the loop exit are modified in the loop body. Declaration of subprograms in the private part of a package is implemented. VC Generator produces hypotheses showing that local variables are "in" their designated subtype. A new "brief" error message mode eases integration with EMACS and GPS by producing "gcc style" errors that can be recognized by such environments. Information flow errors are produced by default in a new easier-to-read format. Refinement proofs between the private and full view of a private type are now supported. The VC Generator can now produce replacement rules for composite constants, under the control of a new command-line switch and a new annotation. Simplifier: New tactics for quantified expressions, structured object updates and scalar inequalities. These give a significant improvement in Simplifier "hit rate" (aka Completeness) for common SPARK idioms, and particularly for proofs of exception freedom. SPARKSimp supports multi-processor machines for improved throughout (NOT available with the Demo toolset...) Other: A new utility "SPARKMake" that automates the production of Examiner index files and meta-files. Yours, Rod Chapman, SPARK Team.