Issue: 1.0 |
||
Status: Definitive |
||
7th November 2001 |
||
|
||
Originator |
|
|
Rod Chapman, Peter Amey |
||
|
||
Approver |
|
|
David Stokes |
||
|
||
|
||
|
|
|
|
|
|
|
|
|
Contents
3.2 Addition to derives annotation
3.4 Exit statements and loop labels
3.5 Global modes on function subprograms
4 Other significant Examiner changes
4.1 Improved run-time check generation
4.2 Relaxation of mandatory type announcement
4.4 Platform-independent switch files and metafiles
4.5 Intentionally infinite loops
5.1 Own variables that can never be initialized (SEPR 726)
5.3 Extra refinement check on global variables
5.4 Unnecessary others clause in case statements
5.5 Extensions to the POGS tool
5.7 SPADE Simplifier Release 2.0
8.1 SPARK — The SPADE Ada Kernel andSPARK95 — The SPADE Ada95 Kernel
8.3 Generation of verification conditions from SPARK programs
8.4 Generation of run-time checks from SPARK programs
8.5 Generation of path functions from SPARK programs
8.6 SPADE Simplifier User Manual
8.7 INFORMED Design Method for SPARK
9 Limitations and known errors
10 Change Summary from Release 2.0
10.1Release 2.0 - November 1995
10.4Release 3.0 - September 1997
10.5Release 4.0 - December 1998
11 Operating system compatibility
The SPARK[1] Examiner has undergone considerable development and revision since Release 5.0. The largest component of this work involves better support for describing the interaction of SPARK programs with the external environment (see Section 3.1); however, a large number of other improvements has also been made.
This document describes changes in the behaviour of all variants of the SPARK Examiner Release 6.0 compared to Release 5.0.
For further information about this document please contact Praxis Critical Systems:
By phone: 01225 466991
By FAX: 01225 469006
By email: sparkinfo@praxis-cs.co.uk
SPARK programs are often used in control situations where they read values from the external environment via sensors and seek to control the environment via actuators. Program variables whose values are obtained from external sensors do not behave like “normal” variables because their values can change without any assignment being made to them; in short, they are volatile. It has always been possible to simulate this volatility in SPARK by careful use of subprogram annotations; however, the methods used do sometimes lead to an undesirable lack of clarity. Furthermore, it is usually not possible to examine the bodies of packages that perform input or output since flow analysis of these bodies is unlikely to match the annotations provided to simulate volatility.
A major new development of the SPARK language provides a straightforward way of dealing with input from and output to the external environment and automates volatility issues. The approach is based around the use of modes on own variables, similar to parameter and global modes, to indicate that the own variable value (or a refinement constituent of an own variable) is obtained from or sent to the environment. Once own variables are annotated in this way, it is no longer necessary to simulate volatility by writing special forms of derives annotations; the Examiner correctly constructs the required volatile behaviour.
A full description of this important development will be found at Appendix A.
The derives annotation has been extended to allow an indication that one or more imports to a procedure are used but have no externally visible effect (in the form of dependent exports). This addition is primarily motivated by the introduction of external variables because these result in cases for which the new notation is useful. For example, see Section A.5.6, which describes a procedure which “busy waits” by reading a sensor until a particular value, passed in as a parameter, is received.
The grammar of the dependency relation is extended as follows (addition in italic text):
+ dependency_relation ::=
--# derives [ dependency_clause { & dependency_clause }
[ & null_dependency_clause] ]; | --# derives null_dependency_clause;
+ dependency_clause ::=
exported_variable_list from [ imported_variable_list ]
+ exported_variable_list ::= exported_variable { , exported_variable }
+ exported_variable ::= entire_variable
+ imported_variable_list ::= * | [ * , ] imported_variable { , imported_variable }
+ imported_variable ::= entire_variable
+ null_dependency_clause ::= null from imported_variable { , imported_variable }
It can be seen that the new null_dependency_clause is optional but if present must be the last clause in the dependency relation. The following are all examples of syntactically valid dependency relations incorporating the new clause.
--# derives null from Sensor.Inputs;
--# derives X from Y &
--# null from Z;
--# derives A, B, C from *, X, Y, Z &
--# P from Q &
--# null from Clock.Seq;
The only additional rule for the list of imports is that they must not have appeared as imports anywhere else in the dependency relation. This should be easy to understand and remember: the null dependency clause is a statement that nothing is being derived from this import, if it appears anywhere else then something is being derived from it. This is also the reason the new clause appears last.
As noted earlier, the primary reason for the introduction of the new notation is to handle cases arising from the reading of external variables as described in Annex A. Only in these cases will it be possible to construct an error-free procedure body that matches the annotation.
There are, however, other uses for the null derives clause as described below. These cases may require the hiding of procedure bodies or the acceptance of flow errors in them. For these reasons, great care should be exercised when using the null derives in these ways.
A common paradigm is the use of a procedure to provide a variable time delay. The required delay is passed in as a parameter, thus:
procedure Delay (X : in MilliSeconds);
If we are not explicitly modelling time by means of some clock sequence global variable then this leaves us with the problem of deciding what is derived from X. Since nothing visible inside the boundary of the SPARK program is affected by X (the only effect is to consume clock ticks outside the boundary) it is reasonable to annotate the procedure:
--# derives null from X;
Where the delay procedure is called with a constant value for the delay period, e.g. Delay (10); , then this reduces, in flow analysis terms, to a null statement which is correct.
Where it is anticipated that a parameter will be needed at some future stage of program development it might be convenient to include it in the subprogram signature and use a null dependency clause to indicate that it is currently unused. Flow errors will occur in the body indicating that the parameter “is imported but neither referenced nor exported” but these could be justified until a later development stage made use of the parameter.
For test, or some other purpose, we may wish to log the values of variables but not wish this, perhaps temporary, requirement to affect the annotations describing the code’s behaviour. The null dependency can be exploited to reconcile these contrary aims as follows:
package DataLog
is
procedure Store (Msg : in String;
Val : in Integer);
--# derives null from Msg, Val;
-- Above is not true but we want to hide logging from the Examiner.
-- The package body will have to remain hidden.
end DataLog;
we can then use the Store operation to capture values without affecting the flow relations of the monitored subprogram.
procedure Sum (X, Y : in
Integer;
Tot : out Integer)
--# derives Tot from X, Y;
is
begin
Tot := X + Y;
DataLog.Store ("Total=",
Tot); -- no
effect on analysis
end Sum;
Modular types are now supported in SPARK95. The syntax of type definitions is extended, thus:
+ type_definition ::=
enumeration_type_definition | integer_type_definition |
real_type_definition | array_type_definition |
record_type_definition | modular_type_definition ;
+ modular_type_definition ::=
mod simple_expression ;
SPARK restricts the use of modular types in the following ways:
· The Modulus of a type must be a positive power of 2.
· Subtypes of modular types are not permitted.
· Unary arithmetic operators (unary -, +, abs) are not permitted. The unary “not” operator is allowed, as are all binary arithmetic and logical operators.
· To avoid possible confusion, an unqualified universal expression may not be implicitly converted to a modular type if the context of that expression is unknown. To illustrate the final restriction, consider:
type T is mod 4;
A : constant := 2;
B : constant T := 3;
C : constant Boolean := (A + 2) < B;
In Ada, the constant C is initialised to the value True, since the (A + 2) term is evaluated using the modular “+” operator for type T. In SPARK, this is illegal, since the context of the expression is lost on either side of a relational operator such as “<”. The Examiner generates the error:
6 C : constant Boolean := (A + 2) < B;
^1
*** ( 1) Semantic Error :804: Universal expression may not be implicitly converted to a modular type here. Left hand operand requires qualification to type T.
To make such expressions legal, qualification of the offending universal expression is required:
C : constant Boolean := T’(A + 2) < B;
SPARK, since Edition 3.1 of the “SPARK Report”, has permitted loop labels for reasons of documentation and clarity. To complement this feature, the language has been further extended to allow loop label names to appear in exit statements. Note that this does not remove the SPARK rule that an exit statement can only be used to leave the most closely-enclosing loop (see Section 5.7 of the SPARK Report).
Example of a legal loop using the new language feature:
SearchLoop: loop
Found := LookForSomething;
exit SearchLoop when Found;
NextItem (LastOne);
if LastOne then
Found := False;
exit SearchLoop;
end if;
end loop SearchLoop;
The following loop remains illegal because the exit is not just from the innermost loop:
Outer: loop
Inner: loop
DoSomething;
exit Outer when Condition; -- illegal exit to Outer
end loop Inner;
end loop Outer;
Global variables of functions are now permitted to have a mode (in the same way that procedure globals may have modes). For functions the mode can only be “in”. The change is for consistency with the way function parameters are handled; these may be of either mode in or of the default (i.e. no) mode. Function globals now have exactly the same rule. (SEPR 1095).
The following function declarations (that search a table for a value and return a Boolean result) are semantically identical:
function LookFor (X : T) return Boolean;
--# global Table;
function LookFor (X : in T) return Boolean;
--# global Table;
function LookFor (X : T) return Boolean;
--# global in Table;
function LookFor (X : in T) return Boolean;
--# global in Table;
Three predefined type declarations have been added: Duration, Long_Integer and Long_Float. These are declared in package Standard and are directly visible throughout SPARK programs.
Type Duration is now predefined in package Standard as a fixed-point type. Values for its attributes such as 'First, 'Last and 'Delta are not provided since they are implementation-defined.
Long_Integer is predefined as an integer type. Values for Long_Integer'First and Long_Integer'Last may be provided in the target data file. Although SPARK provides this declaration, there is no guarantee that a particular Ada compiler will also do so; clearly users should not use Long_Integer unless their compiler supports it.
Long_Float is predefined as a floating point type. Like Duration, no values for the attributes of the type are provided. Like Long_Integer it should not be used unless supported by the Ada compiler being used.
The rules of SPARK require that array component subtypes statically match in array type conversions. Prior to SEPR 1079 the Examiner generated RTC VCs to show this; however, the Examiner also checks this statically. Since no well-formed SPARK array type conversion can cause a run-time error the RTC check is unnecessary and has been removed.
The Examiner generates hypotheses showing that imports to a subprogram are within their type bounds and conclusions to show that the exports also remain in type. These checks are made for both parameters and any global variables which have a concrete Ada type. Where the globals concerned are own variables of packages which can only be manipulated by subprograms exported by that package, it is not possible for a run time error to occur at the point where these subprograms are called (if such an error is possible it will occur inside the called subprogram). Therefore, hypotheses and conclusions concerning global variables which are own variables of packages are required only if that own variable is directly visible according to Ada rules. Currently the Examiner generates unnecessary run time checks for global imports which can only be manipulated indirectly.
SEPR 1172 removes these unnecessary checks. The following example illustrates the change of behaviour that occurs.
package Q
--# own State : Integer; -- type announced own variable
--# initializes State;
is
procedure Get (X : out Integer);
--# global in State;
--# derives X from State;
end Q;
--# inherit Q;
package P
is
procedure Get (X : out Integer);
--# global in Q.State;
--# derives X from Q.State;
end P;
with Q;
package body P
is
procedure Get (X : out Integer)
is
begin
Q.Get (X); -- indirect use of own variable
end Get;
end P;
Previously the run time checks for P.Get would have been:
procedure_get_1.
H1: true .
H2: q__state >= integer__first .
H3: q__state <= integer__last .
H4: x__1 >= integer__first .
H5: x__1 <= integer__last .
->
C1: x__1 >= integer__first .
C2: x__1 <= integer__last .
Where H2 and H3 are unnecessary because there is no way that Q.State could go outside its permitted type range as a result of actions in P.Get. After SEPR 1172 the checks simplify to:
procedure_get_1.
H1: true .
H2: x__1 >= integer__first .
H3: x__1 <= integer__last .
->
C1: x__1 >= integer__first .
C2: x__1 <= integer__last .
This correctly captures the necessary checks because it shows that the parameter returned by the call to Q.Get is correctly in type and requires proof that the value returned by P.Get is also in its type.
Substantial reductions in the size of VCG files produced from run time checks can be expected.
Release 5.0 of the Examiner introduced a backward incompatibility with earlier releases by requiring that own variables which were directly implemented as concrete Ada variables had to be type announced with their Ada type. This rule was introduced as a consequence of work on abstract proof.
As a result of SEPR 1172 (described above), this mandatory type announcement is no longer required. It is the case now that the type information provided could only ever be used to generate checks which SEPR 1172 has now rendered unnecessary. We apologise for those affected by the transient introduction and removal of this mandatory type announcement rule.
Type announcing own variables is now only ever required where there is a need to write subprogram specifications concerning the own variable; the announcement allows the signature of, for example, a proof function to be completed. For example:
package P
--# own State : T; -- type announcement
is
-- type declaration of T
goes here
-- it doesn’t matter
whether T is an Ada type or an abstract type
-- it lets us write the
signature for HighValue
--# function HighValue (S : T)
return Integer;
procedure
GetHigh (X : out Integer);
--# global in State;
--# derives X from State;
--# post X = HighValue (State);
-- and use it in the postcondition of
GetHigh
...
The new plain_output switch suppresses the printing of line numbers, error numbers and dates in all Examiner output. This can be useful for regression testing, where two sets of Examiner output are to be compared.
For convenience when working in a mixed-platform environment, switches and file options in default switch files and in meta files can be introduced with the Solaris switch character ‘-‘ regardless of the platform on which the Examiner is being run. Switches placed on the command line must still be in the form appropriate to the platform.
Continuous control systems usually incorporate an endless loop at the main program (scheduler) level. In order for the Examiner to produce useful analysis from such loops it has always been necessary to provide a syntactically feasible (even if semantically infeasible) exit path from the loop. Traditionally this takes the form of adding “exit when False” as the last statement of the loop. SEPR 1128 now allows a plain loop without exits to be used without the need for this programming “trick”.
A plain loop, with neither iteration scheme nor exit statements, may only appear as the last statement, at the outermost scope, of the main subprogram. Should it be desired to place an infinite loop anywhere else, the exit when False method may still be used.
The analysis of such infinite loops is identical to that obtained where the last statement is exit when False.
The Examiner now warns if it finds a declaration of an own variable where there is no means by which the own variable could ever be given an initial value. The warning is issued if:
· the own variable is not declared in the visible part of the package (where it could be directly updated); and
· the own variable does not appear in an initialization clause (which would indicate that it is initialized during elaboration or by the system environment);
· there is no exported procedure which exports the own variable without importing it; and
· the own variable does not have a mode (see Section 3.1 and Appendix A).
Prior to this change the inability to make use of the own variable (without causing a data flow error) would not be detected until the main subprogram was analysed.
SEPR 1127 introduces checks similar to those described above but for private types rather than own variables. A limited private type is unusable unless the package which declares it also declares a procedure which exports a parameter of the type without also importing it.
For non-limited private types we need either a procedure (as above), a deferred constant or a function that returns the private type without importing it.
The declaration of limited and non-limited private types without a means to initialize variables of those types now results in a warning from the Examiner. These warnings always indicate a problem in SPARK 83; however, in SPARK 95 the required constructor might be placed in a public child of the package that declares the type. For this reason the warning generated is weaker in SPARK 95 than in SPARK 83 and can be suppressed using the warning control file mechanism.
The Examiner checks the consistency of abstract and refined global annotations. An additional test has been added by SEPR 1200; this checks that each own variable which appears in the abstract global annotation and which is not subject to refinement in the package body, appears unchanged in the refined global annotation. For example:
package P
--# own NotRefined, Refined;
is
procedure K;
--# global out Refined;
--# in NotRefined;
--# derives Refined from
NotRefined;
end P;
package body P
--# own Refined is X, Y;
is
NotRefined,
X,
Y : Integer;
procedure K
--# global out X, Y;
--# in NotRefined;
--# -- the new check is that NotRefined must appear here
--# derives X, Y from NotRefined;
is
...
Generally the new check will simply clarify error conditions that are already reported by the Examiner; however, in some rare cases involving data flow analysis only, the new check may be the only one indicating a refinement error.
The Examiner now issues a warning when an “others” clause is redundant in a case statement. A new keyword “others_clauses” can be used to suppress this warning in the warning control file. (SEPR 1054). Unnecessary others clauses are potentially harmful because they may cause misbehaviour if the type which is being cased over is later extended.
The “POGS” tool now recognizes and processes the verification conditions produced by the Examiner for the refinement of abstract own variables. (SEPR 1065).
Semantic error 1, (“The identifier XXX is either undeclared or not visible at this point.”) has been improved for many common cases. The new, more detailed, errors are numbered 750–754.
The SPADE Simplifier release 2.0 is shipped now on Windows and SPARC/Solaris platforms. This includes numerous inprovements:
· Impoved abilitity to prove thoerems involving inequalities over enumerated types.
· The ability to reason about expressions involving modular arithmetic. This is useful given the addition of modular types in SPARK95.
· A /noecho switch that suppresses the Simplifier’s screen output.
· A /plain switch that suppresses date- and time-stamps in the Simplifier’s output. This is useful when used in conjunction with the Examiner “plain output” switch, and the POGS “ignore date stamps” switch.
A new tool called “SPARKSimp” is provided with this release. This is a “make” style tool for the Simplifier. It traverses a directory tree of files, looking for VCG or PFS files that require simplification, either owing to the absence of a corresponding SIV or SIP file, or if the corresponding file is out of date. SPARKSimp then applies the SPADE Simplifier to the list of VCG or PFS files discovered.
Full documentation of SPARKSimp is included in the SPADE Simplifier User Manual.
· The verification condition generator does not word-wrap long type attribute names in the generated VCG file. (SEPR 1073).
· The Examiner now generates a valid proof model of for loops through type Boolean. Previously the FDL model generated included inequalities between Boolean types which are not permitted. (SEPRs 714, 1101).
· If an abstract own variable was “type-announced” and there was no abstract definition of that type provided, the somewhat misleading error message "XXX has already been declared or refined" was issued if a later attempt was made to refine the own variable. The error message is misleading since at the point where it is issued the own variable is neither declared nor refined! SEPR 1085 tries to distinguish between an illegal refinement and a missing abstract type declaration and provide a suitable error message for each case. (SEPR 1085).
· If a type was announced in an own variable declaration and was later implemented as an unconstrained array type the Examiner gave the message "Private types may not be unconstrained arrays"; this is somewhat misleading. SEPR 604 provides appropriate error messages distinguishing the own variable and private type cases.
· When the predefined ** (exponentiation) operator is used with a Float parameter as Left, and an Integer as Right, there is the possibility of Constraint_Error being raised if Left = 0.0 and Right is negative. When in /rtc /real or /exp /real mode, the Examiner did not generate a VC to eliminate this exception. SEPR 1004 adds a check of the form:
--# check (Left = 0.0) -> Right >= 0;
for all occurrences of Left ** Right where Left is of any floating point type and Right is an Integer type. See LRM 4.5.6(9-13)
· The Examiner now correctly generates a check that the operand of a type conversion is in the subtype of the target type for real numbers when the optional RealRTC switch is used. SEPR 1049.
· The Examiner wrongly allowed package prefixes to be repeated in annotation expressions. For example, it was possible to refer to variable X in package P as P.P.P...X. SEPR 1029 corrects this error.
· Additional hypotheses are generated for refinement proofs to show that refinement constituents that are not used at all must be unchanged. This allows completion of some refinement proofs that were previously intractable. SEPR 1158.
· The Examiner no longer malfunctions when both a superindex and an auxiliary index file are referenced in a single index file. (SEPR 1081).
· The Examiner index mechanism malfunctioned if an attempt was made to look up children of package Ada. SEPRs 1099 and 1103 correct this error.
· Under certain uncommon circumstances, the Examiner wrongly considered global variables to be visible when they were not. The problem was associated only with own variables declared in the visible part of a package being viewed from inside a loop. There was no risk of an undetected error occurring since consequential error messages were always generated. SEPR 889 corrects this problem. SEPR 1083 is a special case of this problem involving record fields. (SEPRs 889, 1083).
· Certain malformed Examiner command lines (e.g. spark /i ) where an expected argument was omitted caused the Examiner to terminate with a constraint error. (SEPR 1082).
· Ada 95 attribute 'Valid is now implemented. (SEPRs 1090, 1106). Suitable proof rules for uses of 'Valid are generated.
· The SPARK95 attributes 'Min and 'Max are now fully implemented. (SEPRs 1107, 1110).
· When the Examiner cross checked global modes against the derives annotation any errors were not prefixed with the package name which could make them hard to understand. SEPR 1094 adds package prefixes where necessary.
· All Ada95 Attributes are now recognized in SPARK95 mode, although a number listed in the SPARK95 report remain unimplemented in this release. The unimplemented attributes are: 'Ceiling, 'Exponent, 'Floor, 'Fraction, 'Machine, 'Model, 'Rounding, 'Truncation, 'Unbiased_Rounding, 'Adjacent, 'Compose, 'Copy_Sign, 'Leading_Part, 'Remainder, 'Scaling, 'Base (when not used as a prefix), and S'Range (where S is a scalar). (SEPR 814).
· A malformed pragma Import (SPARK95) or Interface (SPARK83) is no longer regarded as completing the body of the corresponding subprogram. (SEPR 823).
· When Examiner semantic “notes” are suppressed by use of the warning control file, the total number of notes is now correctly reported in the Examiner Report file. (SEPR 830).
· Attributes (such as 'First and 'Last) of constrained subtypes of unconstrained arrays are now allowed by the Examiner. (SEPR 855).
· The installation application for Windows NT has been corrected to more robustly handle the setting of environment variables, and to co-exist with other tools, such as Rational APEX. (SEPRs 1072, 1075).
· In Release 5.0, temporary files used by the Examiner were always written to the root directory of the current working drive; this sometimes caused difficulties on networks were users did not have write priveleges to that location. With Release 6.0, the Examiner writes temporary files to the following locations, in the following priority order:
1 The directory indicated by the %TMP% environment variable.
2 C:\h \tEMP.
3 The root directory of the current drive.
Users may control the location of temporary files by changing the setting of %TMP%.
There are no backward incompatibilities introduced between Release 5.0 and Release 6.0; however, the improvements made to run-time check generation changes the content of VC files and may cause automatic replay of existing proof scripts to fail.
· Extensive additions and modifications to account for the language changes described in section 3.
· The command summary tables at Section 3.1 have been updated with description of the version and plain_output switches.
· Section 3.2 and 4.1 describe the use of Solaris switch characters in a mixed-platform environment.
· A new section 4.6.3 describes how the Examiner uses temporary files.
· Sections 6.2 and 6.3 have been updated with new error and warning messages together with their explanations.
· New section 3.3.1.3 describes the implicitly declared “proof attributes” used to model external variables. Their FDL representation is described in Section 6.4.5.3.
· Section 3.4.1 contains a new note about implicit preconditions associated with the types of imports to subprograms.
· Section 3.4.2 and 6.6.5 include an explanation of the use of implicitly-declared proof functions and refinement proofs.
· Section 6.4.12 has been extended to cover for loops through Boolean and intentionally infinite loops.
· Section 8.8 has been split into two sub-sections. The first, largely unchanged from previous versions, describes traditional methods of dealing with “ports” and the second, which is new, describes the use of external variables.
· The embedded controller example at Section 8.9 has been re-worked using external variables.
· Section 3.2 provides a description of the optional RealRTCs switch.
· Section 4.1.4 clarifies the RTCs that are generated for array type conversions.
· Section 4.1.6 clarifies the RTCs that are generated for conditional expressions.
· Section 4.1.7 describes an additional run-time check for exponentiation involving real numbers.
· Section 4.2 provides an extensive description of the RTC implications of external variables.
· Section 3.2 has been extended to describe the modelling of procedure calls which involve the importing or exporting of external variables.
· Section 5 adds documentation of new /noecho and /plain command line options.
· New section 7 documents the new SPARKSimp tool.
· Re-written to illustrate the use of external variables.
· Updated to reflect POGS version 1.2 and its new “ignore date stamps” command line switch.
This section describes limitations of the Examiner tool arising mainly from incomplete implementation of planned features.
1 Array aggregate and case statement completeness checking: in some, rare, cases involving very large type ranges in the absence of an others clause, a warning may be produced that the Examiner cannot check the completeness of the aggregate or case statement.
2 Target data files can be used only to set values for integer’last, integer’first and their long equivalents. The values supplied can only be literals. It is intended to extend the range of machine-specific values that can be supplied and allow the use of static expressions rather than literals.
3 The flow analyser does not take account of for loops which must be entered because they are looping over a type mark which, in SPARK, cannot be empty. The flow analysis is identical to the case where the loop range might be empty.
4 The Examiner uses a simplification of the Ada type system designed to avoid the need for overload resolution. As a result it may occasionally fail to detect illegally typed expressions made up of literal values; such expressions will be rejected by an Ada compiler.
5 The Examiner does not permit the declaration of subprograms in the private part of a package; this limitation will be reviewed in a future Examiner release since the introduction of child packages may make such subprograms useful.
6 The SPARK 95 language definition removes the distinction between initial and later declarative items; this distinction remains in force in the Examiner which requires SPARK 83 declaration orders even in SPARK 95 mode.
7 The Examiner does not yet permit the use of 8-bit characters in SPARK 95 user-defined identifiers.
8 Universal expressions in a modular context may sometimes require type qualification. See Section 3.3 for an example and explanation.
1 Ada string inequality is not modelled.
2 VCs involving string catenation which includes the character ASCII.NUL will be incorrect.
3 Aggregates of multi-dimensional arrays cannot be modelled although aggregates of arrays of arrays can.
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.
6 Recursion in meta files is not detected. If a meta file contains recursive entries the Examiner will loop until it reaches an internal static limit.
7 Recursion in superindex entries is not detected.
This section lists known errors in the Examiner which 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.
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.
3 The Examiner does not check the Ada rule which requires record field names to be distinct.
4 Where a package declares two or more private types the Examiner permits mutual recursion between their definitions in the private part of the package.
5 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.
6 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.
7 The Examiner wrongly demands that a private type that has limited private components must also be limited.
8 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.
9 A string literal still requires type qualification when it is an actual parameter and the formal parameter is a constrained string subtype.
10 Error messages may appear out of position (at the top of the listing file) if a package elaboration part is hidden and there are completeness errors (e.g. a missing subprogram body) to report.
Each Examiner Release is accompanied by a release note detailing changes from the previous version; this section simply summarises the various changes that have been made.
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
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.
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:
§ facilities for proof of programs containing “abstract state”;
§ addition of quantified expressions;
§ proof rule generation for enumeration types;
§ identification of the kind and source of each VC;
§ suppression of trivially true VCs;
§ 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
Release 6.0 of the Examiner should operate with any version of VAX/VMS later than 5.5-2. Previous Examiners, up to and including Release 5.0, have been operated successfully on VMS versions up to and including 7.0.
The Examiner is compatible with Solaris 5.6 through to 8 including those with a 64-bit kernel.
Release 6.0 of the Examiner is compatible with Windows NT 4.0 and Windows 2000. The executables are also known to work on Windows 95 and 98; however, use of the Examiner on these operating systems is unsupported. The FlexLM licence manager software only runs on Windows NT or 2000.
Appendix A. Description of external variables
A.1 Current methods of handling volatility
It is useful to have a reminder of current typical approaches to volatility in order to provide a frame of reference for the new SPARK language features. Typically, a sensor is encapsulated in a SPARK package with an own variable that represents the external source of the data being read from the environment. The own variable may simply be the name of the Ada memory-mapped variable from which the data is being read or, preferably, an abstract own variable with a more descriptive, domain-oriented name. The subprogram that reads the sensor is annotated so that it appears to have a side effect that modifies the sensor itself; this provides the necessary volatility. The conceptual model is that the own variable represents an infinite sequence of future input values. Reading it returns the head of the sequence (i.e. the current value of the sensor) and has the side effect of removing that value from the sequence so that a, potentially, different value may be read next time.
A typical sensor package might look like this:
package Temperature
--# own Inputs; -- own variable representing input data stream
--# initializes Inputs; -- initialized by the environment
is
procedure Read (CurrentTemp : out Integer);
--# global in out Inputs;
--# derives CurrentTemp from Inputs & -- current value
--# Inputs from Inputs; -- side effect
end Temperature;
The annotation providing the side-effect on Temperature.Inputs ensures that the Examiner can correctly model the fact that the sequence of statements:
Temperature.Read (X);
Temperature.Read (Y);
does not necessarily result in X and Y having the same value.
Similar constructions are used for actuators to capture the property that successive writes to an external variable are not ineffective as they would be if it were a simple Ada variable.
A.2 Disadvantages of current approach
Although it is semantically sound and has been widely and successfully used, there are several drawbacks with the current method of handling sensors and actuators. The three principal ones are:
1 It is unintuitive that the annotations for a sensor (which is conceptually an input) show that it is exported by the Read procedure. Similarly it is unintuitive that an actuator should be an import.
2 The body of package Temperatures cannot be analysed without generating flow errors because, at the code level, the simple reading of a memory-mapped port will not show the side effect described by the annotation.
3 When sensors and actuators are used in combinations, the stream side effects start to interact in confusing ways. This often occurs if the reading of a sensor is conditional on the value obtained from some other sensor. Consider a test procedure that reads a pressure sensor only if a previously-read temperature is above a certain level.
procedure Test (Result : out Boolean)
--# global Temperature.Values, Pressure.Values;
--# derives Result from Temperature.Values,
--# Pressure.Values &
--# Temperature.Values
--# from Temperature.Values &
--# Pressure.Values
--# from Pressure.Values,
--# Temperature.Values;
is
Temp, Press : Integer;
begin
Result := False;
Temperature.Read (Temp);
if Temp > TempLimit then
Pressure.Read (Press);
if Press > PressLimit then
Result := True;
end if;
end if;
end Test;
The annotation shows that the result is obtained from both Pressure.Values and Temperature.Values as we would expect. The dependency of Pressure.Values and Temperature.Values on themselves is part of the normal stream model and shows the expected side effect of reading the sensor; however, the dependency (shown in italics) of Pressure.Values on Temperature.Values is both unexpected and confusing.
The introduction of external variables is intended to address all three of these problems and to provide a clean and consistent way of describing the interaction of SPARK programs with their external environment.
A.3 Overview of external variables
The grammar of own variable declarations and of own variable refinement definitions is extended to allow an own variable or constituent to have a mode. Mode in indicates the own variable represents values which are imports to the program from the external environment. Mode out indicates that values assigned to the variable are exported to the external environment. Mode inout is not permitted. The absence of a mode indicates that the own variable is not a system level import or export and behaves as a normal package “state” variable.
Moded own variables, hereafter called external variables for brevity, may not appear in initializes clauses because they are deemed to be initialized by the environment.
There are restrictions on how modes and own variable refinement may be used together; these are described below.
Global and derives annotations involving external variables are written in what might be called a “naive” form; i.e. without an explicitly-annotated side effect. So we write --# derives Value from Sensor; rather than --# derives Value, Sensor from Sensor; Subprogram annotations are also described in more detail below.
In the explanations that follow, external_in means an own variable or refinement constituent with the mode in and external_out one with mode out.
A.4 Package annotations
A.4.1 Grammar
The grammar of own variable clauses is extended, by the addition of mode, thus:
+ own_variable_clause ::=
--# own own_variable_list ;
+ own_variable_list ::= mode own_variable { , mode own_variable }
+ own_variable ::= direct_name
where
mode ::= [ in ] | in out | out
(Note that mode in out is syntactically correct but is prohibited as described later).
This grammar has been chosen to simplify conversion of existing programs; an own variable can be converted to an external variable simply by add either in or out before it.
Similarly, the grammar for refinement clauses is modified thus:
+ refinement_definition ::=
--# own refinement_clause { & refinement_clause } ;
+ refinement_clause ::=
subject is constituent_list
+ subject ::= direct_name
+ constituent_list ::= mode constituent { , mode constituent }
+ constituent ::= [ package_name . ] direct_name
A.4.2 Language rules for packages
The following rules apply to moded own variable declarations in package specifications:
1 Own variables may not be of mode INOUT.
2 Moded own variables may not appear in initializes annotations.
The following rules apply to moded refinement constituents:
1 Refinement constituents may not be of mode INOUT.
2 Refinement constituents of moded own variables must have the same mode as their subject.
3 Refinement constituents of unmoded own variables can have any or no mode (excluding INOUT).
4 Refinement constituents which refine to own variables of private child packages must have the same mode as that given to the own variable in the child package.
5 Own variables of embedded packages which have been announced in a previous refinement clause must have the same mode as was given in that refinement clause.
A.4.3 Initialization
There are two important rules concerning the intialization of external variables. The first concerns what must be initialized and the second what must not be written to or read from during elaboration.
1 Where an abstract own variable appear in an initializes clause, each refinement constituent of it must either be initialized in the package body or have a mode. In other words, all unmoded refinement constituents must be explicitly initialized.
2 Moded own variables or refinement constituents may not be updated or referenced in package elaboration parts nor may they be initialized at declaration. Permitting interaction with external devices in the environment during elaboration would introduce serious and undetectable elaboration order dependencies.
A.4.4 Examples of package annotations
package P
--# own UnModed,
--# in ModeIn,
--# out ModeOut,
--# in out Illegal; -- mode in out not allowed
--# initializes UnModed,
--# ModeIn; -- moded own variable can’t be initialized
is
...
end P;
package body P
--# own ModeIn is in Register1 & -- legal, same mode as subject
--# ModeOut is in Register2 & -- illegal, must be mode out
--# UnModed is in DataPort, -- legal, subject unmoded
--# out AckPort, -- legal, subject unmoded
--# in out BadComponent, -- in out not allowed
--# State; -- legal, subject unmoded
is
...
begin
State := 0; -- only this component requires initialization
end P;
Two principles should help make the rules clear and easy to remember:
1 Refinement is not allowed to change an explicitly given own variable mode.
2 Moded own variables and constituents are regarded as being initialized by the environment prior to the main subprogram running.
A.5 Subprogram annotations
A.5.1 Overview
Subprogram annotations are written in a “naive” fashion that ignores the volatility of the moded own variables that appear in them. The Examiner reconstructs the required volatile behaviour automatically. For example the simple temperature sensor package of Section A.1 simplifies to:
package Temperature
--# own in Inputs; -- own variable representing input data stream
is
procedure Read (CurrentTemp : out Integer);
--# global in Inputs; -- note mode is now in not in out
--# derives CurrentTemp from Inputs; -- naive annotation
end Temperature;
The rules for subprogram annotations are designed to ensure consistency between own variable modes and how those own variables are used in subprograms. This is achieved by requiring that external_in variables may only be imports to subprogram and external_out variables may only be exports. This can be stated more fully as:
1 External_in variables may only have global mode in (if a global mode is given).
2 External_out variables may only have global mode out (if a global mode is given).
3 External_in variables may appear in function global annotations.
4 External_out variables may not appear in function global annotations.
5 External_in variables may only appear as imports in derives annotations.
6 External_out variables may only appear as exports in derives annotations.
The above rules are sufficient where there is no refinement or where the abstract own variables being refined have a mode. Extra rules are required where an abstract own variable without a mode is refined on to constituents that have modes; this is where further checks, to avoid concealed volatility, are required.
A.5.3 Refinement overview
Refinement checks ensure that the abstract and refined annotations of a subprogram are consistent. Where external variables are concerned there are extra rules to ensure that refinement does not conceal volatile behaviour resulting in a mismatch between the abstract and refined descriptions of an operation. It is worth illustrating such concealment with an example:
package Sensor
--# own State; -- no mode
--# initializes State;
is
function Read return Integer;
--# global State;
-- In the abstract view this function has no side effect and returns an
-- invariant value unless State is visibly updated by another subprogram
end Sensor;
package body Sensor
--# own State is in Port; -- legal refinement with mode in
is
Port : ....;
For Port’Address use ...;
function Read return Integer
--# global Port;
is
begin
return Port;
end Read;
-- now the function does have a side effect because Port has a mode
-- so successive reads may return different values.
-- The abstract and refined views are inconsistent.
end Sensor;
This particular example shows a special case where a function (which must not have a side effect) acquires one by stealth. The general way in which concealed external variable side effects are avoided is that the Examiner compares the side effects implied by the refined subprogram annotation with the stated abstract annotation and flags up discrepancies as errors. For example, consider abstract own variable State, with no mode, which is refined on to a mode in constituent Port in the package body. If a refined derives annotation states:
--# derives Value from Port;
then there is an implicit side effect because Port has a mode so we can think of this is as:
--# derives Value, Port from Port;
and, substituting the abstract own variable for the refinement constituent we get:
--# derives Value, State from State;
which is the required abstract annotation. If the abstract annotation differs from this, perhaps because the self-dependency of State was omitted, then a refinement error message will result.
For own variables and constituents without modes the existing refinement rules of SPARK are unchanged. Furthermore, if the abstract own variables have modes, thus forcing any refinement constituents to have the same mode, then the refinement rules are also unchanged. The only case where refinement is affects is where abstract own variables without modes are refined on to constituents that have modes.
A.5.4 Refinement rules
The refinement rules may be stated formally in the form used in the SPARK language definition. Modifications to these rules are shown in italic text. Commentary and explanation is shown [thus].
A.5.4.1 Global refinement
If and only if a subprogram declaration in a package specification has a global definition containing one or more abstract own variables of the package, then the body of the subprogram, which occurs in the package body, shall also have a global definition, called a refinement of the original one.
A refinement G' of a simple global definition [a global definition without any modes] G shall be reducible to G by replacing all constituents of refinement clauses by the subjects of those clauses [and removing an duplicates that result].
A refinement G' of an extended global definition [one with modes] G shall be reducible to G by replacing all constituents of refinement clauses by the subjects of those clauses, and setting the mode of each subject as follows:
1 For each subject whose constituents appear in G’ with two or more different modes, the mode of the subject is set to in out.
2 For each subject whose constituents appear in G’ only with mode out but which have at least one constituent absent from G’, the mode of the subject is set to in out.
3 For each subject which has no own variable mode [note, its own variable mode, not to be confused with its global mode] but a constituent of which does have a mode [again, own variable mode not global mode] and appears in G’, the global mode of the subject is set to in out.
4 Otherwise the mode of the subject is set to the (common) mode of its constituents in G’.
A.5.4.2 Dependency relation (derives) refinement
For a procedure subprogram whose declaration includes a dependency relation, a refinement of a global definition shall be accompanied by a dependency relation, again called a refinement of the original one. A refinement D' of a dependency relation D shall be reducible to D by the successive application of the five following operations. (In this description, the set of constituents of a refinement of an own variable Vi is denoted by C(Vi)).
1 For each export E of D' in turn, if E is a constituent of a refinement of an own variable Vi then for every constituent W in C(Vi) which is not an export of D', a dependency clause with export W and import W is added to D'.
2 If E is a constituent with mode out whose subject does not have a mode, then E is added as an import.
3 For each import I in D’ where I is a refinement constituent of mode in whose subject does not have a mode, add a new dependency clause to D’ showing that I is derived from I.
4 All dependency clauses whose exports belong to the same set of constituents C(Vi) are combined into a single clause, whose export is Vi and whose imports are all the imports of the original clauses.
5 Wherever the imports of a clause include members of a set of constituents C(Vi), these are removed and replaced by Vi.
A.5.5 Converting existing annotations
The effect of these rules can usefully be summarised in terms of the actions required to convert annotations written in current legal SPARK to their external variable equivalent. Assuming we have taken some existing on variables and made them of mode in and made some of them mode out then we can convert an existing derives annotation as follows:
1 Remove all external_in variables which appear as exports.
2 Remove all external_out variables which appear as imports.
3 Convert any remaining clauses of the form:
“derives (nothing) from (something)” to
“derives null from (something)”. (see Section3.2)
A.5.6 Importation of external in variables that are not used to derive any exports
In some cases, we may wish to import and use an external in variable but not derive any export from it. Consider a procedure which reads values from own variable Sensor.Inputs and does not return until a particular value (0 in the example that follows) is found.
Prior to the introduction of external variables such a procedure would take the following form:
procedure BusyWait
--# global Sensor.Inputs;
--# derives Sensor.Inputs from Sensor.Inputs;
is
Val : Integer;
begin
loop
Sensor.Read (Val);
exit when Val = 0;
end loop;
end BusyWait;
If we convert Sensor.Inputs to an external variable with mode in and apply the rule 1 of the previous section then the annotation of BusyWait reduces to:
--# global Sensor.Inputs;
--# derives <nothing> from Sensor.Inputs;
We then apply rule 3 which gives us:
--# global Sensor.Inputs;
--# derives null from Sensor.Inputs;
This notation allows us to follow the SPARK rule that every item that appears in a subprogram’s parameter and global lists must appear somewhere in its derives annotation while making it clear that no export is derived from Sensor.Inputs.
If BusyWait delayed until the value X (rather than the fixed value 0), passed in as a parameter, was received then the derives annotation would be:
--# derives null from Sensor.Inputs, X;
The simplest way of constructing such derives annotations is to construct the main part of the annotation first by identifying each export and the imports from which it is derived. Any parameters or globals that are clearly required but which have not yet been imported can then be placed in a null dependency clause in order to make the annotation complete.
A more complex example can be found at Section A.11.
A.6 Expressions
A.6.1 Use of external variable in expressions
One of the aims of introducing external variables is to allow SPARK Examination of package bodies that deal with input/output, perhaps via memory-mapped variables. The Examiner has therefore been extended to deal with the volatility arising from direct use of external variables in expressions. For example, if InPort is an external_in variable we can write:
X := InPort;
Y := InPort;
without the Examiner concluding that X = Y.
Similarly, if OutPort is an external_out variable then we can write:
OutPort := X;
OutPort := Y;
without the Examiner reporting that the first assignment is “ineffective”.
The following rules apply to the use of external variables in expressions:
1 External_out variables may not be referenced.
2 External_in variables may not be updated.
3 External variables may only appear directly in simple assignment and return statements.
The first two of these are straightforward but the third requires more explanation. The main issue here is one of avoiding ordering effects. To illustrate the problem consider an external_in variable TemperaturePort. If we were to write:
Rising := TemperaturePort < TemperaturePort;
we have created an expression of undefined meaning because nothing in the rules of SPARK determines which side of the inequality expression will be evaluated first. Rule 3 above requires that the expression must be written as follows:
FirstTemp := TemperaturePort;
SecondTemp := TemperaturePort;
Rising := SecondTemp > FirstTemp;
which is free from order dependencies.
Note that this rule also prohibits less harmful cases such as:
Temp := TemperaturePort + 1;
This has been done both for reasons of simplicity in expressing the language rules and because, in practice it is normal to assign input port values directly to a local variable and perform validity checks on the value received before using the value in expressions. See, for example, Section A.9.
A.6.2 Functions which reference external variables
Rule 3 of Section A.5.2 allows functions to reference external_in variables thus:
function CurrentTemperature return Boolean
--# global TemperaturePort;
is
begin
return TemperaturePort;
end CurrentTemperature;
This represents a significant development of SPARK; previously it was never possible to use a function to read an input port because the annotations required to model the volatility of such inputs would result in the function having a side effect and this is strictly prohibited in SPARK.
Although functions can now be used to read external_in variables, the function call itself has to be obey the same rules as direct references to an external variable. In particular, such a function call can only appear directly in an assignment or return statement. Thus we can write:
Temp := CurrentTemperature;
but not
while CurrentTemperature < 100 loop ...
A.7 Miscellaneous additional rules and checks
Since the Examiner treats external variables in special ways to deal with their volatility, it is important that ordinary, non-volatile variables are not wrongly given modes and regarded as being external. To reduce this risk, the Examiner will issue a warning if an external variable is not given an address clause. The warning is considered important and therefore cannot be suppressed using an entry in a warning control file; however, it has not been made a SPARK semantic error because it is possible that particular compilers might provide other means, such as a pragma, to make a variable into an input/output port. Users should take care to provide own variable modes only in those cases where the variable concerned is connected to the external environment by some means.
The Examiner also issues a warning in the opposite case to that described above: where an address clause is found for a variable which is not identified as an external variable. In this case, however, the warning can be suppressed using the warning control file (keyword: address_clauses) because there are other reasons than connection to the environment that might require an address clause.
A.8 Verification Condition (VC) and Path Function (PF) model
The Examiner is capable of constructing a valid model, for VC and PF generation, of statements which use external variables. The main issues here are capturing the volatility involved and ensuring that invalid proofs cannot be constructed.
A.8.1 Procedure call statements
A.8.1.1 Path functions
When a call is made to a procedure that references an external variable, the Examiner reconstructs the information flow relation for the subprogram that would have been required before external variables were introduced and then generates the path functions. The path functions therefore show that the external variable has been “updated” by the read operation thus ensuring that successive reads are seen to return potentially different values.
Give the specification of sensor device:
package Sensor
--# own in Port : Integer;
is
procedure Read (X : out Integer);
--# global in Port;
--# derives X from Port;
end Sensor;
then a single call to Sensor.Read:
procedure ReadOnce (X : out Integer)
--# global in Sensor.Port;
--# derives X from Sensor.Port;
is
begin
Sensor.Read(X);
end ReadOnce;
generates the following path functions:
Statement: start 1 successor(s)
Successor statement: finish.
Path 1
Traversal condition:
1: true .
Action:
sensor__port' := sensor__read__sensor__port(
sensor__port) &
x' := sensor__read__x(sensor__port) .
There are two modelling functions: sensor__read__x models the explicit exporting of parameter X and its derivation from Sensor.Port and sensor__read__sensor__port model the volatility side effect of reading the external variable.
The result of this method is that it not possible to show that successive values read from an external variable are the same. Consider the following procedure.
procedure ReadTwice (TheSame : out Boolean)
--# global in Sensor.Port;
--# derives TheSame from Sensor.Port;
is
X, Y : Integer;
begin
Sensor.Read(X);
Sensor.Read(Y);
TheSame := X = Y;
end ReadTwice;
This produces the following path functions:
Statement: start 1 successor(s)
Successor statement: finish.
Path 1
Traversal condition:
1: true .
Action:
sensor__port' := sensor__read__sensor__port(
sensor__read__sensor__port(sensor__port)) &
thesame' := sensor__read__x(sensor__port) =
sensor__read__x(sensor__read__sensor__port(
sensor__port)) &
x' := sensor__read__x(sensor__port) &
y' := sensor__read__x(sensor__read__sensor__port(
sensor__port)) .
from which it is clear that it cannot be inferred that TheSame has the value True.
A similar approach is taken for modelling procedure calls which update external variables; in this case the effect is to show that successive values are “appended” to the output “stream”.
A.8.1.2 Verification conditions
There are no changes associated with the generation of VCs from calls to procedures which manipulate external variables. The VC model of a procedure call statement already returns discretely numbered variables for successive calls to a procedure so an attempt to prove TheSame is True using the ReadTwice procedure described above produces the unprovable VC:
procedure_readtwice_1.
H1: true .
->
C1: x__1 = y__2 .
The additional “proof attributes” described in the next section may be used to describe postconditions of procedures which manipulate external variables.
A.8.2 Assignment statements
A.8.2.1 Path functions
Modelling of direct use of external variables in assignment statements (including assignments of function call) is achieved using proof attributes. These attributes are implicitly declared for each external variable. They may only appear in SPARK proof annotations and will only be generated in Examiner PF or VC output.
For each external variable Vin of mode in the proof function attribute ‘Tail is declared. The prefix of the attribute is the external variable itself and the argument and return type are the type of the external variable. The attribute describes the volatility side effect of reading the external variable and emphasises the way these variables behave as sequences of future values to be read.
The body of package Sensor, for example, might be written:
package body Sensor
is
Port : Integer;
for Port'Address use ...;
procedure Read (X : out Integer)
is
begin
X := Port;
end Read;
end Sensor;
path functions generated for procedure Read would be:
Statement: start 1 successor(s)
Successor statement: finish.
Path 1
Traversal condition:
1: true .
Action:
port' := port__tail(port) &
x' := port .
which shows the returned value X being obtained from the head of the in port sequence and the sequence itself being replaced by its tail.
Similarly, for each external variable Vout of mode out the proof function attribute ‘Append is declared. This again has a prefix which is the external variable name and its two arguments and return type are the type of the external variable. The first argument of the attribute represents the external variable which is being written to and the second, the value being written. The attribute captures the essential behaviour of external_out variables which is the way each successive write does not destroy the current value of the updated variable but appends another value to the sequence of values being passed to the environment.
Given a simple actuator package and its body:
package Actuator
--# own out Port;
is
procedure Write (X : in Integer);
--# global out Port;
--# derives Port from X;
end Actuator;
package body Actuator
is
Port : Integer;
for Port'Address use ...;
procedure Write (X : in Integer)
is
begin
Port := X;
end Write;
procedure WriteTwice (X, Y : in Integer)
--# global out Port;
--# derives Port from X, Y;
is
begin
Port := X;
Port := Y;
end WriteTwice;
end Actuator;
Then the path functions for procedure Write would be:
Statement: start 1 successor(s)
Successor statement: finish.
Path 1
Traversal condition:
1: true .
Action:
port' := port__append(port, x) .
and those for WriteTwice would be:
Statement: start 1 successor(s)
Successor statement: finish.
Path 1
Traversal condition:
1: true .
Action:
port' := port__append(port__append(port, x), y) .
The PFs for WriteTwice clearly show the sequence of values (X,Y) being written to Port.
A.8.2.2 Verification conditions
The only extension to the generation of verification conditions is that the proof attributes ‘Tail and ‘Append may be used to express postconditions of subprograms which manipulate external variables. Also, since referencing external_in variables implicitly changes them, the ~ operator may be used to assert “the initial value of” the variable.
In may cases it will not be necessary to use the new proof attributes. For example, where only a single, most recent value read from a sensor is significant. In these cases a simpler postcondition which just describes the assignment from the stream will be sufficient. For the Sensor.Read operation described earlier this would just be: --# post X = Port~;
Where multiple reads are involved, a fuller postcondition must be constructed using the proof attribute. For Sensor.Read this would be: --# post X = Port~ and Port = Port'Tail (Port~); With this postcondition in place, attempts to prove that the TheSame exported by ReadTwice has the value True would give the following unprovable VC.
For path(s) from start to finish:
procedure_readtwice_1.
H1: true .
->
C1: port = port__tail(port) .
Since the proof attributes are declared as FDL functions it is possible to make use of user-supplied proof rules about them.
A.9 Run-time checks
The crucial change in run-time check generation is that no assumption is made that a value obtained from an external variable is a valid value of it type. If the user makes this assumption then it will not be possible to complete a proof of exception freedom.
The Examiner issues a warning message where external variables are assigned or returned as a reminder of the importance of validity checking.
Note. The Examiner does not generate run-time exception-freedom checks for Boolean expressions because a well-formed SPARK Boolean expression can never generate a run-time exception. Therefore, if external variables of type Boolean are assigned or returned then it is essential to take heed of the new warning message since this is the only guard against the possible introduction of invalid values to the program.
Given the sensor package:
package Sensor
--# own in Port;
is
type SensorRange is range 1..10;
procedure Read (X : out SensorRange);
--# global in Port;
--# derives X from Port;
end Sensor;
package body Sensor
is
Port : SensorRange;
for Port'Address use ...;
procedure Read (X : out SensorRange)
is
begin
X := Port;
-- although Port and X are of the same type we cannot assume that
-- the value in Port is valid
end Read;
end Sensor;
The unsimplified run-time checks generated for Read are:
For path(s) from start to finish:
procedure_read_1.
H1: true .
->
C1: true .
C2: port >= sensorrange__first .
C3: port <= sensorrange__last .
which, correctly, cannot be proved.
The Examiner does take note of the fact that Ada does not require a constraint check for an assignment between identical subtypes so it is possible, in SPARK 95, to use a local variable and the ‘Valid attribute to validate an input data item. For example, the body of procedure Read could be rewritten thus:
procedure Read (X : out SensorRange)
is
Local : SensorRange;
begin
Local := Port; -- no constraint check because subtypes are same
if Local'Valid then
X := Local;
else
-- return default value
X := SensorRange'First;
end if;
end Read;
This gives the richer set of VCs:
For path(s) from start to run-time check associated with statement of line 156:
procedure_read_1.
H1: true .
H2: sensorrange__valid(port) .
->
C1: port >= sensorrange__first .
C2: port <= sensorrange__last .
For path(s) from start to run-time check associated with statement of line 159:
procedure_read_2.
H1: true .
H2: not (sensorrange__valid(port)) .
->
C1: sensorrange__first >= sensorrange__first .
C2: sensorrange__first <= sensorrange__last .
For path(s) from start to finish:
procedure_read_3.
H1: true .
H2: sensorrange__valid(port) .
H3: port >= sensorrange__first .
H4: port <= sensorrange__last .
->
C1: true .
C2: port >= sensorrange__first .
C3: port <= sensorrange__last .
procedure_read_4.
H1: true .
H2: not (sensorrange__valid(port)) .
H3: sensorrange__first >= sensorrange__first .
H4: sensorrange__first <= sensorrange__last .
->
C1: true .
C2: sensorrange__first >= sensorrange__first .
C3: sensorrange__first <= sensorrange__last .
The last 3 VCs are directly provable and the first is also provable given the defined semantics of the ‘Valid attribute.
For SPARK 83 users, an alternative to ‘Valid is to read sensor values into a type which guarantees that any bit pattern received from the external variable is a valid value and then perform explicit range checks. The previous example can be recast as:
package Sensor
--# own in Port;
is
type SensorRange is range 1..10;
procedure Read (X : out SensorRange);
--# global in Port;
--# derives X from Port;
end Sensor;
package body Sensor
is
type Word is range 0 .. 65535;
-- type chosen so that any bit pattern is a valid value
Port : Word;
for Port'Address use ...;
procedure Read (X : out SensorRange)
is
Local : Word;
begin
Local := Port;
if Local <= Word (SensorRange'Last) and
Local >= Word (SensorRange'First) then
X := SensorRange (Local);
else
--return default value
X := SensorRange'First;
end if;
end Read;
end Sensor;
This again results in a provable set of run-time check VCs.
We are considering ways in which the proof model of external variables can be enriched. In particular we are seeking ways of allowing reasoning about multiple reads of external_in variables. The intention is to make it possible to express postconditions for operations of a kind illustrated by the informal specification: “read the input until three successive identical values are seen and return that value”. The informal postcondition might be: “there exists a sequence of three identical values in the input sequence and the returned value is equal to them and the input sequence has had N values consumed”. The proof attributes described above are not expressive enough for this purpose.
A.11 Example
The following example uses external variables and refinement to describe and implement a complex input/output device. The device has internal state that records the last value sent to it. Its behaviour when value is written is as follows:
if value = last value sent then
do nothing
else
store value in last value
write value to out register
busy wait until ack received at status port.
The abstract specification of the device is:
package Device
--# own State; -- represents all registers, ports and values
--# initializes State;
is
procedure Write (X : in Integer);
--# global in out State;
--# derives State from State, X;
end Device;
And its body:
package body Device
--# own State is OldX,
--# in StatusPort,
--# out Register;
is
OldX : Integer := 0; -- only component that needs initialization
StatusPort : Integer;
for StatusPort’Address use .........;
Register : Integer;
for Register’Address use ..........;
procedure WriteReg (X : in Integer)
--# global out Register;
--# derives Register from X;
is
begin
Register := X;
end WriteReg;
procedure ReadAck (OK : out Boolean)
--# global in StatusPort;
--# derives OK from StatusPort;
is
RawValue : Integer;
begin
RawValue := StatusPort; -- only assignment is allowed here
OK := RawValue = 16#FFFF_FFFF#; -- ack value
end ReadAck;
procedure Write (X : in Integer)
--# global in out OldX;
--# out Register;
--# in StatusPort;
--# derives OldX,
--# Register from OldX, X &
--# null from StatusPort; -- see A.5.6
is
OK : Boolean;
begin
if X /= OldX then
OldX := X;
WriteReg (X);
loop
ReadAck (OK);
exit when OK;
end loop;
end if;
end Write;
end Device;
The body can be examined and is error free; this is a significant advance over previous Examiner versions where it is likely that the entire package body would have to have been hidden.
Document Control and References
Praxis Critical Systems Limited, 20 Manvers Street, Bath BA1 1PX, UK.
Copyright Praxis Critical Systems Limited 2001. All rights reserved.
Issue 0.1 (26th June 2001): First draft, based on interim Release Note 73_77.doc
Issue 0.2 (12th July 2001): Added “derives null from ...”
Issue 0.3 (13th July 2001): Started on manual change summary and operating system compatibility
Issue 0.4 (20th July 2001): New predefined types
Issue 0.5 (25th July 2001): Modular types
Issue 0.6 (9th August 2001): After initial review comments by jarh
Issue 0.7 (24th August 2001): Added material describing plain_output switch (section 4.3) and improved error messages (section 5.6).
Issue 0.8 (23rd October 2001): Added material on SPARKSimp tool and SPADE Simplifier 2.0 release. Changed paper size to US Letter.
Issue 1.0 (7th November 2001): After review.
None.
CVSROOT/userdocs/Examiner_RN_6.doc
[1] Note: The SPARK programming language is not sponsored by or affiliated with SPARC International Inc. and is not based on SPARC™ architecture.