Tool Development and Support

 

SPARK Toolset Release Note–Release 7.1

 

 

 

 

 

 

 

 

 

 

 

EXM/RN

Issue: 1.7

Status: Definitive

2nd February 2009

 

DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date projectname:varchar=DocumentSet

Issue 1.7, Definitive, 2nd February 2009

000_000 SPARK Toolset Release Note–Release 7.1

 

 

 

Originator

 

 

SPARK Team

 

 

 

Approver

 

 

SPARK Team Line Manager

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 



Copyright

The contents of this manual are the subject of copyright and all rights in it are reserved. The manual may not be copied, in whole or in part, without the written consent of Praxis Critical Systems Limited.

             

Limited Warranty

Praxis Critical Systems Limited save as required by law makes no warranty or representation, either express or implied, with respect to this software, its quality, performance, merchantability or fitness for a purpose. As a result, the licence to use this software is sold ‘as is’ and you, the purchaser, are assuming the entire risk as to its quality and performance.

Praxis Critical Systems Limited accepts no liability for direct, indirect, special or consequential damages nor any other legal liability whatsoever and howsoever arising resulting from any defect in the software or its documentation, even if advised of the possibility of such damages. In particular Praxis Critical Systems Limited accepts no liability for any programs or data stored or processed using Praxis Critical Systems Limited products, including the costs of recovering such programs or data.

SPADE is a trademark of Praxis Critical Systems Limited

Note:  The SPARK programming language is not sponsored by or affiliated with SPARC International Inc. and is not based on SPARC™ architecture.


Contents

1       Introduction

2       Contact Information

3       SPARK language changes

3.1       Relaxation of anti-aliasing rules for array elements

4       Other significant Examiner changes

4.1       Configuration file

4.2       New “NoDuration” command line switch

4.3       VC generation for unconstrained formal parameters

4.4       Suppression of VC generation for illegal function bodies

4.5       Declaration of subprograms in the private part of packages

5       Miscellaneous Examiner corrections

5.1       Plain output

5.2       Arithmetic precision

5.3       View conversion as a (controlling) function parameter

5.4       External functions using external procedures

5.5       Examiner static limits increased

5.6       VC Generation, refinement and analysis order

6       SPADE Simplifier

6.1       Improved handling of large VCs

6.2       New /norule_substitution command-line switch

6.3       Improved tactics for record field inequalities

6.4       New “echo” switch for SPARKSimp

6.5       Concurrent simplification with SPARKSimp

7       SPADE Proof Checker

7.1       Improved handling of large VCs

7.2       Performance

7.3       The “mod” operator

7.4       The “save” command on Windows

7.5       New option “newline_after_prompts”

8       POGS

9       SPARKFormat

9.1       Examples

10       Backward incompatibilities

10.1       Examiner

10.2       SPADE Simplifier and Checker

10.3       Format of Path Function Files

11       User manual change summary

11.1       SPARK95 — The SPADE Ada95 Kernel

11.2       SPARK83 — The SPADE Ada Kernel

11.3       Examiner User Manual

11.4       Generation of VCs for SPARK Programs

11.5       Installation manuals - SUN and NT

11.6       The SPARK Ravenscar Profile

11.7       SPARKFormat

11.8       Quick Reference Guides

11.9       Generation PFs for SPARK Programs

11.10       Checker User Manual

12       Limitations and known errors

12.1       Tool limitations

12.2       Known error summary

13       Change Summary from Release 2.0

13.1       Release 2.0 - November 1995

13.2       Release 2.1 - July 1996

13.3       Release 2.5 - March 1997

13.4       Release 3.0 - September 1997

13.5       Release 4.0 - December 1998

13.6       Release 5.0 - June 2000

13.7       Release 6.0 - November 2001

13.8       Release 6.1 - June 2002

13.9       Release 6.3 – December 2002

14       Operating system compatibility

14.1       VAX/VMS

14.2       SPARC/Solaris

14.3       Windows NT, 2000 and XP

14.4       Intel/Linux

Document Control and References

Changes history

Changes forecast

Document references

File under

 

 

 


1                 Introduction

Release 7 of the SPARK Examiner toolset is primarily concerned with the introduction of the Ravenscar profile to the language.

The Ravenscar Profile provides a subset of the tasking facilities of Ada95 suitable for the construction of high-integrity concurrent programs.  The Profile will become part of the Ada language standard with the Ada0Y revision.  For a full description of the Ravenscar Profile plus the rationale behind the choice of features, and several detailed examples, see the Ravenscar Guide technical report [1].

The Profile says nothing about the sequential parts of the code in the program; however, its adoption is not sufficient to eliminate certain forms of erroneous or implementation-defined behaviour associated with Ada95 concurrency. Furthermore, the Profile defines a number of new errors that must be detected at run time.

SPARK is a well-established sequential subset of Ada.  Combining the best aspects of the Ravenscar Profile (giving deterministic concurrency) with SPARK (to ensure predictable sequential execution) provides means for constructing highly reliable concurrent programs.  Extensions to the analyses performed by the SPARK Examiner provide a way of statically eliminating all forms of undesirable behaviour defined by the Profile and outlined in the previous paragraph.

The new, concurrent features of SPARK are entirely optional.  If not selected, then the definitions of the sequential SPARK language and of the behaviour of the SPARK Examiner are unaffected.  Where it is necessary to distinguish between sequential SPARK and the new language features, we use the term RavenSPARK.  The term SPARK encompasses both the existing sequential SPARK language and RavenSPARK.

This document describes changes in the behaviour of all variants of the SPARK toolset Release 7.1 compared to Release 6.3.

2                 Contact Information

For further information about this document please contact Praxis Critical Systems:

By phone:              +44 (0)1225 823829 (direct line), +44 (0)1225 466991 (exchange)

By FAX:              +44 (0)1225 469006

By email:              sparkinfo@praxis-cs.co.uk

3                 SPARK language changes

As outlined in the introduction the language changes are primarily concerned with the Ravenscar Profile extensions. For more information on the Ravenscar profile see [1,2,3].

One small, but significant change, has been made to the sequential core of the language; this is described in the next section.

3.1         Relaxation of anti-aliasing rules for array elements

SPARK provides protection against aliasing, which is the accessing of a single memory location via more than one name at a time.  Aliasing can lead to erroneous program behaviour and can undermine program proof.  Section 6.4 of the SPARK language definition defines rules to prevent aliasing between parameters and between parameters and global variables.  One rule, which has now been relaxed, prohibited the use of an array element as an actual parameter if the associated formal parameter was exported.  The rationale for this is that it is impossible to tell whether A (I) and A (J) refer to the same memory location, and hence are aliases, without recourse to proof since the values of I and J are dynamic and maybe even unknown.

The relaxation permits the use of an array element as an actual parameter as long as there is no possibility that aliasing can occur.  This is ensured by the rule that if any part of A is exported by a called subprogram then neither A nor any part of A may appear elsewhere in the list of actual parameters or globals. 

Thus: Inc (A(I)); is legal but Swap (A (I), A (J)); is not.  The anti-aliasing rules for arrays are now identical to those for record fields.

The relaxation is useful for some object oriented programming techniques since it allows an array of (perhaps large) objects to be processed one at a time by a handler without having to make an expensive deep copy before and after the parameter association.  For example:

procedure ProcessAll (X : in out Widgets.ArrayOfWidget)

--# derives X from X;

is

begin

   for I in Widgets.Index loop

      -- previously a local copy would be needed here

      Widgets.Handle (X (I));

      -- and copied back here

   end loop;

end ProcessAll;

 

4                 Other significant Examiner changes

This section documents other significant changes to the SPARK Examiner made for release 7.0 and 7.1.  Where appropriate, SPARK Examiner Performance Report (SEPR) numbers are given.

4.1         Configuration file

The configuration file can now contain definitions for the implementation-defined entities present in packages Ada.Interrupts and Ada.Real_Time. These definitions will be ignored in SPARK95 if the Ravenscar profile is not selected whereas they will cause an error in SPARK83. (SEPR 1552)

See the Examiner User Manual section 4.6 for more details of the configuration file.

4.1.1           Example

 

package Ada.Interrupts is

   type Interrupt_ID is range 1 .. 5;

end Ada.Interrupts;

 

package Ada.Real_Time is

   type Seconds_Count is range 0 .. 2**31-1;

end Ada.Real_Time;

The report file will no longer report package System as being required but not found when it’s included in the configuration file. (SEPR 1463)

4.2         New “NoDuration” command line switch

The Examiner command line has a new switch - noduration. The introduction of the type Standard.Duration to the SPARK language was not upwardly compatible for systems that used “duration” as an identifier. When this switch is specified, the Examiner does not predefine the type Standard.Duration. This enables “duration” to be used as an identifier.  For example, on Windows:

 

spark /noduration test.ada

The switch can be used in SPARK83 or SPARK95 mode. (SEPR 1486)

4.3         VC generation for unconstrained formal parameters

The Examiner now allows the attributes of an “out” mode unconstrained formal parameter to be referenced in a subprogram’s precondition. (SEPRs 1555, 1557)

For example, the following procedure specification is now allowed:

procedure Copy (S : in     String;

                D :    out String);

--# derives D from S;

--# pre D'Last >= S'Last;

4.4         Suppression of VC generation for illegal function bodies

The Examiner no longer allows VC Generation to be attempted for a function body that does not have a legal return statement. (SEPR 399)

4.5         Declaration of subprograms in the private part of packages

Examiner 7.1, except when Ada 83 mode is selected, now permits the declaration of subprograms in the private part of a package specification  (SEPR 1059).  Private subprograms are potentially useful in SPARK 95 because they are visible to public child packages but are not visible elsewhere.  A particular use of private subprograms is  to provided a controlled external view of a subprogram for testing purposes.  For example:

package P

is

   procedure Externally_Available (X : in out Integer);

   --# derives X from X;

   --# post X = X~ + 2;

private

   -- this procedure is conceptually local to P and could be declared in the body of P; however,

   -- declaring it here allows it to independently tested using a child package of P

   procedure Inc (X : in out Integer);

   --# derives X from X;

   --# post X = X~ + 1;

end P;

 

package body P

is

   procedure Inc (X : in out Integer)

   is

   begin

      X := X + 1;

   end Inc;

 

   procedure Externally_Available (X : in out Integer)

   is

   begin

      Inc (X);

      Inc (X);

   end Externally_Available;

end P;

 

with SPARK_IO, P;

--# inherit SPARK_IO, P;

package P.Test

-- this package is not part of the final system build; it

-- is used for module testing only

is

   procedure TestInc;

   --# global in out SPARK_IO.Outputs;

   --# derives SPARK_IO.OUtputs from *;

end P.Test;

 

package body P.Test

is

   procedure TestInc

   is

      X : Integer;

   begin

      X := Integer'First;

      SPARK_IO.Put_String (SPARK_IO.Standard_Output, "Inc of ", 0);

      SPARK_IO.Put_INTEGER (SPARK_IO.Standard_Output, X, 0, 10);

      SPARK_IO.Put_String (SPARK_IO.Standard_Output, " is ", 0);

      P.Inc (X);

      SPARK_IO.Put_INTEGER (SPARK_IO.Standard_Output, X, 0, 10);

      SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);

      -- and so on for other test values

   end TestInc;

end P.Test;

As another example, consider a raw input device that returns values from a channel selected by an input parameter.  We wish to bar direct access to this interface but provide instead a set of more specific interfaces with more meaningful domain names.  We can do this by making the raw input procedure private and using child packages to provide the tailored interfaces.

package Multiplex

--# own State;

--# initializes State;

is

   -- no directly accessible subprograms in this package

private

   -- raw interfce to some external device

   procedure RawRead (Channel  : in     Integer;

                      InputVal :    out Integer);

   --# global in out State;

   --# derives InputVal, State from State, Channel;

end Multiplex;

 

-- public packages can be used to provide tailored interfaces to the raw device

 

with Multiplex;

--# inherit Multiplex;

package Multiplex.ChannelA

is

 

   procedure GetVoltage (Volts : out Integer);

   --# global in out Multiplex.State;

   --# derives Volts, Multiplex.State from Multiplex.State;

end Multiplex.ChannelA;

 

package body Multiplex.ChannelA

is

   procedure GetVoltage (Volts : out Integer)

   is

   begin

      Multiplex.RawRead (Channel  => 42,

                         InputVal => Volts);

   end GetVoltage;

end Multiplex.ChannelA;

 

-- similar children for other channels

Although arguably less useful, the Examiner also now allows a own variables to have their Ada declaration in the private part of a package.

5                 Miscellaneous Examiner corrections

5.1         Plain output

The plain output facility has been improved so that the error pointers point to the correct location. There was a problem whereby the pointers were incorrect if there were more than one error on a single line. This has been resolved. (SEPR 1545)

5.2         Arithmetic precision

The Examiner was failing to process very precise numbers correctly. This problem caused very precise numbers to be reported by the Examiner as being out of range when they clearly were not. The Examiner now accepts more precise numbers and outputs a warning when precision is lost. (SEPR 1475)

5.3         View conversion as a (controlling) function parameter

Prior to this release, the Examiner could sometimes produce incorrect flow analysis of a function call if the actual parameter associated with the controlling parameter was a view conversion.  This problem only affected functions which had a tagged type as a parameter and which also referenced global variables.

5.4         External functions using external procedures

In release 7.1, a function that references an external variable may now call a procedure that also references the same external variable as long as that procedure has no other side-effect. (SEPR 1630)

5.5         Examiner static limits increased

The static limits on the Examiner’s tables have been increased for release 7.1.  The “mediumspark” Examiner now has limits the same as previous versions of “largespark.”  The “largespark” Examiner on the Windows and Solaris platforms now has larger tables in the flow analyser, VC generator, and can accommodate more compilation units and source files in a single analysis run. (SEPR 1634)

5.6         VC Generation, refinement and analysis order

In rare circumstances, the VCs generated by Examiner 7.0 for a package containing state refinement differed depending on the order of package bodies analysed. This problem has been corrected in release 7.1. (SEPR 1636)

6                 SPADE Simplifier

SPADE Simplifier version 2.13 ships with toolset release 7.1. This version includes the following improvements over and above version 2.08:

6.1         Improved handling of large VCs

The capacity of the Simplifier has been improved, particularly where very large VCs (e.g. those with several thousand hypotheses or conclusions) or very large FDL records are concerned. (SEPRs 1530, 1544)

6.2         New /norule_substitution command-line switch

A new command-line switch “/norule_substitution” is now supported.  This switch disables the substitution of FDL constants by literal values given the rules generated by the Examiner in the RLS file. The efficiency of the rule substitution phase has also been improved when it is enabled. (SEPRs 1533, 1534)

6.3         Improved tactics for record field inequalities

Simplifier 2.13 implements a new tactic for conclusions that arise from SPARK 1-dimensional arrays of records.  A typical VC might have conclusions of the form:

 

C1: fld_f(element(a, [i]) >= t__first.

C2: fld_f(element(a, [i]) <= t__last.

Such conclusions are now proven automatically if a suitable quantified hypothesis can be found.

6.4         New “echo” switch for SPARKSimp

A new switch “/e” (or “-e” on UNIX systems) instructs SPARKSimp to echo the Simplifier’s output to the screen. This allows Simplification progress to be monitored more closely if required.

6.5         Concurrent simplification with SPARKSimp

A new switch “/p=n” (or “-p=n” on UNIX systems) instructs SPARKSimp to use n concurrent instances of the Simplifier (the default is 1).  This option allows multiprocessor systems to be used.  The /e switch is not permitted when this option is specified.  Each instance of the Simplifier will require a licence.

7                 SPADE Proof Checker

SPADE Proof Checker version 2.02 ships with toolset release 7.1.  This includes the following improvements over and above version 1.48:

7.1         Improved handling of large VCs

The capacity of the Checker has been improved, particularly where very large VCs (e.g. those with several thousand hypotheses or conclusions) or large FDL records are concerned. (SEPRs 1520, 1522, 1523)

7.2         Performance

The speed of the Checker has also been improved dramatically in the simplification of quantified expressions, in line with the improvements made in Simplifier 2.08. (SEPR 1571)

Note: The improvements to the simplification of quantified expressions may alter the behaviour of the Checker when reading in and simplifying nested quantified hypotheses or conclusions. Such expressions typically arise from SPARK programs that use multi-dimensional arrays, for example. In these cases, proof scripts may require some review and re-work.

7.3         The “mod” operator

When the Checker detects that a VC has been generated by the SPARK Examiner, it now enables the simplification and standardisation of the “mod” operator as defined by Ada.  When the Examiner is not the source of a VC, no simplification or standardisation of “mod” is performed. (SEPR 1583)

7.4         The “save” command on Windows

In release 2.00, the “save” command in Windows platforms did not function correctly if external proof rule families had been used in the proof session.  This problem has been corrected in release 2.02 (SEPR 1613)

7.5         New option “newline_after_prompts”

This option instructs the Checker to send an additional carriage-return/line-feed sequence following every prompt. This may be useful for some users who “drive” the checker from another 3rd party tool or user-interface. (SEPR 1639)

8                 POGS

POGS version 3.2 ships with the toolset release 7.1. This release includes support for VCs arising from RavenSPARK task types, and corrects a small problem where POGS required a large amount of stack memory on the Intel/Linux platform.

9                 SPARKFormat

SPARKFormat is a new tool that is capable of formatting SPARK global and derives annotations to a predefined format. SPARKFormat can add modes to global annotations, which is particularly useful when migrating a project from SPARK83 to SPARK95.  It can also expand derives annotations to their most verbose form, or compress them by grouping like terms and taking advantage of the “*” notation. It is also possible to integrate SPARKFormat with most popular compilers’ development environments and/or text editors, so that SPARK annotations can be formatted automatically.

For full details of SPARKFormat, please see its user manual[4].

Note: SPARKFormat is not supplied on VAX/VMS.

9.1         Examples

The annotation:

 

--# derives A from A,

--#                C &

--#         B, C from B,

--#                   C;

 

would expand to:

 

--# derives A from *,

--#                C &

--#         B from *,

--#                C &

--#         C from *,

--#                B;

and would compress to:

 

--# derives A,

--#         B from *,

--#                C &

--#         C from *,

--#                B;

10           Backward incompatibilities

10.1    Examiner

There are no known backward incompatibilities introduced between Examiner Releases 6.3 and 7.1.

10.2    SPADE Simplifier and Checker

The Simplifier may prove VCs that it previously failed to prove.  This may render existing Checker proof scripts for those VCs redundant.

The Checker implements a slightly different (but much faster) strategy for the simplification and standardisation of quanitifed expressions in version 2.00 and above.  This may require some existing proof scripts to be revised.

10.3    Format of Path Function Files

Examiner 7.1 no longer generates the ‘ character in expressions in PFS files.  For this reason path function files are only compatible with Simplifier 2.13 or above.

11           User manual change summary

The following user manuals have been updated as part of this release:

11.1    SPARK95 — The SPADE Ada95 Kernel

·          Updated to include the Ravenscar profile and revised rules for array aliasing.

11.2    SPARK83 — The SPADE Ada Kernel

·          Updated to include revised rules for array aliasing.

11.3    Examiner User Manual

·          Adds new error messages and warnings.

·          New command line switches

11.4    Generation of VCs for SPARK Programs

·          Updated to describe the use of attributes of unconstrained “out” mode parameters in subprogram preconditions.

11.5    Installation manuals - SUN and NT

·          Updates to reflect additional files installed with releases 7.0 and 7.1, and to reflect to adoption of FlexLM version 9.

11.6    The SPARK Ravenscar Profile

·          New manual describing the design and rationale of the SPARK Ravenscar profile.

11.7    SPARKFormat

·          New user manuals for the SPARKFormat utility.

11.8    Quick Reference Guides

·          Three new quick reference guides are now included with Release 7.0, covering the tools, their main options, the core SPARK annotations and common design patterns.

11.9    Generation PFs for SPARK Programs

·          Updated to reflect the removal of the ‘ character in expressions.

11.10    Checker User Manual

·          Updated for the new “newline_after_prompts” option.

12           Limitations and known errors

12.1    Tool limitations

This section describes limitations of the Examiner tool arising mainly from incomplete implementation of planned features.  Where appropriate a SPARK Examiner Performance Report (SEPR) number is given.

12.1.1       General

1         The flow analyser does not take account of for loops that must be entered because they are looping over a type mark that, in SPARK, cannot be empty.  The flow analysis is identical to the case where the loop range might be empty. (SEPR 601)

2         The SPARK 95 language definition removes the distinction between initial and later declarative items; this distinction remains in force in the Examiner that requires SPARK 83 declaration orders even in SPARK 95 mode. (SEPR 813)

3         The Examiner does not yet permit the use of 8-bit characters in SPARK 95 user-defined identifiers. (SEPR 818)

4         Universal expressions in a modular context may sometimes require type qualification. (SEPR 1591)

5         The Examiner does not yet permit the use of “use type” following an embedded package specification. (SEPR 747)

6         The Examiner does not yet permit the renaming of packages in the same way that subprograms can be renamed. (SEPR 1391)

7         The Examiner does not yet allow the ‘Base attribute when not used as a prefix. (SEPR 1114)

8         The Examiner does not yet allow S’Range where S is scalar. (SEPR 1115)

9         The Examiner does not allow an unqualified string literal to be an actual parameter corresponding to a formal parameter that is a constrained string subtype.  It does work if the formal parameter is the normal unconstrained String type. (SEPR 869)

12.1.2       Verification Condition Generation and Run-time Checks

1         Ada string inequality is not modelled. (SEPR 712)

2         VCs involving string catenation that includes the character ASCII.NUL will be incorrect. (SEPR 661)

3         Aggregates of multi-dimensional arrays cannot be modelled although aggregates of arrays of arrays can. (SEPR 590)

4         Verification conditions involving real numbers are evaluated using infinite precision or perfect arithmetic; this allows the correctness of an algorithm to be shown but cannot guard against the effects of cumulative rounding errors for example.

5         The Examiner does not generate VCs for package initialization parts.  Statically determinable constraint errors will be detected during well-formation checking of package initialization. (SEPR 288)

6         The VC Generator cannot model the implementation-dependent attributes of floating and fixed-point types; see section 12.1.3.

12.1.3       Attribute limitations

12.1.3.1     Unimplemented attributes

The following attributes are officially supported by SPARK according to the language definition, but are not yet implemented by the Examiner.  The Examiner will generate error number 30 (“Attribute XXX is not yet implemented in the Examiner”) if you try to use them.

·          Adjacent

·          Compose

·          Copy_Sign

·          Leading_Part

·          Remainder

·          Scaling

·          Exponent

·          Fraction

·          Machine

·          Model

·          Rounding

·          Truncation

·          Unbiased_Rounding

Note that these are all function-like attributes concerning floating- and fixed-point types.

12.1.3.2     Unevaluable attributes

The Machine_* and Model_* attributes are accepted by the Examiner, but it does not know how to statically evaluate them since they are inherently implementation dependent.  For example, the package:

 

package F is

   type T is digits 6 range –10.0 .. 10.0;

   C : constant := T’Machine_Emax;

end F;

is legal SPARK, but the Examiner does not know the actual numeric value of C.

12.2    Known error summary

This section lists known errors in the Examiner that are awaiting investigation and correction.

1         The SPARK rule that array actual parameters must have the same bounds as the formal parameter is not checked for function parameters where the actual parameter is a subtype of an unconstrained array type.  Since subtype bounds are static in SPARK errors of this kind should be detected by an Ada compiler.  If not an unconditional run-time error will occur. (SEPR 1060)

2         The Examiner permits the body of a subprogram to be entirely made up of proof statements thus breaching the Ada rule that at least one Ada statement must be present. (SEPR 278)

3         Where a package declares two or more private types the Examiner permits mutual recursion between their definitions in the private part of the package. (SEPR 848)

4         The Examiner does not “freeze” for loop bounds properly when generating VCs.  For example given for I in Integer range 1.. F(X) loop where the value of F(X) changes in the body of the loop.  To avoid this problem assign the value of F(X) to a suitable variable and use this as the loop bound. (SEPR 968)

5         The Examiner does not take due account of a range constraint when determining the subtype of a loop variable; this affects completeness checking of case statements within the loop.  For example for I in Integer range 1..4 loop would require only values 1, 2, 3 and 4 to be covered by the case statement. (SEPR 693)

6         When summarising the counts of pragmas found during an analysis the totals may depend on whether units are selected via the command line (or metafile) or using the index mechanism.  The difference affects only pragmas placed between program units and arises because placing a file name on the command line causes the entire file to be analysed whereas selecting it using indexes causes only the required unit to be read from the file. (SEPR 483)

13           Change Summary from Release 2.0

A release note detailing changes from the previous version accompanies each Examiner Release; this section simply summarises the various changes that have been made. 

13.1    Release 2.0 - November 1995

Release 2.0 added:

·          static expression evaluation;

·          variable initialization at declaration;

·          full-range scalar subtypes; and

·          operator renaming in package specifications.

13.2          Release 2.1 - July 1996

Release 2.1 added:

·          facilities for proof of absence of run-time errors

13.3          Release 2.5 - March 1997

Release 2.5 was distributed with “High Integrity Ada - the SPARK Approach” and provided initial facilities for SPARK 95

13.4          Release 3.0 - September 1997

Windows NT was supported for the first time with this release.  Release 3.0 also added:

·          additional SPARK 95 support;

·          flow analysis of record fields;

·          command line meta files;

·          named numbers;

·          unqualified string literals;

·          moded global annotations; and

·          optional information flow analysis.

13.5          Release 4.0 - December 1998

With Release 4.0 we upgraded all users to a single product standard supporting SPARK 83, SPARK 95 and analysis options up to an including proof facilities.  New features were:

·          full implementation of public and private child packages;

·          default switch file; and

·          provision of the INFORMED design document.

13.6          Release 5.0 - June 2000

·          Enhanced proof support:

                                            I.facilities for proof of programs containing “abstract state”;

                                          II.addition of quantified expressions;

                                         III.proof rule generation for enumeration types;

                                        IV.identification of the kind and source of each VC;

                                          V.suppression of trivially true VCs;

                                        VI.Proof Obligation Summariser tool (POGS)

·          Optional HTML output files with hyperlinks that can be “browsed” interactively

·          Better support for common Ada file naming conventions

·          User-selectable annotation character

·          Improved suppression of analysis were results might otherwise be misleading

·          Static expression evaluation in proof contexts

·          Singleton enumeration types

·          Revised SPARK_IO package

·          Error numbering

13.7          Release 6.0 - November 2001

·          Introduction of “external variables” to simplify modelling of the interactions between a SPARK program and its external environment.

·          Addition of the “null derives” annotation to describe information flows which affect only the external environment.

·          Introduction of modular types

·          Use of loop labels in exit statements

·          Use of global modes on function subprograms

·          Extended support for predefined types such as Long_Integer

·          Simplified run-time check generation for own variables

·          Relaxation of need for mandatory type announcement of own variables

·          Plain output option to simplify comparisons of Examiner output files

·          Platform-independent switch files and metafiles

·          Support for intentionally infinite loops

·          Detection of own variables that can never be initialized

·          Detection of unusable private types

·          Extra refinement checks on global variables when performing data flow analysis

·          Detection of unnecessary others clause in case statements

·          Extensions to the POGS tool

·          Improved error messages to distinguish different cases of variables which are “not declared or visible”

·          Improved SPADE Simplifier Release 2.0

·          New “SPARKSimp” Tool

13.8          Release 6.1 - June 2002

·          Introduction of tagged types

·          Introduction of type assertion annotations

·          Introduction of modular subtypes

·          Introduction of the configuration file

·          Introduction of the help command line switch

·          Demo Examiner now runs on Linux.

·          VCG generation for inherited operations of tagged types

·          Improved handling of null derives

·          Attributes ‘Floor and ‘Ceiling implemented

·          Detection of duplicate record fields

·          Improved overflow checks on universal integer expressions

·          Corrected handling of loop invariants in while loops

·          Strengthened behaviour of /noecho option

·          Trapping non-positive accuracy in real type declaration

·          Recursion in meta-files and index-files

·          Improved handling of Address clauses

·          Improved handling of Import and Interface pragmas

·          VCG Modelling of Boolean membership operators

·          Simplification of common Integer inequalities

·          Simplification of common enumerated inequalities

·          Simplification of VCs involving quantified expressions

·          Simplifier performance

·          Checker has new built-in rule families: MODULAR, BITWISE and ENUMERATION

·          Proved by review option in POGS

13.9          Release 6.3 – December 2002

Release 6.3 of the toolset comprised:

                   Examiner version 6.3

                   Simplifier version 2.08

This toolset was constructed to accompany the textbook “High Integrity Software: The SPARK Approach to Safety and Security” by John Barnes, but was not delivered to other users.  Its main new features were:

·          Slight revision to the rules regarding the placement of tagged type declarations.

·          Correction to the modelling of Boolean type membership operators in the verification conditions.

·          Support for generating VCs that allow the verification of the Liskov Subsitution Principal (LSP) for tagged types and their operations.

·          Dramatically improved performance of the Simplifier, particularly in the simplification of quantified expressions.

14           Operating system compatibility

14.1          VAX/VMS

Release 7.0, but not 7.1, of the Examiner is available for VAX/VMS.  Releases of the SPADE Simplifier, Checker, SPARKFormat, and POGS for VAX/VMS are not planned at this time.

14.2          SPARC/Solaris

The toolset is compatible with Solaris 5.6 through to 8 including those with a 64-bit kernel.

14.3          Windows NT, 2000 and XP

The toolset is compatible with Windows NT 4.0, Windows 2000, and Windows XP.  The executables are also known to work on Windows 95 and 98; however, use of the toolset on these operating systems is unsupported.  The FlexLM licence manager software only runs on Windows NT, Windows 2000, or Windows XP.

14.4          Intel/Linux

All the toolset, with the exception of the Checker, is compatible with Intel-based Linux operating systems. Only the “FreeDemo” version of the toolset is currently available for Linux to support buyers of John Barnes’ “SPARK Book.” If you require a full profession SPARK toolset for Linux, then please contact us.

Document Control and References

Praxis Critical Systems Limited, 20 Manvers Street, Bath BA1 1PX, UK.

Copyright Praxis Critical Systems Limited 20039.  All rights reserved.

Changes history

Issue 0.1                   (14 March 2003): First draft

Issue 0.2                   (2 June 2003): Adds Simplifier and Checker sections, and updates Examiner changes for release 6.3d09.

Issue 0.3                   (5 June 2003): Replaces colour Praxis Logo with TrueType Black/White Logo.

Issue 1.0                   (11 June 2003): Definitive issue following review.

Issue 1.1                   (13th June 2003): Add explanation of SEPR 1592

Issue 1.2                   (10th July 2003): Add explanation of sparksimp “echo” switch.

Issue 1.3 (15th August 2003):  Add sections on developments post Release 7.0

Issue 1.4 (2nd October 2003): Add explanation of sparksimp parallel switch, and changed too version numbers.

Issue 1.5 (7th October 2003): Definitive release after review S.P0468.79.87.

Issue 1.6 (29th October 2003): Further actions from review S.P0468.79.87.

Issue 1.7 (2nd February 2009): Modify copyright notice.

Changes forecast

Nil

Document references

1                         Guide for the use of the Ada Ravenscar Profile in high integrity systems.  A.Burns, B. Dobbing and T. Vardanega.  University of York report YCS 348 (2003). http://www.cs.york.ac.uk/ftpdir/reports/YCS-2003-348.pdf

2                         SPARK95 - The SPARK Ada95 Kernel (including RavenSPARK), Issue 4.0. Praxis Critical Systems, 2003

3                         The SPARK Ravenscar Profile, Issue 1.0, Praxis Critical Systems, 2003

4                         SPARKFormat User Manual, Issue 1.0, Praxis Critical Systems, 2003.

File under

CVSROOT/userdocs/Examiner_RN_7.doc