|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Issue: 1.1 Status: Definitive
DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date projectname:varchar=DocumentSet Issue 1.1, Definitive, 2ed February 2009 000_000 SPARK Toolset Release Note–Release 7.2
|
|
|
|
Originator |
|
|
|
SPARK Team |
|
|
|
Approver |
|
|
|
SPARK Team Line Manager |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||
|
|
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 High Integrity Systems Limited.
Limited Warranty
Praxis High Integrity 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 High Integrity 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 High Integrity Systems Limited accepts no liability for any programs or data stored or processed using Praxis High Integrity Systems Limited products, including the costs of recovering such programs or data.
SPADE is a trademark of Praxis High Integrity 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
3.1 Relaxation of anti-aliasing rules for array elements
3.2 Unconstrained string constants allowed
4 Other significant Examiner changes
4.1 Declaration of subprograms in the private part of packages
4.3 Added hypothesis for local variables
4.4 Value on entry to loop in Proof context
4.5 Private types and refined proof annotations
4.6 Warning for machine code insertions
4.7 Replacement rules for composite constants
4.8 Original Flow Errors switch
5 Miscellaneous Examiner corrections
5.1 External functions using external procedures
5.2 Examiner static limits increased
5.3 VC Generation, refinement and analysis order
5.4 Subunits of public functions
5.5 Flow analysis of for loops
5.7 Invalid hypotheses for moded globals
5.8 Changed casing for unknown_type
5.10 Scalar type mark as actual parameter
5.11 Unneeded body for embedded package
5.12 Unneeded package elaboration
5.13 Invalid flow analysis for array elements
5.14 Visibility of public child package
6.1 Concurrent simplification with SPARKSimp
6.2 SPARKSimp gives elapsed time
6.3 Improved simplification of VCs with large structured objects
6.4 Correction to simplification of real division
6.5 Improved Simplification of arithmetic expressions
6.6 Improved handling of logical expressions
6.7 Reporting number of Conclusions remaining in /noecho mode
7.1 The “save” command on Windows
7.2 New option “newline_after_prompts”
10.2 SPADE Simplifier and Checker
10.3 Format of Path Function Files
11.1 SPARK95 — The SPADE Ada95 Kernel
11.2 SPARK83 — The SPADE Ada Kernel
11.4 Generation of RTCs for SPARK Programs
11.5 Generation of VCs for SPARK Programs
11.6 Installation manuals - SUN and NT
11.7 Generation PFs for SPARK Programs
12 Limitations and known errors
13 Change Summary from Release 2.0
13.1 Release 2.0 - November 1995
13.4 Release 3.0 - September 1997
13.5 Release 4.0 - December 1998
13.7 Release 6.0 - November 2001
13.9 Release 6.3 – December 2002
14 Operating system compatibility
Document Control and References
Continued development of the SPARK Toolset has resulted in the development of a number of useful features which have been incorporated into Toolset Release 7.2.
This document describes changes in the behaviour of all variants of the SPARK Toolset Release 7.2 compared to Release 7.0.
For further information about this document please contact Praxis High Integrity Systems:
By phone: +44 (0)1225 823829 (direct line), +44 (0)1225 466991 (exchange)
By FAX: +44 (0)1225 469006
By email: sparkinfo@praxis-his.com
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;
3.2 Unconstrained string constants allowed
The SPARK language has been relaxed to admit the declaration of constants of type String without the need for a specific named string subtype to be used. For example the following is now legal:
MyText : constant String := “Hello World”;
This provides the ability to define ‘named strings’, analogous to named numbers in the numeric domain (SEPR 298, SEPR 912).
The Examiner now recognises the generic Unchecked_Conversion function and valid instances of this function. In SPARK95 mode, use of the fully qualified name Ada.Unchecked_Conversion is also allowed.
The Examiner raises a warning whenever an instance of Unchecked_Conversion is used and it does not generate any hypotheses associated with the call[2, section 4.2]. This means that any VCs that make use of an unchecked conversion will not be provable and must be justified on a case-by-case basis. Note that a warning is raised because in the case of an unchecked conversion returning a Boolean type there will be an implicit (possibly fallacious) assumption that the return is in type as no type hypotheses are required for Booleans.
This single generic instance has been admitted to the language specifically to aid the analysis of external interfaces. Our recommended approach to reading interfaces in SPARK95 has been to make use of the ‘Valid attribute to ensure that the data read from the interface is in type. Where the permitted range of values read from the interface does not include the full range of bit values available across the width of the interface then assigning the external variable to a variable of the same (sub)type may raise a constraint error. To overcome this the preferred solution is to read the external variable into a variable of a type that does allow all possible bit values across the interface. Then use unchecked conversion to convert the input data to a variable the type of which only contains the permitted range of values and use the ‘Valid attribute to ensure that the data read from the interface is in type. This new approach avoids any possibility of raising a constraint error when reading the data from the external source.
In SPARK83 where the ‘Valid attribute is not available all range checking must be performed in the raw type before the type conversion is performed.
The following example demonstrates the use of unchecked conversion in this manner.
type Byte is range 0 .. 255;
for Byte’Size use 8;
SignalPort : Byte;
for SignalPort’Address use System.Storage_Elements.To_Address (16#FFFF_FFFF#);
-- Interface to external variable admits any bit pattern.
type SignalT is range 0 .. 5; -- valid range of input signals
for SignalT’size use 8;
…
procedure ReadSignal (V : out SignalT)
--# global in SignalPort;
--# derives V from SignalPort;
is
Signal : SignalT;
function ConvertToSignal is new
Unchecked_Conversion(Byte, SignalT);
begin
Signal := ConvertToSignal(SignalPort);
-- Examiner warns of use of an instance of Unchecked_Conversion here
if not Signal’Valid then
Signal := SignalT’First;
end if;
V := Signal;
end ReadSignal;
The SPARK language now allows (full) subtypes of non-tagged records. For example:
type Pair is record
X : Long_Float;
Y : Long_Float;
end record;
subtype Vector is Pair;
4 Other significant Examiner changes
This section documents other significant changes to the SPARK Examiner made for releases 7.1 and 7.2. Where appropriate, SPARK Examiner Performance Report (SEPR) numbers are given.
4.1 Declaration of subprograms in the private part of packages
Examiner 7.2, 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 provide 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 own variables to have their Ada declaration in the private part of a package.
This format is designed to simplify integration with other development environments and tools.
4.3 Added hypothesis for local variables
Release 7.2 of the Examiner exploits the benefit of data flow analysis by assuming that a local variable, anywhere it is referenced in an expression, must be validly in type[2, Section 4.2]. The additional hypotheses generated by this are especially helpful in the discharge of VCs associated with code containing loops. Note that this assumption depends on:
1 The absence of data flow errors, which would otherwise introduce uninitialised values to local variables.
2 The absence of invalid values. For this reason no assumptions for local variables are made for subprograms which reference external variables or which use Unchecked_Conversion.
4.4 Value on entry to loop in Proof context
The VCG model of for loops has been revised so that the value of a for loop bound is now preserved on entry to the loop and this value is used in wherever the for loop exit condition is required[3, section 3.3]. This model produces correct VCs even when a variable that is used in the evaluation of a for loop bound is later modified in the body of the loop. The value of this variable on entry to the loop can be referred to by using a % suffix on entire variables within proof contexts within the for loop. The following example demonstrates the use of the % suffix.
procedure Double (X : in out MyInt)
--# derives X from X;
is
begin
for I in MyInt range 1 .. X loop
--# assert X% = X~ -- X% refers to the value of X on entry to the loop.
--# and X = X~ + I - 1;
X := X + 1;
end loop;
end Double;
4.5 Private types and refined proof annotations
Examiner 7.2 supports refined proof annotations for operations using private types[3, section 2.7.5]. This enables the specification of the subprogram to contain abstract pre- and post-conditions while the body of the subprogram contains refined proof annotations written in terms of the concrete definition of the type. Proof refinement checks are performed in the same manner as for subprograms that use own variable refinement, although if there is no own variable refinement data flow annotations are not refined and as such are not repeated. For example:
package P
--# own Store : PT;
--# initializes Store;
is
type PT is private;
--# function IsValid (X : PT) return Boolean;
--# function PT2Int (X : PT) return Integer;
procedure IncrementStore;
--# global in out Store;
--# derives Store from Store;
--# pre IsValid (Store);
--# post PT2Int (Store) = PT2Int (Store~) + 1;
private
type PT is record
Valid : Boolean;
F : Integer;
end record;
end P;
package body P
is
Store : PT;
procedure IncrementStore
--# pre Store.Valid; -- Refined pre- and post-conditions
--# post Store.F = Store~.F + 1;
is
begin
Store.F := Store.F + 1;
end IncrementStore;
end P;
4.6 Warning for machine code insertions
Version 7.2 of the Examiner raises a warning if a machine code insertion is detected. Machine code insertions are subject to all the same problems as representation clauses and hidden code, in that the flow associated with such insertions is invisible to the Examiner so raising a warning is appropriate.
4.7 Replacement rules for composite constants
Version 7.2 of the Examiner can generate replacement rules for composite constants used within VCs. Rules are selectively generated based on the current value of the /rules switch and any object assertions relating to the constant within the code. Object assertions take the form:
--# for Const1 declare Rule;
--# for Const2 declare NoRule;
If NoRule is asserted for an object then no replacement rules will be generated when the /rules switch is set to keen, lazy or none. If a Rule is asserted for an object then replacement rules will be generated when the /rules switch is set to keen, lazy or all. For constants with no object assertion replacement rules are generated when the /rule switch is set to keen or all.
Replacement rules for composite constants can improve the success rate of the SPADE Simplifier. However control of replacement rules for composite constants has been provided in recognition that the number of rules generated could be extensive.
Object assertions may be placed anywhere that a basic declarative item is permitted (such as the declaration of a variable or constant).
Multiple object assertions may be supplied for a given constant although each object assertion must be in a different scope, the Examiner will make use of the object assertion in the nearest enclosing scope of the current subprogram. If multiple object assertions are found for a constant in a given scope then the Examiner makes use of the first one found and warns that subsequent object assertions for that constant in that scope are ineffective.
4.8 Original Flow Errors switch
Version 7.2 of the Examiner incorporates an improved formatting of flow error messages:
!!! Flow Error :50: XXX is not derived from the imported value(s) of YYY, ZZZ.
where previously an individual line was written for each error:
!!! Flow Error :50: The imported value of YYY is not used in the derivation of XXX.
!!! Flow Error :50: The imported value of ZZZ is not used in the derivation of XXX.
Note that the structure of the error is reversed, i.e. the variable has moved from the beginning to the end of the sentence. This applies to error messages 50 and 601. If the old format of error messages is required, then the switch “original_flow_errors” should be used.
The VCS switch resulted in VCs being generated corresponding to all pre, post, assert and check statements in proof contexts within the code.
VCs (and their proofs) are only valid on the assumption that there are no run-time errors in the software. This is due to certain assumptions made about variables and return values being in type. The VCS switch did not generate the necessary VCs to prove that the software is runtime error free and thus the results only held subject to the unproved assumption that the software is free from runtime errors.
Due to major enhancements in VCs generation and improvements in the performance and success rate of the Simplifier (in this release of the toolset) it has become far easier to automatically prove the absence of run-time errors. The RTC switch generates VCs for all run time checks (excluding sub-expression overflow checks) in addition to VCs corresponding to proof contexts in the code. The EXP switch adds VCs for expression overflows to those generated by RTC. The EXP switch should now be used in circumstances where the VCS switch was previously used.
5 Miscellaneous Examiner corrections
5.1 External functions using external procedures
In release 7.2, 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.2 Examiner static limits increased
The static limits on the Examiner’s tables have been increased for release 7.2. 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). The number of index files supported by the Examiner has been increased for “mediumspark” and “largespark”. (SEPR 1660)
5.3 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.2. (SEPR 1636)
5.4 Subunits of public functions
Examiner 7.0 failed when analysing subunits of public functions. This problem has been corrected in release 7.2. (SEPR 1654).
5.5 Flow analysis of for loops
If a for loop is of the form
for I in T loop
then the loop must be entered at least once because a type cannot be empty in SPARK. In release 7.2 the flow analyser no longer produces flow analysis for the semantically non-existent path where the loop is not entered. (SEPR 1356)
Invalid iteration schemes of the form
for I in T range T’First .. A’Range loop
were not previously detected by the Examiner. Subsequent VCs were meaningless causing the SPADE Simplifier to fail with a type check error. This has been corrected in release 7.2 of the Examiner and a semantic error is now generated when errors are detected in the construction of the range expression. (SEPR 1708)
In a loop statement ‘for I in TypeMark range 1 .. Expression loop’ the value of the Expression was not frozen on entry to the loop. This resulted in erroneous VCs being generated relating to the exit condition. This is corrected in version 7.2 of the Examiner. VCs now refer to the initial values on entry to the loop of the variables in the for loop range condition (SEPR 968). See also Section 4.4.
5.7 Invalid hypotheses for moded globals
The Examiner erroneously generated VC hypotheses assuming that external variables used within a called procedure are exported in type from the procedure call. External variables (own variables or refinement constituents with the mode in or out) are assumed to be connected to the external environment and, as such, no inferences can be made about the validity of their values.
In certain circumstances this fault could allow invalid proofs of subsequent statements involving external in variables.
Release 7.2 of the Examiner corrects this and no longer generates invalid type hypotheses for these external variables. (SEPR 1738).
5.8 Changed casing for unknown_type
When semantic errors prevent the Examiner from providing type information the Examiner prints UNKNOWN_TYPE in place of the type information in the VCG file. This used to be printed in capitals but this could potentially conflict with prolog variables of the same name and case resulting in unpredictable behaviour in the SPADE Simplifier. Examiner 7.2 now prints unknown_type in lower case, which causes the simplifier to fail with a type check error. (SEPR 1675)
The Examiner did not always correctly locate the elsif part of a conditional when making a line reference for the VCs generated from the elsif expression. This has been corrected in release 7.2. (SEPR 599).
5.10 Scalar type mark as actual parameter
The Examiner could fail to detect a scalar type mark being passed as an actual parameter when an object of that type was intended. This has been corrected in release 7.2 (SEPR 720).
5.11 Unneeded body for embedded package
Where an embedded package contains own variables that are initialised at declaration within the specification the Examiner fails to detect that no package body is required and demands a body. This has been corrected in release 7.2 so a body is only demanded if there are own variables that are not declared or own variables appearing in an initialises clause that are not initialised at declaration. (SEPR 832).
5.12 Unneeded package elaboration
When a package elaboration part is hidden and not required a semantic error relating to the unnecessary package elaboration was raised. In release 7.2 of the Examiner a semantic error is only raised if the package elaboration is not hidden and not required. (SEPR 923)
5.13 Invalid flow analysis for array elements
In rare circumstances where an array element is passed as an actual parameter to an exported formal the Examiner could report that the array index had been modified when it clearly had not. This only occurred where the actual parameter was an element of a global variable, which was its self a refinement constituent. This has been corrected in release 7.2 of the Examiner. (SEPR 1719).
5.14 Visibility of public child package
Release 7.0 of the Examiner reported that a public child of a private child is not visible from the parent package in circumstances when it should have been visible. This has been corrected in release 7.2 of the Examiner. (SEPR 1720)
SPADE Simplifier version 2.17 ships with toolset release 7.2. This version includes the following improvements over and above version 2.12:
6.1 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)[4, Section 7]. 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.
6.2 SPARKSimp gives elapsed time
SPARKSimp has been modified to report the elapsed time for each Simplifier run that it invokes, and the elapsed time for the complete set of files simplified.
6.3 Improved simplification of VCs with large structured objects
The Simplifier now applies a “proof framing” technique to allow the automatic simplification of VCs relating to large structured objects. The simplifier is now able discharge a large class of VCs relating to arrays and records where fields have been updated, giving a far higher simplification rate.
6.4 Correction to simplification of real division
A correction has been made to the SPADE Simplifier to enable it to restructure and simplify expressions involving real division. (SEPR 1674)
6.5 Improved Simplification of arithmetic expressions
Improvements have been made to the SPADE Simplifiers ability to simplify arithmetic expressions and inequalities. In particular additions have been made to the properties of abs, mod and div known to the Simplifier. Additions have been made to the inference engine relating to the numeric bounds of X**Y. Finally enhancements have been made to the deductive reasoning applied to expressions involving inequalities.
6.6 Improved handling of logical expressions
The Simplifier now adopts a standard form for common Boolean expressions. For example, “x = true” is simplified to simply “x”, while “x = false” is simplified to “not x”. Secondly, Boolean equality is replaced by logical equivalence, so “x = y” is simplified to “x « y”.
6.7 Reporting number of Conclusions remaining in /noecho mode
The Simplifier’s /noecho switch has been improved so that the number of remaining Conclusions for each VC is reported. For example:
D:\sparkdev\examiner\cells>spadesimp varname /noecho
SPADE/SPARK Automatic Simplifier, Release Version 2.17
Praxis High Integrity Systems, Bath, England
Copyright (C) 1992-2004 Praxis High Integrity Systems Ltd., Bath U.K.
Incorporating Poplog (C) 1991-95 Integral Solutions Ltd. & University of Sussex
Reading varname.fdl (for inherited FDL type declarations)
Processing varname.vcg ...
Simplified VC: 1 - All conclusions proved
Simplified VC: 2 - 1 conclusion remains unproven
Automatic simplification completed.
Simplified output sent to varname.siv.
This option is particularly useful when used with SPARKSimp’s “echo” option so that the progress of the Simplifier can be observed. For example:
sparksimp /a /e /sargs /noecho
SPADE Proof Checker version 2.03 ships with toolset release 7.2. This includes the following improvements over and above version 2.00:
7.1 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.03 (SEPR 1613)
7.2 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)
The side condition on this rule was incorrect such that proofs using this rule could be unsound. The rule has been corrected in release 2.03. (SEPR 1689)
POGS version 4.0 ships with the toolset release 7.2. This release
· includes support for VCs arising from RavenSPARK task types;
· corrects a small problem where POGS required a large amount of stack memory on the Intel/Linux platform;
· accepts proof using the Checker alone rather than only looking for Checker output if the simplifier output (.siv file) fails to prove all VCs;
· corrects a problem with reporting the date that VCs are proved using the Checker;
· suppresses printing of the date from the .plg file when the /i switch is used.
SPARKMake is a new tool that can be used to automatically generate an index file and a SPARK meta file.
The index file is built by recursively scanning the specified directories for files matching the supplied (or default) regular expression. For each relevant file the compilation unit is extracted and the association recorded in the index file.
To generate a meta file SPARKMake generates the closure of files that are required to examine the root file. These files are added to the meta file in the order in which they must be analysed.
For more details on the use of SPARKMake please see its user manual [1].
Note: SPARKMake is not supplied on VAX/VMS.
There are no known backward incompatibilities introduced between Examiner Releases 7.0 and 7.2.
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.
10.3 Format of Path Function Files
Examiner 7.2 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.
The following user manuals have been updated as part of this release:
11.1 SPARK95 — The SPADE Ada95 Kernel
· Updated to include revised rules for array aliasing and instantiation of Unchecked_Conversion.
11.2 SPARK83 — The SPADE Ada Kernel
· Updated to include revised rules for array aliasing and instantiation of Unchecked_Conversion.
· Adds new error messages and warnings.
· New command line switches
11.4 Generation of RTCs for SPARK Programs
· Updated to describe the new assumption that local values are in type and added note on effect of concurrency.
11.5 Generation of VCs for SPARK Programs
· Updated to describe
¾ the use of attributes of unconstrained “out” mode parameters in subprogram preconditions,
¾ object assertions and composite constant replacement rule generation policy,
¾ the % operator in proof contexts in for loops, and
¾ private type refinement.
11.6 Installation manuals - SUN and NT
· Updates to reflect additional files installed with release 7.2, and to reflect to adoption of FlexLM version 9.
11.7 Generation PFs for SPARK Programs
· Updated to reflect the removal of the ‘ character in expressions.
· Updated for the new “newline_after_prompts” option.
· New user manuals for the SPARKMake utility.
12 Limitations and known errors
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 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)
2 The Examiner does not yet permit the use of 8-bit characters in SPARK 95 user-defined identifiers. (SEPR 818)
3 Universal expressions in a modular context may sometimes require type qualification. (SEPR 1591)
4 The Examiner does not yet permit the use of “use type” following an embedded package specification. (SEPR 747)
5 The Examiner does not yet permit the renaming of packages in the same way that subprograms can be renamed. (SEPR 1391)
6 The Examiner does not yet allow the ‘Base attribute when not used as a prefix. (SEPR 1114)
7 The Examiner does not yet allow S’Range where S is scalar. (SEPR 1115)
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.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.
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 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)
5 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.
Release 2.1 added:
· facilities for proof of absence of run-time errors
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.
· 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
· 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 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.
Release 7.0 of the toolset comprised:
Examiner version 7.0
Simplifier version 2.12
Release 7.0 added:
· Ravenscar profile extensions to the language.
· Support for Ada.Interrupts and Ada.Real_Time in the configuration file.
· The new /noduration command line switch.
· VC generation for unconstrained formal parameters.
· Suppression of VC generation for illegal function bodies.
· New “SPARKFormat” tool.
14 Operating system compatibility
Release 7.2 is not available for VAX/VMS at this time.
The toolset is compatible with Solaris 5.6 through to 9 including those with a 64-bit kernel.
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.
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 professional SPARK toolset for Linux, then please contact us.
Document Control and References
Praxis High Integrity Systems Limited, 20 Manvers Street, Bath BA1 1PX, UK.
Copyright Praxis High Integrity Systems Limited 2009. All rights reserved.
Issue 0.1 (18 November 2004): First draft
Issue 0.2 (23 November 2004): Updates following inspection and issued at draft for User Group.
Issue 0.3 (6th December 2004): Added change to error messages 50 and 601. Introduced SPARKMake utility.
Issue 0.4 (13th December 2004): Incorporated feedback from User Group.
Issue 0.5 (14th December 2004): Update for Simplifier 2.17 and other minor corrections.
Issue 1.0 (6th January 2005): Definitive issue following review S.P0468.79.88.
Issue 1.1 (2nd February 2009): Modify copyright notice.
Updates following review.
1 SPARKMake User Manual, Issue 1.2, January 2005.
2 Generation of RTCs for SPARK Programs, Issue 8.4, January 2005.
3 Generation of VCs for SPARK Programs, Issue 8.6, January 2005.
4 SPADE Automatic Simplifier User Manual, Issue 5.7, January 2005.
CVSROOT/userdocs/Examiner_RN_7p2.doc