This manual explains the process of generating verification conditions for SPARK programs together with their format, interpretation and proof. Details of the use of the Examiner, Simplifier, Proof Checker and POGS are described in their respective user manuals [1, 2, 4, 5].
The structure of the remainder of this document is as follows.
Chapter 2 introduces the concepts of:
· formal verification,
· proof contexts,
· the form and generation of verification conditions (VCs), and
· refinement proofs.
Chapter 3 explains what the various SPARK proof contexts are used for, as well as defining their syntax and placement in SPARK code.
Chapter 4 describes the extended form of the part of the FDL modelling language used for expressing VCs.
Chapter 5 provides detailed examples of the process employed by the Examiner to generate VCs showing the (partial) correctness, with respect to its formal specification, of a piece of SPARK code.
Chapter 6 discusses the VCs that are associated with run-time checks (including intermediate expression overflows) and looks at various strategies for eliminating run-time errors.
Chapter 7 covers certain assumptions and limitations that can affect the validity of a SPARK proof.
Chapter 8 defines the mapping of SPARK language constructs into the FDL employed by VC generation. This includes the generation of refinement integrity VCs for reasoning about abstract own variables.
Chapter 9 includes guidance on the process of annotating SPARK code and proving it correct (wrt the annotations).
Chapter 10 gives examples of SPARK code, their specifications and correctness VCs.
Readers new to formal verification may like to start with Chapters 2, 5, 9 and 10, referring to Chapters 3, 4, 6, 7 and 8 for technical details, as required.
Readers using this document for reference should consult Chapters 3, 4, 6, 7 and 8, depending on whether they are looking for material on SPARK proof contexts, FDL, or the conversion of SPARK into FDL.
Given a formal specification of the functional requirements of a subprogram, expressed as a precondition and a postcondition, we can attempt to prove that the subprogram meets its specification; this is called formal verification.
· The precondition is a predicate which expresses a constraint on the imported variables of the subprogram (eg that a scalar import is in a certain range, that an array is ordered, or perhaps some more complex properties).
· The postcondition is a predicate which expresses a relation between the initial values of imported variables and the final values of exported variables of the subprogram. (Where a variable is both imported and exported, we require some notation to distinguish its initial and final state in the postcondition.)
In software for an embedded system, the imports used in the precondition are typically values read from sensors together with historic values forming part of the state, while the exports appearing in the postcondition are values to be transmitted to the outside world, for example via actuators.
A common, though risky, laxity is to say that a piece of software has been “formally verified” or “proved correct.” This laxity makes such claims meaningless: one must always be careful to state what one has proved about a piece of software, or against which specification it has been verified.
The specification used may itself be expressed either informally, as a natural language document, for instance, or formally, in a suitable notation. In either case, though particularly in the former, care must be taken to ensure that interpretation of the specification does not compromise the proof, by introducing unjustified assumptions for instance.
What is generally understood by proof of correctness (with respect to a specification) is a proof of partial correctness: that if the precondition is met on entry to the program and it terminates (without a run-time error occurring during execution), then the postcondition will hold on exit.
Proof of termination in general involves providing suitable metrics for each loop; these are typically integer expressions, which are strictly monotonically increasing (or decreasing) and bounded above (below). The Examiner does not, at present, provide automatic support for the generation of proof obligations to prove the validity of such metrics.
If we establish both partial correctness (wrt a specification) and termination, we are generally said to have achieved a proof of total correctness. Even a proof of total correctness may omit to establish the absence of certain errors which may arise in execution, and which may therefore compromise the validity of a proof if care is not taken. For example, if division is used in the code, we must ensure that the implicit precondition (which is present in most programming languages) for such an operation, namely that the divisor is non-zero (or even, for “real” arithmetic, that the divisor is not too small), is established for all possible executions of the program.
We refer to these potential errors as run-time errors. The verification conditions for the proof of absence of run-time errors can be generated automatically by the Examiner see section 6.
In SPARK, pre- and postconditions are expressed as annotations called proof contexts. Unlike the core annotations of SPARK (such as global), proof contexts are optional annotations, and are written in an expression language which is an extension of Ada's. Within subprogram bodies, additional proof contexts are used for:
· code cutpoints (eg loop invariants) via assert statements;
· well-formation checks, via check statements.
We can also declare proof functions (for use in annotations as mathematical functions which we define by means of a collection of proof rules), proof types, and type assertions. These are described in section 3.3.
Each proof context is associated with a particular location in the code:
· the precondition is associated with the begin of the procedure (or function) body;
· the postcondition of a procedure (or the return annotation of a function) is associated with the end P; of the subprogram body; and
· each assert or check statement in the code is located at a point in between two executable statements, in general, ie it is associated with a point on the arc of the flowchart of the subprogram which passes between the two statements it appears between. Each such assertion specifies a relation between program variables which must hold at that precise point, whenever execution reaches it. Assert statements generate a cut point on the flowchart of the subprogram, check statements do not.
2.3 The origin of proof annotations
Ideally, the contents of proof contexts should be derived from a formal specification (e.g. in Z). Even in such a case, however, the annotations present in an implementation will differ from those in a specification in that they will be expressed in terms of concrete data types (e.g. arrays) rather than abstract ones (e.g. sequences). There will also be notational differences: a Z convention in specifying an operation, for instance, is to use x' for the value of x after the operation, while in SPARK a tilde (x~) is used to decorate the initial value of an imported, exported variable (apart from in the precondition, where all values are initial). The specification may be used to suggest proof functions and rule definitions to use.
Where specifications are less rigorous great care will be needed to obtain meaningful proof contexts. If a specification is too weak or ambiguous we may prove the code against it but fail in the process to prove the intended properties of the code. For example, consider the following formally-expressed but ambiguous specification:
Suppose array B(1..n) is to be A(1..n) sorted into order; let
same_elements(A, B) º " i Î 1..n, $ j Î 1..n · A(i) = B(j)
This specification ignores duplication, eg
if A(1)=1, A(2)=2, A(3)=1
then B(1)=1, B(2)=2, B(3)=3
would satisfy the above same_elements relation: the specification is too weak. We need the idea of an exact permutation to allow for arrays which contain repeated elements.
2.4 Examiner switches and output files
2.4.1 Command line switches
The Examiner’s command line switches are described in the
Examiner User Manual [1]. The main switches of relevance to proof are:
|
Option |
Description |
|
-vcg |
Generates all VCs, including those for numeric overflow and real numbers. |
|
-rules |
This option defines the policy applied by the Examiner to replacement rule generation for composite constants. |
|
-debug |
There are various debug options of relevance to proof, most significantly: i – Print default loop invariants (in FDL) as they are generated. v – Print VCG state and BPG after DAG.BuildGraph. V – as v, but also print BPG during each iteration of VC Generation. |
|
-dpc |
Generate Dead Path Conjecture (.dpc) files for input to ZombieScope [7]. |
|
-fdl |
Controls the Examiner’s treatment of FDL reserved words. |
2.4.2 Output files
Output files are generated for each subprogram which is free of SPARK semantic errors. The file names and locations are obtained from the subprogram name and location as described in [1]. Three files are produced for each subprogram as follows.
2.4.2.1 Verification conditions
The verification conditions are contained in files with the extension .vcg. The form and significance of these VCs is described in section 2.7. Typically the number of VCs generated will be quite large with at least one for every statement in the subprogram; however, they are usually quite simple in form and will be reduced extensively by the Simplifier. It is usually not worth expending much effort in manual interpretation of the unsimplified VC output. The validity of the VCs generated depends on some important assumptions, principally that the SPARK source is free from data flow errors; these are described in section 7.1. Note that it is not a requirement that the program is free from information flow errors in the form of reported mismatches between the calculated information flow and that specified in the dependency or derives relation.
The Simplifier and Checker require some type information for the entities in the VC file. These declarations are contained in a file with the extension .fdl. It should not be necessary manually to interpret this file.
The Simplifier is capable of reading and using a file of proof rules during the simplification process. A proof rule states some property which may be assumed, for example, that a constant has a particular numeric value or that a type has particular bounds. A standard set of rules are generated automatically by the Examiner using information from declarations in the SPARK source and placed in a file with the extension .rls. The automatically generated rule file should not be edited and will be overwritten each time the Examiner is applied to the source text.
The Simplifier User Manual [2] describes the use of user-defined proof rules that can be written to supplement the automatically generated rules.
The Examiner can generate Dead Path Conjecture (.dpc) files for analysis by the ZombieScope tool. One file is generated per subprogram analysed by the Examiner, with each file containing one DPC (similar to VC) for each path through the code. ZombieScope processes these files and attempts to find dead paths in the SPARK source code by finding contradictions in their traversal conditions. For more details see the ZombieScope User Manual [7].
2.5 Generating verification conditions
To establish the correctness of a fragment of code, we must prove that, if the procedure (or function) is invoked in a state which satisfies the precondition, then the postcondition is satisfied on reaching the exit from the code. (Note that we regard the postcondition of a function subprogram to be that the value returned by the code is equal to that specified in its return proof context.) A verification condition (VC) is a formula for the correctness of a particular path between two cutpoints — the precondition, the postcondition and any other assert annotations present in the body of the code. To generate the VC associated with a particular path between two assertions, we hoist the assertion step by step from the end of the path up to the top.
There are only two sorts of statement which are relevant to the hoisting process:
· an assignment statement (... := ...); and
· a conditional statement (if/case/exit when).
All other statements can be modelled via these two forms; for example:
· a procedure call can be regarded as performing a collection of simultaneous assignments to the exported variables of the procedure; and
· a loop can be defined implicitly via recursion; for the loop L:
while e loop S; end loop;
we can see, for example, that:
L if e then S; L; end if;
For the annotated code fragment:
the assertion at point A which is sufficient to guarantee that the assertion P(...,V,...) (containing instances of variable V and other variables) is always true at point B is P(...,e,...), ie the assertion with all instances of variable V replaced by expression e. For example,
For the annotated code fragment:
the assertion at point A which is sufficient to guarantee that assertion P is always true at point B is e P. Suppose we know that e P is true at point A, for instance, and execution of the code reaches point B, so we also know that e is true. Then these two formulae e, e P together imply P, as we require to establish P at point B.
2.5.3 The weakest precondition of an assertion
This method allows us to deduce the weakest precondition — WP — at a given point for an assertion at another point in the code. We can hoist the assertion successively up the code to reach another assertion in the code; if the assertion at the top of the path implies the weakest precondition at that point of the assertion at the bottom of the path, we have proved the correctness of the path wrt the specification.
We call the formula for the correctness of a path between two assertions a verification condition (VC), as noted earlier.
To prove the correctness of the code of an entire procedure, we must prove the correctness of each path between two assertions (and that any subprograms called by the procedure are themselves also correct wrt their specifications). Given the necessary code annotations, the generation of VCs is itself an entirely mechanical process; in general, proving these formulae is not as automatic, however.
It is worth noting that the proof of partial correctness of a subprogram establishes that the exported values returned by it will satisfy the postcondition relation if the subprogram is called with imported values which satisfy its precondition: it says nothing about how the subprogram might behave if it is called with imported values which do not satisfy the precondition. Proof that the subprogram is always invoked with imported values which do indeed satisfy its precondition must be performed in the calling environment. This is as it should be: if we write a routine to calculate a square root of a non-negative number, for instance, we must show that wherever it is invoked it is used appropriately, and this can only be done by considering each such invocation in the appropriate context.
The generation of VCs requires that all cyclic paths are cut with a suitable loop-invariant assertion. Because run-time checks can be generated from SPARK code without the use of additional annotations the Examiner may encounter an uncut cyclic path. To enable the generation of VCs to continue, the Examiner will choose a suitable location in the loop and insert a default assertion. When this occurs the Examiner issues a warning (which is included in the listing file as usual) as follows:
--- Default assertion planted to cut loop.
To see the contents of such default assertions use the debug=i switch (see section 2.4).
Assertions planted within the body of a loop need to provide some relation between the variables being modified in the body of the loop. Frequently, they may also need to carry forward other invariant information; for example, if variable x is both imported and exported, but it is not modified within the body of loop L, then the loop-invariant for L will need to carry forward the assertion x = x~ (or some other relation) to make the relationship between the initial and final (or so-far) value of x available to subsequent assertions, including the postcondition. Often, one also needs to place bounds on scalars which are modified within loop bodies, and to record how the loop is working incrementally towards satisfying other assertions (such as the postcondition) which follow it. Ideally, loop-invariants should be written at the same time as the loop is coded, since the author of the detailed code should be the person with the best understanding of the behaviour of the loop.
For example, consider a very simple natural number division algorithm, for a processor which doesn't provide a divide instruction; we suppose it is to return a quotient Q and remainder R for M divided by N.
The postcondition which a loop to calculate these will need to establish is:
M = Q * N + R and 0 <= R < N
(The range constraint on R is necessary to ensure that it is the lowest remainder satisfying the relation.) One way of satisfying the first clause of the postcondition is to note that if we choose Q = 0 and R = M, then the relation is satisfied. This does not in general satisfy the range constraint on R, however. To achieve this, one approach is to look for a succession of values for R, getting smaller with each iteration and ending with the right one. If we decrease R, we will need to increase Q to offset this; yet if Q gets bigger by 1, R needs to decrease by N to preserve the desired relation. This suggests a loop body:
Q := Q + 1; R := R - N;
which satisfies the relation M = Q * N + R on each successive iteration of the loop, provided it is true on entry to the loop body. Finally, we note that we must exit from this loop body as soon as R < N is achieved, and that if we do so, we can ensure R >= 0 is preserved throughout execution of the loop body, provided it is true on entry to the loop.
2.7 The form of verification conditions
Each verification condition generated by the Examiner has the following form:
H1: ....
H2: ....
....
->
C1: ....
....
Each Hi is a hypothesis.
Each Ci is a conclusion.
The formula represents:
(H1 H2 ...) -> (C1 ...)
The hypotheses are derived from the assertion at the head of the path and the path traversal condition and the conclusions are derived from the assertion at the end of the path (suitably transformed).
To prove a VC, we can assume that the hypotheses are true and demonstrate that the conclusions follow from them. We must prove all of the VCs associated with a subprogram to establish the correctness of the code with respect to its specification.
In proving a subprogram P which calls another subprogram Q, in the proof of correctness of P we assume the correctness of the subprogram Q. If we find subsequently that Q does not satisfy its specification, then:
· if we only need to modify the body of Q to correct the error, the proof of the correctness of P is not affected; but
· if we have to modify the specification (ie the precondition and/or the postcondition) of Q, we must re-establish the correctness of P to ensure Q's precondition is met when called and that the assumption of Q's postcondition is sufficient to allow the proof of P's correctness.
2.7.1 Simplification and proof of verification conditions
Verification conditions can be quite large formulae for non-trivial programs; consequently, pencil-and-paper proofs carry a large risk of error; for this reason, automated proof support tools are essential in practice. We can make a number of observations, however:
· The larger and/or more complex the program, the larger the number of VCs and the greater their complexity, in general.
· Procedural decomposition and self-containment helps to reduce the number and size of VCs.
· Many VCs contain a number of trivial components, which can be eliminated by automatic simplification.
· We must strike the right balance in our annotations to achieve VCs that can be proved as simply as possible.
· Tool support for simplification and proof are provided by the Simplifier, the Proof Checker and the Proof Obligation Summariser (POGS). The Simplifier deals effectively with most verification conditions, allowing effort to be concentrated on the more challenging ones. The Proof Checker is an interactive assistant that aids in the construction of proofs, prevents the construction of erroneous proofs and provides an audit trail of the proof work undertaken. Finally, the POGS tool helps with the management of proof work by providing a summary of VCs, indicating their source and current proof status. For further details of the use of these tools, refer to the user manuals [2, 3, 4, 5].
2.8 An introduction to refinement proofs
This section provides a basic introduction to refinement proofs involving abstract own variables or private types. It includes only sufficient explanation of refinement to describe the facilities currently supported by the Examiner. Any reader interested in a more comprehensive treatment of formal refinement should consult an appropriate textbook. As refinement is a more advanced proof concept, new readers may choose to skip this section if they are not interested in proofs involving abstract own variables or the refinement of private types.
2.8.1 SPARK refinement
SPARK supports two distinct forms of refinement.
1. Own variable refinement in flow analysis.
2. Using pre- and postconditions, or return annotations, to specify subprogram behaviour.
In both types of refinement[1] the fundamental purpose is to be able to hide or ignore detail that is unnecessary for the analysis being performed.
With own variable refinement in flow analysis an abstract (SPARK) own variable represents a set of concrete (Ada) variables used in the bodies of subprograms.
In the case of pre- and postconditions etc. the refinement arises because a formal specification defines only the end effect of a subprogram and not the detail of any algorithms used to achieve that effect.
The hiding of unnecessary detail in refinement is beneficial because it can lead to:
· simpler specifications that are easier to understand and review;
· reduced maintenance, both through less material to maintain and material being less sensitive to changes in implementation detail;
· decreased coupling between program units, as changes in one unit are less likely to require changes in another.
However, for any refinement to be valid it must be established that the specification, although less detailed, is consistent with the actual implementation behaviour.
SPARK provides facilities to reason about own variable refinement in program proof. That is, to specify the behaviour of subprograms (using pre- and postconditions or return annotations) in terms of abstract SPARK own variables and prove that the specifications are consistent with the Ada implementations of the subprograms.
2.8.2 Abstract and concrete views
Clearly for refinement to exist there must be two separate descriptions or views of behaviour, one of which ‘refines’ (i.e. in some sense provides more detail than) the other. We use the term abstract to refer to the less detailed view and the term concrete to refer to the more detailed view.
In the case of information flow analysis using abstract (i.e. non-Ada) own variables:
· the abstract view of information flow is the derives annotation in a package specification;
· whereas the concrete view is the derives annotation in the package body.
With proofs of functional behaviour:
· the abstract view consists of pre- and postconditions (or return annotations);
· the concrete view is the corresponding Ada code.
Note that the concrete view in one refinement may also be the abstract view in another refinement. For example, a package’s abstract own variable may be refined by variables that are themselves abstract (from child or embedded packages).
Where private types are used, the abstract view is the external one where the implementation details of the private type are concealed and the refined one, within the body of the package that declares the type, is where the implementation details are known.
To show that a refinement is valid it must be established that the abstract and concrete views are consistent. In essence this means that the concrete view can only add detail to the abstract view, everything stated in the abstract view must still be true in the concrete view.
Where private types are processed by a subprogram, the variables manipulated in the abstract and concrete view are the same but the concrete view provides a richer set of operations to describe the subprogram’s behaviour.
With own variable refinement[2] the abstract and concrete views actually refer to different variables. So to check that the views are consistent requires a definition of how the abstract and concrete variables relate to each other. We call this relationship the abstraction relation.[3]
For example, with flow analysis involving own variable refinement the abstraction relation is provided by the ‘--# own’ annotation in the package body (which lists the concrete variables that the abstract own variable represents).
2.8.4 Refinement verification conditions
For flow analysis, establishing the validity of a refinement is completely automated by the Examiner. However, establishing the validity of refinement involving proof annotations requires the generation of verification conditions (VCs). In this section we briefly describe the VCs that are generated when proving the correctness of own variable and private type refinement.
As with flow analysis, involving abstract own variables, proof requires two separate sets of annotations:
· an abstract specification of a subprogram's behaviour in a package specification (that refers to abstract own variables or a type’s private view);
· a concrete specification in the package body (that does not refer to the abstract own variables given in the package specification).
From these annotations two VCs are generated to establish the validity of the refinement:
· to show the consistency of any abstract and concrete preconditions;
· to show the consistency of any abstract and concrete postconditions or return annotations.
Each of these VCs is briefly described below.
2.8.4.1 Precondition VC
The fundamental condition for an abstract and concrete precondition to be consistent is that whenever the abstract precondition holds then so does the concrete. That is, the concrete precondition is true if the abstract precondition is.[4] The concrete precondition is said to be weaker than the abstract precondition.
This condition is necessary as only the abstract precondition of a subprogram is visible to any callers external to the subprogram’s package. VCs of such external callers therefore establish the abstract precondition. However, the body of the called subprogram is proved correct with respect to the concrete precondition. So if the abstract precondition does not guarantee that the concrete precondition of the called subprogram is met, then the caller may be proved correct despite the fact that the execution of the called subprogram may fail.
2.8.4.2 Postcondition VC
Fundamentally an abstract and concrete postcondition are consistent if whenever the concrete postcondition is true then so is the abstract.[5] The concrete postcondition is said to be stronger than the abstract postcondition.
This condition is necessary as only the abstract postcondition of a subprogram is visible to any callers external to the subprogram’s package. VCs of such external callers therefore assume the abstract postcondition. However, the body of the called subprogram is proved correct with respect to the concrete postcondition. So if the concrete postcondition does not guarantee that the abstract precondition of the called subprogram is met, then the caller may be proved correct despite the fact that the execution of the called subprogram does not achieve what the caller assumes.
The VC for the consistency of return annotations is similar. (For details see section 8.6.5.)
2.8.5 Overview of refinement proof facilities
2.8.5.1 Own variable refinement
SPARK and the Examiner support refinement proofs involving an abstract own variable as follows.
1 The abstract own variable is type announced in its package specification.
2 The type used in the announcement must be a unique abstract type (declared using a SPARK annotation for proof types). Such a type is only visible in SPARK proof contexts (ie there is no corresponding Ada type).
3 External to the package the Examiner treats the abstract type as if it is a private Ada type (and hence only equality comparisons are possible).
4 Properties of the abstract own variable have to be expressed using proof functions.
5 Public subprograms in the abstract own variable's package, which import and/or export the own variable, have two sets of proof annotations: an abstract set in the package specification and a concrete set in the package body.
6 For VC generation internal to the package the Examiner has a built-in abstraction relation – namely the abstract type is modelled as a record type with one field for each of the concrete own variables that the abstract variable is refined to.
7 For each subprogram described in item 5 above, two additional VCs are generated by the Examiner to ensure that:
· the abstract precondition is not weaker than the concrete precondition;
· the concrete postcondition is not weaker than the abstract postcondition (or that the return annotations are consistent);
and hence formally prove that the refinement is valid.
2.8.5.2 Private type refinement
SPARK and the Examiner support refinement proofs involving a variable of a private type as follows.
1 Public subprograms in the private type’s package, which import and/or export the variables of the private type, have two sets of proof annotations: an abstract set in the package specification and a concrete set in the package body.
2 In the abstract annotation, where the type’s implementation is not known, properties of the variable have to be expressed using proof functions.
3 In the concrete annotation, internal to the package, the private type’s implementation details are known and the appropriate operators, selectors and functions can be used.
4 For each subprogram described in item 1 above, two additional VCs are generated by the Examiner to ensure that:
· the abstract precondition is not weaker than the concrete precondition;
· the concrete postcondition is not weaker than the abstract postcondition (or that the return annotations are consistent);
and hence formally prove that the refinement is valid.
2.9 Behavioural Subtyping and Extended Tagged Types
SPARK permits the use of tagged types and type extensions. Extended types may inherit operations from their ancestor, root types. An important principle in the use of such type extensions is that each extended type should be a behavioural subtype of its ancestor type; this is known as the Liskov-Wing substitution principle[6]. Given an extended type E which is derived from an ancestor tagged type T, then the principle requires that for each primitive operation P of E and T:
pre (PT) pre(PE) and post(PE) post (PT)
Or, in English, an operation on an extended type must require less and promise more than the primitive operation it overrides.
The Examiner generates VCs to show that the substitution principle is respected. These are indicated in the VC file with the title “For checks of subclass inheritance integrity”. An example can be found at Section 10.8. Note that the Examiner does not require the pre and post conditions of the extended operation to be written in a particular or special form (for example, or-ed with its original precondition and and-ed with its original postcondition) provided that the generated VCs can be shown to be true.
The Examiner provides support for extensions to SPARK which include the “Ravenscar Tasking Profile”. These extensions are known as “RavenSPARK” and are described fully in the manual “The SPARK Ravenscar Profile”. RavenSPARK allows the construction of programs comprising a fixed set of tasks, protected objects and interrupt handlers. To avoid the possibility of constructing invalid proofs the Examiner prohibits the use of shared variables (i.e. protected variables that may be accessed by more than one program thread) in constraints and proof statements (as described in Sections 3.4 and 3.5).
SPARK Proof Contexts are annotations which are not mandatory annotations of the SPARK language but which are extensions to it for formal verification purposes, and are recognised by the Examiner. They are the means by which we introduce the preconditions, postconditions and assertions described earlier into a SPARK program text.
SPARK proof contexts are of three kinds:
Subprogram constraints. These are annotations specifying pre- and postconditions of procedures and preconditions and return values of functions.
Proof statements. These are employed within the body of a subprogram to specify cut points (eg loop-invariants) via an assert statement, or to introduce other kinds of proof obligations (such as range constraints) via check statements.
Proof declarations. The formal specification of a program unit can often conveniently be expressed in terms of proof functions (as opposed to SPARK function subprograms) with well-defined properties (which may be specified in the form of re-write rules, for use with the Proof Checker). The declaration of such functions in a SPARK program text makes it possible to refer to them in subsequent proof contexts. If refinement VCs involving abstract own variables are to be generated, then SPARK abstract proof types must be declared to represent the types of the abstract own variables. Finally, a type assertion may be used to specify the implementation-defined base-type of a signed integer or floating point type declaration.
The syntax rules of SPARK prescribe the places where proof contexts may appear. The following sections describe the use of the three kinds of proof contexts in more detail.
3.2 The language of proof contexts
The language used to write expressions in subprogram constraints and proof statements is the language of SPARK expressions with the following extensions:
· logical implication;
· structured object update expressions;
· quantified expressions;
· the application of proof functions; and
· decorations to denote the initial values of variables which are both imported and exported.
To assist in writing the Boolean-valued expressions used in proof contexts SPARK is extended, in such contexts, to include the logical implies (->) and equivalence (<->) operators. For example:
X(J) = 3 <-> B.
(Note that implication and equivalence bind less tightly than equality.)
Although it is possible to use alternatives to implication and equivalence, their use is recommended since the Simplifier and Proof Checker are better able to simplify Boolean expressions of this form.
3.2.2 Structured object update expressions
When one or more components of a structured variable are updated this cannot be represented with a single, simple SPARK expression. For this reason, SPARK in proof contexts is extended to support the description of such updating. An update takes the form of the name of a record or array followed by one or more override expressions in square brackets. The override expressions show which components of the record or array are being overwritten and with which values. Components which do not appear in the list of override expressions retain their original values.
update ::= name [ override { ; override } ]
override ::= expression { , expression } => expression
3.2.2.1 Record updates
Record updates take the form R[N => C; M => D] where R is the name of a record, N and M are the names of fields in R and C and D are expressions whose types are the same as fields N and M, respectively of R. The update expressions can be read as record R with the value of field N replaced by C and the value of field M replaced by D (with other fields remaining unchanged).
3.2.2.2 Array updates
Array update expressions are similar to those for records except that the field names are replaced by expressions of the index type of the array indicating which elements of the array are being updated. For example: A[3 => 5; J+1 => 0; J-1 => X + Y], which represents array A but with elements 3, J+1 and J-1 (in turn) overwritten by the values of the expressions shown. Update expressions can be written for multi-dimensional arrays by including the index expressions for each dimension of the array to the left of the arrow symbol. For example A[1,1 => 0; 2,2 => 1] to update elements (1,1) and (2,2).
3.2.2.3 Updates as names
The sequence of override expressions in the square brackets of an update expression are read from left to right. Update expressions are considered to be names in the grammar so they may be used as a prefix to a further update expression. Thus V[O;P] and V[O][P] are equivalent in meaning. Similarly an update expression can be indexed into or selected from, in order to read the value of a component of the expression, eg A[1 => 2](1) (which has the value 2) or R[F1 => 2].F1 (which also reduces to 2). When VCs are generated from expressions involving update expressions they are modelled in FDL using element and update in the case of arrays and upf_ and fld_ functions in the case of records.
It is often necessary to express constraints about array data structures and quantified expressions are a convenient way of doing this. Quantified expressions are a kind of predicate and their syntax is:
quantified_expression ::= quantifier_kind defining_identifier in discrete_subtype_mark
[ range range ] => ( predicate );
quantifier_kind ::= for all | for some
This syntax has been chosen to be as similar as possible as that for for loops and should thus be familiar to SPARK programmers. The grammar term identifier is a user-chosen name for the quantified variable; this, as is also the case for for loop control variables, must not already be visible. The quantified variable has a scope that extends only to the end of the quantified expression so a quantified variable may be re-used in later expressions. If an explicit range is given, then the given subtype_mark must not be Boolean or a subtype of Boolean.
The keywords ‘for all’ denote a universal (") quantification, ie the whole quantified expression is true if, and only if, the predicate part of the quantifier is true for every value of the quantified variable in the defined type and range. The keywords ‘for some’ denote an existential ($) quantification, ie the whole quantified expression is true if, and only if, the predicate part of the quantifier is true for at least one value of the quantified variable in the defined type and range. Quantifiers can be nested, ie the predicate part of one quantified expression can include another quantified expression.
As an example consider an array of type Table that may, or may not, contain some sought value. We can express the return condition of a function that reports whether or not the sought value is present thus:
function ValuePresent(A : Table;
Sought : Integer) return Boolean;
--# return for some M in Index => ( A(M) = Sought );
A more complex example is a function that, given that Sought does appear somewhere in the table, returns the index of first occurrence of it. The precondition of the function ensures that it is only called if Sought is definitely present and the postcondition uses the implicit form of function return annotations, together with a quantifier to capture the property that the first occurrence of Sought is returned.
function FindSought(A : Table;
Sought : Integer) return Index;
--# pre for some M in Index => ( A(M) = Sought );
--# return Z => (( A(Z) = Sought) and
--# (for all M in Index range 1 .. (Z - 1) =>
--# (A(M) /= Sought)));
3.3.1.1 Implicitly-declared proof constants
Value of a variable on entry to a subprogram
For each variable V which is both an import and an export of a procedure subprogram P, a constant of the same type as V is implicitly declared, to represent the initial value of V within P's proof contexts. The name of this constant is obtained by decorating V with the suffix ~ (tilde). The name of this constant may only occur in the postcondition of P, and in proof contexts placed in the body of P. Notice that unless V is both imported and exported it may not be decorated with ~.
In SPARK, a function is not permitted to have explicit side effects on program variables and so it is not regarded as exporting any variables. For this reason, ~ is not generally permitted in function return annotations. An exception to this rule occurs when a function is used to read an external variable (see section 10.10) which therefore appears in the function’s global annotation. Reading an external variable has an implicit side effect of modifying that variable (see section 3.3.1.3). To allow the initial value of an external variable, prior to this side effect, to be specified, ~ may be used in function annotations only in the case of external variables globally referenced by the function.
The table below shows the meaning of a variable identifier X and its decorated variant X~ in various locations.
|
Location |
X |
X~ |
|
In a subprogram precondition |
Initial value of X |
Not permitted |
|
In a procedure postcondition |
Final value of X |
Initial value of X |
|
In a function return annotation |
Final value of X* |
Initial value of X* |
|
In a check or assert statement within a subprogram |
Value of X at that point in the subprogram's execution |
Initial value of X |
* where X is an external variable of mode IN globally referenced by the function
Value of a variable on entry to a for loop
For each variable V which is used in the range bounds expressions of a for loop, a constant of the same type as V is implicitly declared to represent the value of V on entry to the loop. The name of this constant is obtained by decorating V with the suffix % (percent). The name of this constant may only occur in proof contexts within the loop body.
The need to refer to variable values on entry to for loops arises from the semantic rules of Ada that require the loop exit bound expressions to be evaluated once only, and remain fixed, even if variables appearing in them are modified in the loop body.
Example (see Section 8.4.12 for more information on loop models):
type MyInt is range 0 .. 1000;
procedure Double (X : in out MyInt)
--# derives X from X;
--# pre X <= 500;
--# post X = 2 * X~;
is
begin
for I in MyInt range 1 .. X loop -- X used in exit expression
X := X + 1; -- X changed in loop body
--# assert X% = X~ and -- assertion of X initial value
--# X = X~ + I; -- rest of loop invariant
end loop;
end Double;
Note: where variables appear in the loop bound expressions but are not altered in the loop body it will usually only be necessary to add the assertion X% = X to the loop invariant.
3.3.1.2 Implicitly-declared proof functions
For each SPARK function in the source file the Examiner implicitly declares an FDL function. The signature of this implicitly-declared proof function contains all the arguments of the corresponding SPARK function followed by an additional argument for each global variable referenced by the SPARK function. Because the rules of SPARK prevent functions from having side-effects, the SPARK function and its implicitly-declared proof function are in precise correspondence for number and type of data objects read. Note that a SPARK function may not appear in proof contexts: the corresponding implicitly-declared proof function must instead be used in its place. An implicitly-declared proof function is considered to be declared immediately following the corresponding SPARK function's declaration.
3.3.1.3 Implicitly declared proof attributes
External variables are own variables or own variable refinement constituents declared with a mode indicating that they import values from or export values to the external environment. Where external variables of mode in are read, there is considered to be an implicit side-effect which transforms the external variable so that the next read operation will return a (possibly) different value. The conceptual model is that the external in variable is a sequence; reading it returns its head and the side-effect returns its tail ready for the next read. Values written to external out variables are considered to be appended to a sequence of values passed out to the environment.
For each external variable of mode in, a proof function attribute ’Tail is declared. The argument to this function attribute is the external variable itself and its return type is the type of the external variable. If Sensor is an external in variable then after the operation X := Sensor the following is true:
X = Sensor~ and
Sensor = Sensor’Tail (Sensor~);
For each external variable of mode out, a proof function attribute ’Append is declared. The first argument to this function attribute is the external variable itself, the second is the value written and its return type is the type of the external variable. If Actuator is an external out variable then after the operation Actuator := X the following is true:
Actuator = Actuator’Append (Actuator~, X);
There are four types of proof declaration: proof functions, proof types, type assertions, and object assertions. The following sections describe the use of each.
3.3.2.1 Explicitly-declared proof functions
Proof functions may also be declared explicitly and used after their declaration to simplify the expression of proof contexts within a SPARK program. The behaviour of such proof functions is specified in proof rules which can be used by the Proof Checker - see the Proof Checker Rules Manual [3]. A proof function declaration has exactly the same syntax as a SPARK function except that it is introduced with an annotation start symbol --#. Proof function declarations can appear anywhere a later_declarative_item or subprogram_declaration is permitted in SPARK. Proof functions declared either explicitly or implicitly are visible only in proof contexts.
A proof function without arguments is a useful way of defining a constant value which is visible only in a proof context.
It is sometimes useful to create a package especially to hold proof declarations; this package can then be inherited by packages which wish to refer to items in it but it does not need to be with’d since nothing in it is visible in the Ada sense. Note that this approach is not always possible since it may introduce circularity into the inherit chain.
3.3.2.2 Explicitly-declared proof types
SPARK abstract proof type declarations may be included in a package anywhere that basic declarations can be given. The relevant clauses from the SPARK syntax are:
basic_proof_declaration ::= proof_type_declaration | type_assertion | object_assertion ;
proof_type_declaration ::= --# type defining_identifier is proof_type_definition;
proof_type_definition ::= abstract
and basic_proof_declaration is included as a clause of the basic_declarative_item syntax production.[7] The name of a proof type must be distinct from any other SPARK name in scope in the defining package.
An abstract proof type, like a user defined proof function, only exists in SPARK annotations and does not have any corresponding Ada definition. Hence such a type can only be used in:
· an abstract own variable type announcement in the type’s package only;
· proof annotations in the package specification in which the type is declared;
· proof annotations in any package that inherits the type’s defining package.
An abstract proof type cannot be used in the body of the package in which it is declared.
3.3.2.3 Type assertions
A type assertion annotation is also a basic_proof_declaration. Its syntax is as follows:
type_assertion ::= base_type_assertion ;
base_type_assertion ::= --# assert identifier'Base is type_mark;
The base_type_assertion is used to specify the predefined base type that is chosen by the compiler to represent a particular signed integer or floating point type. This assists the Examiner when generating verification conditions for Overflow_Check for a type T, so that T'Base'First and T'Base'Last are known [2].
In a base type assertion, the identifier given must denote a signed integer or floating point type whose full declaration precedes the base type assertion in the same declarative region. The type mark given must denote one of the predefined signed integer or floating point types, which are typically specified using the target configuration file mechanism [1].
More information on the use of base type assertions is given in section 6.4.10.2.
3.3.2.4 Object assertions
An object assertion annotation is also a basic_proof_declaration. Its syntax is as follows:
object_assertion ::= --# for simple_name_rep declare identifier;
The object_assertion is used to specify whether replacement rules should be generated for the listed composite constants where the constant appears in VCs generated for subprograms directly or indirectly within the scope of the object_assertion. The identifier may take the values Rule or NoRule depending on whether replacement rules are required or to be suppressed.
Multiple object_assertions may appear for a given constant, although only one is permitted in a given declarative region. An object_assertion in the declarative region of a subprogram takes precedence followed by the object_assertion in the closest enclosing scope of a subprogram finally any object_assertion in the declarative region of the constant declaration is considered.
Replacement rules will be generated for composite constants based on the command line -rules switch [1] and the object_assertions within the code.
|
|
|
|
-rules switch value |
composite constant rule generation policy |
|
none |
No replacement rules are generated for composite constants (default) |
|
lazy |
Replacement rules are only generated if there is an object assertion requiring rule generation |
|
keen |
Replacement rules are generated unless there is an object assertion suppressing rule generation |
|
all |
Replacement rules are generated for all composite constants. |
3.3.3 Own variable type announcements
The announcement of both concrete and abstract own variables may contain a type mark. (Remember that concrete own variables are those that have Ada declarations.) We describe the announcement of concrete own variables first.
3.3.3.1 Concrete Own Variables
The type announcement of a concrete own variable allows reference to the type to be made in proof contexts prior to its Ada declaration. If this type mark is a selected component then its name must refer to a type declared in the visible part of an inherited package. If the type mark is a simple name then either it is the name of a type declared in package STANDARD or it is treated as an announcement of a type or subtype declaration that must occur within the package. Once a type is announced its simple name may not be used, other than for the declaration of further own variables, until the declaration of a type or subtype with the same simple name. When the own variable is declared in a SPARK variable declaration the type it is declared with must be the same as that announced in the own variable declaration.
The following are all legal examples of typed concrete own variables.
package P
--# own State : Integer; -- simple name of type from package standard
is
end P;
package body P
is
State : Integer; -- own variable declared with same type as announced
end P;
-------------------------------------
package Q
is
type Colour is (Red, Yellow, Blue);
end Q;
-------------------------------------
with Q;
--# inherit Q;
package P
--# own State : Q.Colour; -- selected component from inherited package
is
State : Q.Colour; -- own variable declared in package specification
end P;
-------------------------------------
package P
--# own State : Buffer; -- announcement of type buffer
is
end P;
package body P
is
type Index is range 1..100;
type Buffer is array(Index) of Integer; -- declaration of
-- announced type
State : Buffer; -- declaration of own variable
end P;
Note that in the final example, packages external to P do not have visibility of the type definition of the own variable (as the declaration of the announced type Buffer is in P’s body). This limits the statements about P.State that can be made in proof contexts in other packages.
3.3.3.2 Abstract Own Variables
The type announcement of an abstract own variable allows reference to the type to be made in proof contexts (in particular, in the declaration of proof functions). There are a couple of rules for the announcement of abstract own variables:
1 An own variable cannot be announced as being of a proof type declared in another package; this is because the proof type is considered to be a record based on the SPARK own variable refinement which is not visible outside the package in which it occurs. Thus --# own State : P.T; is illegal if P.T is an abstract proof type declared in package P.
2 Only one own variable may be declared as being of each abstract proof type. Thus ‘--# own State1, State2 : StateType;’ is illegal if StateType is an abstract proof type. This is because the built-in abstraction relation creates a record from the refinement constituents of the own variable. Since both State1 and State2 cannot be refined to the same constituents there would be no valid single definition of the StateType record.
Once an abstract proof type is announced its simple name may not be used until the declaration of the type.
Abstract proof types are handled in a similar way to private Ada types. Hence, in SPARK annotations no information about an abstract type is available, other than that two objects of the type can be compared for equality. External to an abstract type's package, its FDL model is simply a ‘pending’ FDL type (see Section 4.3.1). The FDL model internal to the package is described in Section 8.6.1.
In the previous section we stated that the Examiner regards any own variable lacking a type announcement as being abstract. If an abstract own variable is not type announced then the Examiner creates an FDL declaration for the own variable’s type, where the type name is formed by appending ‘_ _ type’ to the variable’s name. All the features of abstract proof (see Section 8.6) are unaffected by the absence of a user-provided name for the abstract proof type. The absence of such a name, however, does fundamentally limit what can be achieved because it means that it is not possible to define proof functions to describe the behaviour of operations in abstract terms.
Subprogram constraints are annotations that may be used to introduce specifications (pre-, postconditions and return expressions) of subprograms into SPARK program texts.
In the SPARK syntactic categories
· subprogram_declaration
· subprogram_body and
· body_stub,
procedure_annotation may be followed immediately by procedure_constraints, where
procedure_constraints ::= [ --# pre predicate ]
[ --# post predicate ]
In the above, predicate indicates an extended SPARK expression which is of type Boolean. The scope of the procedure_constraints of a procedure S is that of the declaration of S.
A procedure can only have constraint predicates on both its declaration and body if it imports or exports (as defined by its flow annotations) an abstract own variable from its own package or if it imports or exports a variable or parameter of a private type declared in its own package. The constraint predicates on the procedure’s declaration provide the abstract (external) view of the procedure and those on its body provide the concrete (internal) view.
If the procedure does not import or export an abstract own variable or a variable of a private type (from its own package) then any constraint predicates must be placed with the first appearance of the procedure (ie its declaration). These predicates can only refer to the concrete variables of the package containing the subprogram (and hence the same concrete view is used both externally and internally). However, the predicates may refer to abstract own variables from other (inherited) packages that are imported or exported by the procedure.
There are limitations to what may appear in the predicate expressions associated with pre- and postconditions:
precondition. In a precondition of a subprogram S, every identifier must be either
· the name of an imported variable of S;
· the name of an exported formal parameter of S which is of an unconstrained type (to allow the expression of constraints, such as length, on the actual parameter supplied. See Section 10.9 for an example);
· the name of a predefined function or attribute;
· a type-identifier;
· a constant;
· the name of a quantified bound variable; or
· a proof-function identifier.
Note. For convenience, the Examiner also assumes that a subprogram has the implicit precondition that its imports (formal parameters and concrete global variables) are correctly within their type. For example, if an in parameter X is of type Natural, it is not necessary to provide an explicit precondition that X >= 0.
postcondition. In a postcondition of a subprogram S, every name must be as for the precondition of S as specified above, but any variables which are both imported and exported by S may appear decorated with the tilde (~) suffix as described earlier.
The precondition of a subprogram specifies the properties of the computational state which are required to hold whenever the subprogram is called; the post-condition specifies the required relationship between the initial and final values of the state whenever execution of the subprogram terminates.
For example
procedure Inc(X : in out Integer)
--# derives X from X;
--# pre X < Integer'last;
--# post X = X~ + 1;
is
begin
X := X + 1;
end Inc;
If a pre- or postcondition is omitted, either abstract or concrete, the Examiner regards the constraint to be the predicate ‘true’ in all generated VCs. Typically this will be of use if a subprogram has no precondition, ie it may always safely be called. An empty postcondition may be of use if an attempt is being made to prove some property of a SPARK program where the values returned by a particular procedure are not of interest, for instance the absence of run-time errors.
The constraints assumed by the Examiner also mean that SPARK code is always proved against constraint predicates involving only concrete variables from the package. (As if a subprogram has abstract constraints, and no user supplied concrete constraints, then the Examiner uses concrete constraints of ‘true’ in generated VCs.).
In the SPARK syntactic categories
· subprogram_declaration
· subprogram_body
· body_stub
the function_annotation may be followed by function_constraints, where
function_constraints ::= [ --# pre predicate ]
[ --# return_expression ]
return_expression ::= return annotation_expression | return simple_name => predicate
The rules for the content, visibility and placement of function preconditions are identical to those for procedures. In place of a procedure’s postcondition, functions have a return expression which may specify the value returned by the function either explicitly or implicitly.
Example 1, an explicit return statement:
function Inc(X : Integer) return Integer
--# return X + 1;
is
begin
return X + 1;
end Inc;
Example 2, an implicit return statement:
function Max(X, Y : Integer) return Integer
--# return M => (X > Y -> M = X and
--# Y > X -> M = Y); -- deliberately incomplete
is
Result : Integer;
begin
if X > Y then
Result := X;
else
Result := Y;
end if;
return Result;
end Max;
The => symbol can be read as “satisfying” or “such that”. The identifier (here, M) in front of the => symbol has the same type as the result of the function and is used as a local name for the result; it must not be an otherwise visible identifier at the point of the function declaration. The entire return expression in the above example can be read as: return some M such that if X is greater than Y then M is X and if Y is greater than X then M is Y.
Note in this example that the return expression annotation is indeterminate in the case where X = Y. We can nevertheless prove that the function meets this partial specification, though ideally the return expression annotation should specify the value returned in such a case also.
The rules for the placement of abstract or concrete return annotations are the same as for procedure postconditions. Similarly, if a function’s precondition or return annotation is omitted, either abstract or concrete, the Examiner regards the constraint to be the predicate ‘true’ in all generated VCs (see also section 8.6.5.). Again this means that SPARK code is always proved against constraint predicates involving only concrete variables from the package.
Note that the implicitly-declared proof function (see section 3.3.1.2) associated with an Ada function is declared immediately after that function’s signature and so may be used in its return annotation, thus:
function Extract return Integer;
--# global State;
--# return Extract (State); -- use of implicit proof function
This technique can be useful in refinement proofs involving functions. See section 8.6.5.
Proof statements are transparent to the SPARK flow analysers, but they are used by the verification-condition generator to produce verification conditions and other formulae relating to the validity of a SPARK text.
The syntax category statement is extended with the category proof_statement.
proof_statement ::= --# assert predicate |
--# check predicate
Every sequence of statements must contain at least one statement which is not a proof statement.
In addition the syntax of loop statements is modified to allow an assertion to appear between iteration_scheme, if there is one, and the reserved word loop.
Both check and assert statements express constraints that the programmer wishes to show are true. VCs will be generated, by the Examiner, whose proof will confirm this. The expression describing the constraint may refer both to imported and exported variables (with decoration if appropriate) and to the subprogram's local variables. Whether a check or assert is used determines how VCs are produced.
An assert statement represents a cut point in the program control flow graph. Each loop must have an assert statement which cuts the loop and serves as a loop invariant. A loop invariant is a Boolean expression which must be true every time execution of the code of the loop body reaches the point at which it is placed. For example
while I <= n loop
........
--# assert I <= n and
--# X = X~ and .....;
........
end loop;
Because an assert statement is a cutpoint, hypotheses from previous check and assert statements are not carried through an assert statement; what is known about the subprogram’s state after an assert statement is only that which is included in it. For example:
............
--# check X /= 0;
Y := Z / X;
while Y > 0 loop
--# assert f(X, Y) > 0;
-- from here on X /= 0 cannot be assumed
............
It is therefore necessary sometimes to include additional clauses in an assert statement to specify relations between variables which are being maintained by the code if they are needed for some later part of a proof.
As well as their use as loop invariants, assert statements can be useful to break a long sequence of statements into several parts, each of which can be proved separately (though the need to do this may suggest that the code could be better structured, eg through procedural decomposition). Such use may simplify the overall task by reducing the number of VCs and/or making each somewhat easier to prove, since we need only reason about a relatively contained change of state.
A check statement is not a cutpoint (unlike assert). Like assert, however, it also results in the generation a proof obligation to show that the associated formula is true whenever execution reaches the point at which it is embedded in the code.
We can use check to prove the absence of certain run-time errors, eg:
--# check i in IndType and
--# a(i) in XType;
x := a(i);
--# check j /= 0
k := i / j;
(Note, however, that the Examiner generates VCs for such run-time conditions automatically, so it is not necessary to insert check statements manually for this particular purpose.)
3.6 Examples of proof contexts
3.6.1 Naive integer square root
This routine finds the integer square root of a non-negative number by starting the search at zero and trying successive candidates in turn until the root is found. (This is an extremely inefficient algorithm, particularly for larger N, but it is easy to prove its correctness.)
procedure Integer_Square_Root (N : in Natural;
Root: out Natural)
--# derives Root from N;
--# pre N >= 0;
--# post (Root * Root <= N) and
--# (N < (Root + 1) * (Root + 1));
is
R, S, T : Natural;
begin
R := 0; S := 1; T := 1;
loop
--# assert (T = 2 * R + 1) and
--# (S = (R + 1) * (R + 1)) and
--# (R * R <= N);
exit when S > N;
R := R + 1;
T := T + 2;
S := S + T;
end loop;
Root := R;
end Integer_Square_Root;
3.6.2 A more efficient integer square root
This algorithm expresses exactly the same functionality as the above example, but employs a binary search to find the square root, resulting in a much more efficient algorithm in the general case. It has also been written as a function subprogram, rather than a procedure, to illustrate the use of the return expression annotation. In all other respects, its visible specification is identical.
function Integer_Square_Root (N: in Natural) return Natural
--# pre N >= 0;
--# return Root => (Root * Root <= N) and
--# (N < (Root + 1) * (Root + 1));
is
lower, upper, middle: Integer;
begin
lower := 0;
upper := N + 1;
loop
--# assert (0 <= lower) and (lower < upper) and
--# (upper <= N + 1) and
--# (lower * lower <= N) and
--# (N < upper * upper);
exit when lower + 1 = upper;
middle := (lower + upper) / 2;
if middle * middle > N then
upper := middle;
else
lower := middle;
end if;
end loop;
return lower;
end Integer_Square_Root;
This is an implementation of the Euclidean algorithm to find the greatest common divisor of two non-negative numbers (at least one of which must be positive: this must be the first parameter of the procedure below). It also calculates two (non-unique) multipliers, Y and Z satisfying the relation shown in the postcondition below. Note that we use a proof function, gcd, as a shorthand for the mathematical function whose result we wish to calculate: its definition may be provided to the SPARK proof tools in the form of one or more proof rules (which are not given here).
--# function gcd(A, B: Natural) return Natural;
procedure Greatest_Common_Divisor
(M, N: in Integer; X, Y, Z: out Integer)
--# derives X, Y, Z from M, N;
--# pre (m > 0) and (n >= 0);
--# post (x = gcd(m, n)) and (x = y * m + z * n);
is
a1, a2, b1, b2, c, d, q, r, t: Integer;
begin
a1 := 0; a2 := 1; b1 := 1; b2 := 0; c := m; d :=
n;
loop
--# assert (c > 0) and (d >= 0) and
--# (gcd(c, d) = gcd(m, n)) and
--# (a1 * m + b1 * n = d) and
--# (a2 * m + b2 * n = c);
exit when d = 0;
q := c / d; r := c - q * d;
a2 := a2 - q * a1; b2 := b2 - q * b1;
c := d; d := r;
t := a1; a1 := a2; a2 := t;
t := b1; b1 := b2; b2 := t;
end loop;
x := c; y := a2; z := b2;
end Greatest_Common_Divisor;
As described in section 3.2.3, the Examiner supports the explicit use of quantification over predicates, eg to allow the statement of loop invariants:
i := index'first;
loop
a(i) := i;
exit when i = index'last;
--# assert
--# index'first <= i and i < index'last and
--# (for all k in Integer range index'first..i =>
--# (a(k) = k));
i := i + 1;
end loop;
(where k is an identifier not already in scope at the point that the quantification is introduced, in order to avoid variable capture).
However, the Examiner does not support explicit quantification over (non-predicate) expressions, eg to express the sum of a series of numbers. A numerical quantification example follows of what to do in such situations. (The format of proof rules, included in this example as an illustration, are covered in detail in the Proof Checker Rules Manual [3].)
Consider taking the sum of a collection of numbers: we must use proof function notation in this case. Suppose a program is to calculate
To specify its postcondition, we can declare
--# function sum (A: arrtype; L, U: index) return Integer;
intending sum(x, y, z) to be the sum of the elements of array x in the index range y..z inclusive. We may then write:
--# post s = sum (a, m, n);
We must take care to address the boundary cases, however: what is sum(a, 3, 2), for instance? Either the definition of sum, as provided in the proof rules to be used with the Proof Checker, must define this, or we must take care to ensure the question cannot arise. Two alternative means of addressing this are proposed below.
Solution 1: Make sum a total function:
sum(1): sum(A, I, J) may_be_replaced_by 0 if [I>J].
sum(2): sum(A, I, I) may_be_replaced_by element(A, [I]).
sum(3): sum(A, I, J) may_be_replaced_by
sum(A, I, J-1) + element(A,[J])
if [I<J].
We do not then need a precondition to the subprogram, and it is clear what result should be returned for empty index ranges.
Solution 2: Preclude empty index ranges:
--# pre m <= n;
In this case, the definition of sum can instead be:
sum(1): sum(A, I, I) may_be_replaced_by element(A, [I]).
sum(2): sum(A, I, J) may_be_replaced_by
sum(A, I, J-1) + element(A, [J])
if [I<J].
A possible implementation (with sum partial) is:
begin -- SumTotal
k = m;
s := a(k);
loop
--# ???;
exit when k = n;
k := k + 1;
s := s + a(k);
end loop;
end SumTotal;
What can we propose for a loop invariant for the above, given the proposed placement?
From the precondition, m <= n, so on entry to the loop we can see that m <= k <= n (since k = m initially). Does the loop preserve this? Yes, because if we get back to the invariant, we did not exit (so k <> n held, giving k < n) and we have incremented k by 1.
The other component that we are calculating is sum: on reaching the invariant initially on entry to the loop, s = a(m) = sum(a, m, m) = sum(a, m, k).
When VCs are produced by the Examiner they are expressed in a form which can be manipulated by the Simplifier and Proof Checker; the notation employed is an extended form of the expression language of FDL. FDL is the modelling language of the SPARK proof tools. Its use in expressing VCs generated from SPARK programs is limited since we are only concerned with FDL expressions together with such declarations as are required to denote the type of these expressions; we are not concerned here with FDL statements. Within a SPARK source text, proof contexts are expressed in an extended version of the SPARK language itself.
This chapter describes only those elements of FDL used to denote VCs of SPARK programs. Readers interested a full description of FDL are referred to the SPARK FDL manual [6]. New readers may choose to skim over this chapter since it is possible to gain an intuitive understanding of those elements of FDL needed to understand the Examiner's output from later chapters.
FDL bears some resemblance to a programming language; however, it is important to appreciate that FDL is essentially a modelling language used to describe the semantics of constructs present in imperative programming languages, to support the rigorous analysis of algorithms written in these languages. FDL's descriptions of objects, and of operations upon them, are to be interpreted in a mathematical sense. With regard to declarations, the FDL type-identifier integer, for example, refers to the set of mathematical integers. In the same way, the operations such as addition and subtraction on these numbers have their mathematical significance: they do not give rise to overflows. Similarly, an FDL declaration of a function introduces a pure function, ie a mapping from one set to another whose evaluation cannot produce any side-effects. We describe below those constructs present in FDL which are needed to express VCs generated by the Examiner.
The following is a list of the reserved identifiers of FDL (excluding those that are also reserved words of SPARK). Identifiers in this list may not be used as identifiers in a SPARK program if it is intended to use the VC generation facilities of the Examiner on it. By default the Examiner will report such use as syntax errors; however, it is possible to suppress this behaviour if only the non-proof facilities of the Examiner are to be used ¾ see the Examiner User Manual [1] for details.
|
abstract |
are_interchangeable |
as |
|
assume |
const |
div |
|
element |
finish |
first |
|
for_all |
for_some |
goal |
|
last |
may_be_deduced |
may_be_deduced_from |
|
may_be_replaced_by |
nonfirst |
nonlast |
|
not_in |
odd |
pending |
|
pred |
proof |
real |
|
requires |
save |
sequence |
|
set |
sqr |
start |
|
strict_subset_of |
subset_of |
succ |
|
update |
var |
where |
In addition identifiers beginning with the character sequences fld_ or upf_ are also regarded a predefined FDL identifiers.
Generally it should not be necessary for the user to create FDL declarations, since the Examiner automatically creates a file of those declarations used in the VCs that it generates. The syntax and explanation that follows is intended as a reference to enable these declarations to be read if so desired. A fuller explanation of all the FDL types available can be found in the FDL Manual [6].
A type characterizes a set of values which variables and constants of that type may assume, and the set of basic operations which may be performed on them. Type is an attribute possessed by every value and every variable.
FDL has three standard types: the real-type, the Boolean-type and the integer-type. Other types can be created through type declarations.
An FDL type-declaration associates an identifier with a type; the identifier may then be used to denote this type. A type-declaration may also give a definition of the type (in which case the type is said to be concrete); alternatively, the type-definition may be the reserved word pending (in which case the type is said to be abstract).
Abstract FDL types are used solely for abstract own variables, irrespective of whether or not SPARK abstract proof types are used to type announce them (see Section 3.3).
Concrete FDL types are classified into simple types and structured types. A simple type is a type whose values have no components, and form an ordered set. A structured type is a composite type, characterized by the type(s) of its components and the structuring method.
type-declaration ::= type type-identifier = type-definition | pending
type-identifier ::= identifier
type-definition ::= simple-type-definition | structured-type-definition
4.3.1.1 Simple types
A simple type is a type whose values have no components, and form an ordered set. The simple types comprise the ordinal types and the real type. The ordinal types comprise the enumerated types (which are defined by enumeration of their values, and include the standard Boolean type) and the integer type.
4.3.1.2 Enumerated types
An enumerated-type-definition defines an ordered set of values by enumeration of the identifiers which denote these values.
enumerated-type-definition ::= ( identifier-list )
identifier-list ::= identifier { , identifier }
The ordering of the values is determined by the sequence in which their identifiers are enumerated, ie if x precedes y then x is less than y.
The occurrence of an identifier in the identifier-list of an enumerated type constitutes its declaration as a constant.
An identifier cannot appear in more than one enumerated-type-definition.
Example:
type colour = (red, orange, yellow, green, blue, indigo, violet);
4.3.1.3 The Boolean type
The type-identifier boolean denotes the Boolean type. This is a standard enumerated type, whose values are the truth values denoted by the constant-identifiers false and true.
The Boolean-type is equivalent to the type-declaration
type boolean = (false, true);
together with additional logical operations such as and and or.
4.3.1.4 The integer-type
The type identifier integer denotes the integer type. This is a standard ordinal type, whose values are the positive and negative integers, in the mathematical sense.
4.3.1.5 The real type
The type-identifier real denotes the real type. This is a standard simple type, whose values are the real numbers, in the mathematical sense.
A structured type is a composite type, characterized by the type(s) of its components and the structuring method. The structured types comprise the array types and record types.
structured-type-definition ::= array-type-definition | record-type-definition
There are no restrictions on the types of the components of structured types, which can even be abstract.
4.3.2.1 Array types
An array type is a structured type consisting of a fixed number of components (called elements) which are all of the same type. An element of an array is designated by one or more index values belonging to declared enumerated or subrange types.
array-type-definition ::= array [ index-type-list ] of element-type-identifier
index-type-list ::= index-type-identifier { , index-type-identifier }
index-type-identifier ::= type-identifier
element-type-identifier ::= type-identifier
Examples:
type bit = (zerobit, onebit);
type bitposition = 1 .. 8;
type byte = array [bitposition] of bit;
type address = 1 .. 48;
type memory = array [address] of byte;
type matrix = array [row,column] of real;
Note that the FDL produced by the Examiner does not specify
ranges for integer types such as bitposition and address in the example above.
Instead, these types would appear simply as integers, with corresponding
constants to specify their minimum and maximum bounds, ie:
type bitposition = integer;
const bitposition__first : bitposition = pending;
const bitposition__last : bitposition = pending;
The actual values for these constants are then given in rule files (see section 4.3.3).
4.3.2.2 Record types
A record type is a structure consisting of a fixed number of components, possibly of different types. The record type definition specifies for each component, called a field, its type and an identifier which denotes it.
record-type-definition ::= record field-list end
field-list ::= record-section { ; record-section }
record-section ::= identifier-list : type-identifier
Examples:
type daynumber = integer;
type monthname = (jan,feb,mar,apr,may,jun,jul,aug,sep,oct,nov,dec);
type yearnumber = integer;
type date = record
day : daynumber;
month : monthname;
year : yearnumber
end;
A constant-declaration introduces an identifier to denote a value, which can be of any type, concrete or abstract. The declaration consists of an identifier denoting the new constant, followed by the identifier representing its type, followed by a constant-definition. If the constant is declared as being of integer type then the constant-definition can be a signed-integer, a character-string (which could be used to denote a very large integer), or the reserved word pending. If a constant is not of integer type then its definition must be either a character-string or the word pending.
constant-declaration ::= const identifier : type-identifier = constant-definition
constant-definition ::= signed-integer | character-string | pending
signed-integer ::= [ sign ] unsigned-integer
sign ::= + | -
Examples:
const answer : integer = 42;
const million : integer = '1000000';
const matrixorder : integer = pending;
const pi : real = '3.141593';
const avogadro : real = '6.02295e23';
const emptystack : stack = pending;
The constants produced by the Examiner are always declared as pending; values for such constants are substituted using suitable, automatically-generated proof rules. Proof rule generation for composite constants is governed by the rule generation policy requested on the Examiner command line and object assertions within the source code.
A variable is an entity to which a value may be attributed.
A variable-declaration consists of a list of identifiers denoting new variables, followed by their type.
variable-declaration ::= var identifier-list : type-identifier
Examples:
var x, y, z: real;
var p, q: boolean;
FDL functions are pure mathematical functions, as noted earlier.
function-declaration ::= function identifier [ ( parameter-type-list ) ] : type-identifier
parameter-type-list ::= parameter-type { , parameter-type }
parameter-type ::= type-identifier
Examples:
type stack = pending;
const emptystack : stack = pending;
function push(stack, integer) : stack;
function pop(stack) : stack;
function top(stack) : integer;
function is_empty(stack) : boolean;
function is_full(stack) : boolean;
4.3.6.1 Arithmetic functions
|
abs(x) |
For an expression x of integer type or real type, abs(x) denotes the absolute value of x. The type of the value of the function is the same as the type of its parameter, x. |
|
sqr(x) |
For an expression x of integer type or real type, sqr(x) denotes x * x. The type of the value of the function is the same as the type of its parameter, x. |
4.3.6.2 Ordinal functions
|
pred(x) |
For an expression x of ordinal type T, whose value is greater than the least member of T, pred(x) denotes the value immediately preceding that of x (in the enumeration of T). If x is the least member of T then the value of pred(x) is undefined. |
|
succ(x) |
For an expression x of ordinal type T, whose value is less than the greatest member of T, succ(x) denotes the value immediately succeeding that of x (in the enumeration of T). If x is the greatest member of T then the value of succ(x) is undefined. |
4.3.6.3 Boolean functions
|
odd(x) |
For an expression x of integer type, odd(x) is equivalent to the expression abs(x) mod 2 = 1. |
4.3.6.4 Functions for manipulating arrays
|
element |
Let A be an expression, of an array type declared in the form array[ i1, i2, ... , ip ] of T. Then the function-designator element(A, [k1, k2, ... , kp]), in which k1, k2, ... , kp are expressions whose values are assignment-compatible with the types i1, i2, ... , ip respectively, has the value of the array element A(k1, k2, ... , kp). |
|
update |
Let A be an expression, of an array type declared in the form array[ i1, i2, ... , ip ] of T. Then the function-designator update(A, [k1, k2, ... , kp], x), in which k1, k2, ... , kp are expressions whose values are assignment-compatible with the types i1, i2, ... , ip respectively, and x is an expression whose value is assignment-compatible with type T, has the value of the array A after the assignment of the value of x to its element A(k1, k2, ... , kp). |
Examples:
type rowindex = 1 .. 10;
colindex = 1 .. 20;
matrix = array [rowindex,colindex] of real;
var m: matrix; r: real;
............................
r := element(m, [3, 4]);
............................
m := update(m, [3, 4], r);
............................
m := update(m, [3, 4], element(M, [4, 3]) + r);
4.3.6.5 Functions for manipulating records
The declaration of a record-type R, with fields f1, f2, ... , fp of types t1, t2, ... , tp respectively, implicitly introduces p pairs of functions:
fld_f1(r) : t1 upf_f1(r, t1) : r
fld_f2(r) : t2 upf_f2(r, t2) : r
.............. .................
fld_fp(r) : tp upf_fp(r, tp) : r
For an expression x whose value is a record of type R, fld_fi(x) denotes the value of the field fi of the record, and it is of type ti. Also, if y is an expression whose value is assignment-compatible with type ti, then upf_fi(x, y) denotes the value of x, after the assignment of the value of y to its field fi.
4.3.6.6 Functions for assembling structured values
For every array or record type T, FDL implicitly declares a function mk__t which can be used to assemble objects from a collection of values. The parameters of mk__t are a series of assignments to the elements of an object of type t with an optional default value appearing first.
For records the function takes the following form:
mk__record ::= mk__record_type_identifier ( argument_list )
argument_list ::= association { , association }
association ::= field_identifier := expression
record_type_identifier ::= identifier
field_identifier ::= identifier
For arrays the form is slightly more complicated because defaults values are permitted as are assignments to multiple array elements:
mk__array ::= mk__array_type_identifier ( argument_list )
argument_list ::= expression | expression associations | associations
associations ::= association { , association }
association ::= index { & index } := expression
index ::= [ index_expression { , index_expression } ]
index_expression ::= expression [ .. expression ]
array_type_identifier ::= identifier
Examples
mk__complex(real := 1, imag := 0);
mk_table(0, [1] := 1, [2] := 99);
mk_matrix(0, [1,1] := 1, [2,2] := 2, [3,3] := 1);
mk_lookup([1] := 0, [2] & [3] := 1, [4] & [5] := 2);
mk_atype([1..10] := 1, [11..20] := 2);
Expressions are constructs denoting rules of computation for obtaining values of variables and constants, and generating new values by the application of operators and functions. FDL expressions consist of operands, operators, function-designators, set- and sequence-constructors, and quantifiers. Not all the elements of FDL expressions described in this section are used when VCs are produced from SPARK texts, however; they are included here because they may be introduced when VCs are manipulated with the Proof Checker.
expression ::= disjunction [ ( -> | <-> ) disjunction ] | quantified-expression
disjunction ::= conjunction { or conjunction }
conjunction ::= negation { and negation }
negation ::= [ not ] relation
relation ::= sum [ relational-operator sum ]
sum ::= term { adding-operator term }
term ::= factor { multiplying-operator factor }
factor ::= [ sign ] primary | primary exponentiation-operator primary
primary ::= variable-identifier | unsigned-integer | constant-identifier |
function‑designator | ( expression )
variable-identifier ::= identifier
constant-identifier ::= identifier
Any factor whose value is of type S, where S is a subrange of a type T, is treated as being of type T.
Examples:
|
Primaries: |
x 15 abs(x + y) (x + y + z) |
|
Factors: |
-x a ** b -(a ** b) a ** (-b) |
|
Terms: |
x * y i div (1 - i) |
|
Simple expressions: |
-x i * j + 1 |
|
Relations: |
Answer = 42 p < q (i < j) = (j < k) |
|
Negations: |
not p |
|
Conjunctions: |
x <= y and y <= z p and not q p = q and r |
|
Disjunctions: |
p or (x > y) |
|
Expressions: |
(a * a > b * b) -> (abs(a) > abs(b)) |
The FDL operators are:
exponentiation-operator ::= **
multiplying-operator ::= * | / | div | mod
adding-operator ::= + | -
relational-operator ::= = | <> | < | > | <= | >=
The types of the operands used with the FDL operators must be the same as the types specified in the subsections below, or subranges of those types.
4.4.1.1 Arithmetic operators
The arithmetic operators comprise the unary-minus operator “-” and the binary operators listed in the table below.
|
operator |
operation |
types of operands |
type of result |
|
** |
exponentiation |
(Integer or real) - integer |
If the left hand operand is an integer then the right hand operand must be greater or equal to zero and the result is an integer. If the left hand operand is a real then the result is a real. |
|
* |
multiplication |
integer or real |
integer if both operands are of type integer; otherwise real |
|
/ |
division |
integer or real |
real |
|
div |
division with truncation |
integer |
integer |
|
mod |
modulus |
integer |
integer |
|
+ |
addition |
integer or real |
integer if both operands are of type integer; otherwise real |
|
- |
subtraction |
integer or real |
integer if both operands are of type integer; otherwise real |
The unary-minus operator takes an integer or real operand; it produces a result of the same type as its operand.
The div operator truncates towards zero, so that -(a div b) = -a div b. Also, a div -b = -a div b. The FDL mod operator is defined by a mod b = a - ((a div b) * b). The right operands of div and mod must be non-zero.
4.4.1.2 Boolean operators
In the list of operators given below, the not operator is a unary operator and the others are binary operators. They all take Boolean operands and produce a Boolean result.
|
operator |
operation |
|
not |
logical negation |
|
and |
logical conjunction |
|
or |
logical disjunction |
|
-> |
logical implication |
|
<-> |
logical equivalence |
4.4.1.3 Relational operators
The relational operators compare their operands and produce a result of type Boolean.
|
operator |
relations |
types of operands |
|
= <> |
equality and inequality |
any type |
|
< > <= >= |
ordering |
any simple type |
|
-> <-> |
logical implication and equivalence |
Boolean |
The operators <= and >= stand for less than or equal, and greater than or equal, respectively. In comparing values of set type they denote set inclusion in FDL, though this overloading is eliminated within the SPARK proof tools.
4.4.1.4 Operator precedence
In the table below, the operators are listed in order of decreasing precedence (but with operators at any level being of equal precedence). Note that this ordering can be inferred from the syntax of expressions.
**
- + (unary minus or plus)
* / div mod
+ -
= <> < > <= >=
not
and
or
-> <->
In expressions, sequences of operators of the same precedence are applied from left to right.
Since functions cannot have side-effects, the order of evaluation of operands in an expression need not be defined.
A function-designator specifies the evaluation of a function. It consists of the identifier designating the function, and a list of actual parameters. The parameters are expressions, whose values must be assignment-compatible with the corresponding parameter-types in the function.
function-designator ::= function-identifier [ ( actual-parameter-list ) ]
function-identifier ::= identifier
actual-parameter-list ::= actual-parameter { , actual-parameter }
actual-parameter ::= expression
Examples: abs(x) gcd(m, 42) sin(p + q)
4.4.3 Quantifiers
A quantified-expression consists of the quantifier, the quantified variable (with its associated range of values) and the Boolean-valued expression that is being quantified over.
quantified-expression ::= quantification-kind ( quantification-generator , boolean-expression )
quantification-kind ::= for_all | for_some
quantification-generator ::= identifier-list : type-identifier
boolean-expression ::= expression
Examples:
for_all (k : indexrange,
(1 <= k) and (k < r) ->
(element(a, [k]) <= element(a, [k + 1])))
for_some (m : mapping,
for_all (k : indexrange,
element(a, [element(m, [k])])
= element(b, [k])))
5 Generation of Verification Conditions
This chapter provides a more detailed example of the process employed by the Examiner to generate verification conditions by hoisting assertions up through the code to generate weakest preconditions, as briefly outlined earlier.
Consider the following SPARK code fragment which represents an integer division algorithm.
--# pre (M >= 0) and (N > 0);
--# post (M = Q * N + R) and (R >= 0) and (R < N);
Q := 0;
R := M;
loop
--# assert (M = Q * N + R) and (R >= 0);
exit when R < N;
Q := Q + 1;
R := R - N;
end loop;
This can be represented by the following annotated flow chart.
Weakest preconditions can be generated by hoisting the post condition through the code as described earlier; the weakest precondition of each reachable assertion at each point on the flow chart is shown on the second annotated diagram.
For a path from assertion A to another assertion B, with traversal condition T (possibly rewritten by the assignment statements along the path), the verification condition is:
A (T B')
(where B' is B rewritten by the assignment statements of that path). T B' is the weakest precondition of assertion B for this path, with B' being the assertion B after transformation by the assignments and procedure calls which occur along the path.
This formula may be written as:
(A T) B'.
We can rewrite it in this way, because
A (T B') (A T) B'
is a tautology.
5.2 Verification conditions for integer division example
Given the above annotated example, the VCs generated are:
For path from start to loop-invariant:
Weakest precondition: 0 * N + M >= 0.
VC: M >= 0 M = 0 * N + M and M >= 0.
For path from loop-invariant back to itself:
Weakest precondition:
R >= N (M = (Q + 1) * N + R - N and R - N >= 0).
VC: (M = Q * N + R and R >= 0 and R >= N)
(M = (Q + 1) * N + R - N and R - N >= 0)
For path from loop-invariant to end of subprogram:
Weakest precondition:
R < N (M = Q * N + R and R >= 0 and R < N).
VC: (M = Q * N + R and R >= 0 and R < N)
(M = Q * N + R and R >= 0 and R < N)
5.3 Further example: “sum” revisited
Consider again the annotated code fragment shown below:
--# pre m <= n;
--# post s = sum(a, m, n);
begin -- SumTotal;
k = m;
s := a(k);
loop
--# assert(s = sum(a, m, k)) and
--# (m <= k) and (k <= n);
exit when k = n;
k := k + 1;
s := s + a(k);
end loop;
end SumTotal;
The VCs generated from this are as follows:
For path from start to loop-invariant:
m <= n a(m) = sum(a, m, m).
For path from loop-invariant back to itself:
(s = sum(a, m, k) m <= k k <= n k n)
(s + a(k+1) = sum(a, m, k+1) m <= k+1 k+1 <= n)
For path from loop-invariant to end of subprogram:
(s = sum(a, m, k) m <= k k <= n k = n)
s = sum(a, m, n).
5.4 The relationship between verification conditions and code
This section records some common observations about the correspondence between code annotated for proof and the VCs generated from it.
If we prove a VC by establishing a contradiction amongst the hypotheses of the VC, this VC corresponds to a non-executable path. Such a path can be non-executable either implicitly or explicitly:
· If the path traversal condition (without the assertion at the top of the path) contains a contradiction, the path is explicitly non-executable; for example:
if x = 1 then y := y + 1; end if;
if x = 2 then y := y - 1; end if;
Syntactically, there is a path for x=1 x=2 but semantically, it is non-executable.
· If the contradiction is between the traversal condition and the assertion at the top of the path, the path is implicitly non-executable:
--# assert x >= 1;
if x < 0 then y := y - 1; end if;
If a conclusion C in a VC is identical to a hypothesis H, this often indicates an expression which is invariant for this path (for example, around a loop).
For a loop with incrementing counter (i, say), we must often establish, to prove the subsequent VCs, that i attains its maximum value on exit from the body of the loop.
A VC which does not appear to be provable suggests:
· a fault on the corresponding path in the code; or
· that the code annotations are themselves either false or insufficiently strong; or
· possibly both of the above!
Experimenting with counter-examples to invalidate the VC can reveal which case applies.
The ZombieScope tool [7] searches for non-executable paths in SPARK code by attempting to find contradictions in the hypotheses in Dead Path Conjecture (.dpc) files produced by the Examiner. (See section 2.4.2.4.) The output from ZombieScope may be summarised using POGS.
6 Verification Conditions for Run-time Checks
This section covers the form and meaning of the VCs corresponding to Ada’s predefined run-time checks (RTCs). Subsections identify:
· the program constructs for which RTCs are generated;
· the hypotheses that are inferred from code and can be used to help discharge the VCs;
· proof of VCs;
· important assumptions affecting the validity of the proof; and
· significant limitations.
6.1 Sources of run-time errors
The Ada language definition requires compilers to generate
checks for certain error conditions at run time, raising a predefined exception
when they occur, unless such checking is suppressed by the user. The
predefined exceptions and their causes are tabulated below.
|
Exception |
Source |
|
CONSTRAINT_ERROR[8] |
access check, discriminant check, division check, index check, length check, overflow check, range check, tag check. |
|
PROGRAM_ERROR |
erroneous execution, incorrect order dependence, return not executed in function subprogram, elaboration check, accessibility check. |
|
STORAGE_ERROR |
exhaustion of dynamic heap storage, stack overflow |
|
TASKING_ERROR |
exceptions raised during intertask communication |
The use of SPARK removes the possibility of many forms of run-time error either because
· the language subset does not include the Ada feature concerned; or
· the additional static semantic rules of SPARK allow the error to be detected before the program is run.
An example of the former is the elimination of TASKING_ERROR in sequential SPARK as it does not permit tasking. An example of the latter is the Examiner’s ability to detect whether a subtype indication is compatible with the type mark in a subtype definition. By these means, all the errors in italics in the table above are eliminated.
SPARK also greatly reduces the likelihood, and eases the prevention, of STORAGE_ERROR because the programmer does not have direct access to the dynamic heap; furthermore, the rules of SPARK enable a program’s maximum memory requirements to be calculated prior to execution.
We are therefore left with index check, range check, division check and overflow check. It is to the elimination of errors associated with these checks that the generation and discharging of RTC VCs is applicable.
6.2 Detection of run-time errors
Ada compilers insert additional code to check at run time whether certain language rules are being violated. For example, whenever an expression is used as an array index a check will be made that the value of the expression lies within the array’s bounds. The Examiner automatically inserts check statements[9] at the same points and generates verification conditions from them. Proof of these verification conditions shows that the associated run-time errors cannot occur. The Examiner also takes advantage of the Ada type system in providing additional information that can be assumed during the proof process.
Consider the following tiny example:
7 type T is range -128 .. 128;
8
9 procedure Inc(X : in out T)
10 --# derives X from X;
11 is
12 begin
13 X := X + 1;
14 end Inc;
On entry to Inc we can assume that T’First £ X £ T’Last because if this were not true then a run-time error would already have occurred at the point where Inc was called. In order to show that the single executable statement in Inc does not cause a run-time error we need to show that at that point T’First £ (X + 1) £ T’Last is true. Both the assumption and required check are automatically inserted by the Examiner which causes VCs to be generated. After simplification these VCs reduce to the following.
For path(s) from start to check associated with statement of line 13:
procedure_inc_1.
H1: x >= - 128 .
H2: x <= 128 .
->
C1: x <= 127 .
There are two hypotheses (which may be assumed true) and a
single conclusion to be proved. Unfortunately it is clear that the hypotheses
are not strong enough to allow the conclusion to be proved so a potential
run-time error exists. From the VC we can readily deduce the circumstances
when the run-time error will occur: when Inc is
called with
X = 128.
Strategies for eliminating such potential run-time errors are discussed in section 6.7.
6.4 What VCs are generated for RTCs?
This section summarises the language constructs for which RTC VCs are generated.
Wherever an expression of a scalar type is assigned, a VC is generated to show that the value of the expression lies in the subtype of the object to which it is being assigned. A similar check is made that a function return value is in range.
Note that VCs are generated on the assumption that function calls are evaluated in lexical order (i.e. from left to right) within an expression. The compiler is permitted to reorder evaluation under some circumstances. However, because in SPARK functions cannot have side effects, the order of evaluation is immaterial to the validity of the VCs. The order in which the VCs are generated may affect the ease of proof of an individual VC. For example, if the left hand function has a more severe precondition than that on the right then its proof will provide a hypothesis making proof of the right hand function’s precondition trivial. If the functions are placed in the reverse order then both preconditions will have to be proved separately; however, the overall proof obligation is the same in both cases.
Similar checks are made for the components of a named or positional association. These include procedure calls, function calls and aggregates. Each expression is checked to ensure that it lies in the subtype range of the component with which it is being associated. For a procedure call the required check is that each expression associated with an imported scalar, formal parameter is in range. A check is also required that each exported scalar, formal parameter is in the subtype of its associated actual parameter.
Wherever name argument lists occur (e.g. in array accesses) a check is made that each index expression lies in the subtype range of its corresponding index subtype. These checks are sufficient to show that arrays are never accessed outside their bounds.
6.4.4 Type conversion and qualification
Scalar type conversions and type qualifications require similar checks: the value of the expression must lie in the subtype range of the type to which it is being converted or with which it is qualified. The static semantic rules enforced by the Examiner ensure that type conversion of arrays cannot give rise to run-time errors so no run-time check is generated for such conversions. Other type conversions are not permitted apart from unchecked type conversions. Unchecked type conversions are not checked and may give rise to invalid values. Dealing with potentially invalid values is covered in section 6.5.2.
6.4.5.1 Succ
A check is made that X ¹ T’Last in the expression T’Succ(X);
6.4.5.2 Pred
A check is made that X ¹ T’First in the expression T’Pred(X);
6.4.5.3 Val
A check is made that X >= T’Pos(T’First) and X <= T’Pos(T’Last) in the expression T’Val(X);
In the case of if-statements, case-statements, while-loops and conditional exits, checks are made, in the same way as all other expressions, that the controlling expression of the condition is free from run-time errors.
6.4.6.1 Short-circuit forms
Modified checks are required in the case of the short-circuit forms and then and or else. When these forms are used a run-time error may not occur even if the right hand side of the short circuit conditional would appear to generate one. For example: if X /= 0 and then Y / X > 10 cannot cause a division by zero. Using the decoration ok to indicate “free from run-time error” the checks required for Left and then Right are:
and for Left or else Right:
A check is made that the right-hand side of all division operators is non zero. A check is also made that the exponent of an exponentiation is not negative if the operand is integral.
An additional check is made that the exponent of an exponentiation is not negative if the operand is the real value zero (0.0).
Checks are made at all unary and binary operators that the result of the operation lies in the base type of the type returned by the operator. Note that this differs from most of the run-time checks so far described where we are typically interested in an expression lying in a particular subtype range.
6.4.8 Private and abstract types
The uses of an object of a private type outside its package of definition are limited to assignment and comparison for equality. Since there are no subtypes of private types, run-time errors cannot occur during such operations. The only other operations defined for a private type are those specifically declared and exported by its declaring package. No run-time error can occur from the use of private types at the interface to these operations (although, of course, one might within the body of such an exported subprogram where the full details of the private type are known).
Similarly, a SPARK subprogram may indirectly import or export global data which is not directly visible according to the rules of Ada; for example, the abstract own variables associated with a package implementing an abstract state machine. Run-time errors cannot occur outside such a package from manipulation of this abstract state although, as with private types, checks will be required within the bodies of the subprograms which provide the exported operations of the abstract state machine.
The Examiner does not, therefore, generate any VCs associated with the assignment of objects of private types nor their passing as parameters. Neither are checks generated where global data, which is not directly visible, is imported or exported.
The static semantic rules of SPARK ensure that Boolean expressions cannot cause run-time errors. For example Boolean’Succ(True) is not permitted. For this reason VCs are not generated from such expressions.
6.4.10 Detection of Intermediate Expression Overflows
The Examiner generates VCs to guard against overflow during expression evaluation. VCs are generated for all unary and binary operators.
Where an expression contains operators of the same precedence a compiler is permitted to re-order the expression even if this results in a run-time error where left-to-right evaluation would not have done so. This permission is given in LRM 11.6(5) for Ada 83 and 4.5(13) for Ada 95 and Ada 2005. The Examiner generates VCs on the basis of left-to-right evaluation but will issue a warning message (included in the listing and report files) if an expression is vulnerable to change in this way. It is highly recommended that such expressions are parenthesised to make their evaluation order unambiguous.
An overflow occurs during expression evaluation when the result of applying an operator cannot be contained in the base type of the type returned by the operator. The size of this base type is determined by the compiler and is not normally available to the Examiner for the purpose of generating rules, unless it is specified using a type assertion annotation. This section illustrates the use of this facility.
Suppose we have the following type declaration:
type T is range 1 .. 10;
The Examiner cannot know the range of the corresponding base type chosen by a compiler. The user, though, may be able to determine which base type is used through inspection of a compiler's documentation, or by experiment, so SPARK allows a base type assertion annotation to assert the compiler's choice in the source text. It is used as follows:
type T is range 1 .. 10;
--# assert T'Base is Short_Integer;
The type on the right-hand side must be one of the predefined numeric types defined in package Standard, which is supplied by the target configuration file. To be useful, the configuration file for the target platform must supply a well-formed type declaration for any such predefined numeric types, such as Short_Integer. For example, the target configuration file might contain a declaration of Short_Integer as follows:
type Short_Integer is range -32768 .. 32767;
This declaration, along with the base type assertion annotation, allows the Examiner to generate proof rules for the Simplifier that allows VCs arising from Overflow_Check to be fully discharged.
Since release 10.0 of SPARK, the language and toolset have supported explicitly derived numeric types, so the base type assertion is now considered redundant. The following example:
type T is range 1 .. 10;
--# assert T'Base is Short_Integer;
is equivalent to:
type T is new Short_Integer range 1 .. 10;
The latter form does not require the user to add the base type assertion, and does not suffer the risk of the user indicating the incorrect base type, so is preferred.
6.4.10.2.1 Overflow checks and dynamic universal integer expressions
Rarely, a universal integer expression is evaluated dynamically (i.e. at run-time) in SPARK. In this case, the expression is evaluated using a base type whose range is equivalent to System.Min_Int .. System.Max_Int. Again, the target configuration file or a shadow specification of package System can be used to specify these constants so that such VCs may be automatically discharged by the Simplifier.
6.4.10.3 Other proof approaches
6.4.10.3.1 Provide actual values as proof rules
As for predefined types such as integer we can provide rules giving the Simplifier the actual value of the bounds of base types. These can either be obtained by writing a test program to obtain the exact values or by using information supplied by the compiler vendor. This approach allows proof of absence of overflow to be established for a particular compiler and target processor.
6.4.10.3.2 Use of conservative values
The Examiner generates rules for base types of the following form:
integer__base__first <= integer__first may_be_deduced.
integer__base__last >= integer__last may_be_deduced.
If a value has been provided for integer’first and integer’last using a configuration file for the target platform then these rules are sufficient to show that overflow will not occur provided intermediate expression values remain in the range integer’first.. integer’last.
Alternatively, user defined proof rules can be provided allowing the bounds of base types to be replaced by arbitrary but conservative values. For example integer__base__last may_be_replaced_by 32767. would allow proof of absence of overflow for all target platforms where the underlying integer type was at least 16 bits long.
6.4.10.3.3 Use of explicit type conversion
Given: type T is range -128..128; we can guard against expression overflow, without knowing the size of T’Base’First and T’Base’Last by using some larger, intermediate, user-defined type within the expression. For example we can replace the statement:
X := X * X + X; (where X is of type T)
by
X := T(ET(X) * ET(X) + ET(X));
(where ET is a user-defined type somewhat larger than T)
With expression checks enabled we will get VCs in terms of ET’Base’First and ET’Base’Last as before; however, we will have proof rules for ET’First and ET’Last and with these (if ET is big enough) we will be able to show that the sub-expression results lie within the type ET. Since we also know that a base type is always at least as big as any subtype of it we will have also proved that the sub-expression results lie in the base type of ET.
The previous section describes checks “planted” by the Examiner from which verification conditions are generated. To assist in the proof of these VCs the Examiner also provides as hypotheses properties of the code which may be assumed. For example, since a check is made on a procedure call statement that each imported actual parameter lies in the subtype range of its corresponding formal parameter, the Examiner provides hypotheses within a subprogram body that each imported formal parameter, or directly visible global import, is in range. Where a structured object is imported, each of its elements is assumed to be correctly within type. Similarly, it is assumed that any constant used is in range.
Hypotheses that variables exported by called subprograms are within the type exported, and that function return values are within their specified type, are also generated. Hypotheses are also generated from preceding statements in a sequence of statements. Each statement will have associated with it a VC whose proof will show that statement to be free of run-time errors. If the statement is free of run-time errors then control will pass to the next statement where the correctness of the preceding VC may be assumed as a hypothesis.
Additionally, 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. 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 (see Section 7.1) which would otherwise introduce random values to local variables.
2 The absence of invalid values (See section 6.5.2).
For example:
procedure Process(X : in out T)
--# derives X from X;
is
begin -- we can assume X in T here
X := X + 1; -- we must show X + 1 in T here
-- we can assume X + 1 in T here
X := X * 2; -- we must show (X + 1) * 2 in T here
end Process;
-- given subtype ST is T range ? .. ?; and A : ST;
-- a call to Process has the following obligations
we must show A in T here
Process(A);
we can assume A in T here
we must show A in ST here
An invalid value may be read from an external source, occur as the result of an unchecked type conversion, or as a value returned from an external subprogram (for instance written in C or assembler).
For this reason the Examiner makes no assumption that the value read from an external variable (an own variable or refinement constituent with the mode in) or the result of a call to an instantiation of Unchecked_Conversion is in its type. An Unchecked_Conversion is literally unchecked and therefore any value returned may be invalid. External variables are assumed to be connected to the external environment from which any bit pattern (not necessarily a legal value) might be received.
For example:
package Sensor
--# own in Port; -- an external in variable
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.
6.5.2 Avoiding potentially invalid values
To avoid the potential for an invalid value ensure that the variable to receive the external input or result of the unchecked conversion is of a type which guarantees that any bit pattern received is a valid value. The example from 6.5.1 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 ...;
--# assert Port’Always_Valid;
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;
The Always_Valid assertion is recommended to inform the Examiner that an invalid value will not be read from the attributed external variable (see section 6.5.4).
This example results in a provable set of run-time check VCs.
6.5.3 Input validity and the ‘Valid attribute
The Examiner does take note of the fact that Ada does not require a constraint check for an assignment between identical subtypes (although an Ada compiler is at liberty to perform a run-time check) so it is possible 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; -- Examiner does not generate check because subtypes are same
-- However, the compiler is at liberty to place a run-time check here
if Local'Valid then
X := Local;
else
-- return default value
X := SensorRange'First;
end if;
end Read;
The example assumes that the Ada compiler used to compile the code does not generate a run-time check for the assignment of “Port” to “Local” or that the unit has been compiled with checks suppressed.
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 and the Examiner VC Generator automatically generates proof rules defining the sensorrange__valid function to complete the proof formally.
6.5.4 Input data validity and the ‘Always_Valid assertion
As described section 6.5.1, the validity of input data is an important topic in ensuring the robustness of SPARK programs. As noted, by default, the Examiner makes no assumption about the range or validity of a value that is read directly from an external variable. This is safe, but is sometimes over-conservative when an external value definitely has no possible invalid values.
To this end, SPARK provides an “Always_Valid” assertion that indicates to the VC Generator that an external variable is to be “trusted” in that a value read from it may be assumed to be valid at all times.
Syntax
Syntactically, the Always_Valid assertion is a type_assertion in the grammar, which is in turn a form of basic_proof_declaration:
type_assertion :
base_type_assertion
| alwaysvalid_variable_assertion ;
alwaysvalid_variable_assertion :
proof_context assert
dotted_simple_name attribute_ident semicolon annotation_end ;
Static Semantics
The attribute_ident in this assertion must be ‘Always_Valid. The prefixing dotted_simple_name must denote an external variable of mode “in” that is of one of the following:
1 a scalar type,
2 an array of scalar components,
3 a non-tagged record whose components comprise only scalar or array of scalar types,
4 an array of records where the elements satisfy constraint (3), or,
5 a field of a, possibly tagged, record object which is compliant with one of types (1-4).
The object denoted by the prefix must have been previously declared within the same declarative region as the assertion itself.
Examples:
Port : T; -- where T is denotes one of the types in 1-4
-- and Port is an “in” mode own variable.
for Port'Address use ...;
--# assert Port’Always_Valid;
Port2 : R; -- where R is a record type with a field F1
-- that is compliant with one of the types 1-4
-- and Port2 is an “in” mode own variable
for Port2’Address use ...;
--# assert Port2.F1’Always_Valid;
Dynamic semantics
The assertion has three significant effects:
· The generation of warnings 392 and 393 is suppressed for references to that external variable.
· When the external variable is read, the VC Generator generates an additional hypothesis to indicate that the variable is considered to be valid.
· The VC Generator produces additional proof rules indicating that the value of an object, or that of each of its subcomponents, is considered to be “Always Valid” and therefore within the range of its scalar subtype.
Example
The first example in section 6.5.1 above showed how a normal untrusted external variable results in an unprovable VC:
For path(s) from start to finish:
procedure_read_1.
H1: true .
->
C1: true .
C2: port >= sensorrange__first .
C3: port <= sensorrange__last .
Now consider a similar package, but where the Port being read returns a 16-bit modular type. In this case, we assume that the actual hardware device being read can only ever return 16 bits of information, so that there are no invalid values for this type. In this case, we can indicate to the Examiner that the external variable is considered to be always valid, thus:
package Port
--# own in S : T;
is
type T is mod 2**16;
function Read return T;
--# global in S;
end Port;
package body Port
is
S : T;
for S'Address use 16#FFFF_0000#;
--# assert S'Always_Valid;
function Read return T is
Tmp : T;
begin
Tmp := S;
return Tmp;
end Read;
end Port;
Firstly, the Examiner does not report warning 392 for the body of the function Read:
+++ Flow analysis of subprogram Read performed: no
errors found.
Secondly, the unsimplified VC for Read appears as:
function_read_1.
H1: true .
H2: t__always_valid(s) .
->
C1: true .
C2: s >= t__first .
C3: s <= t__last .
With an additional FDL declaration:
function t__always_valid(integer) : boolean;
and proof rules:
read_rules(3): X <= t__last may_be_deduced_from
[ t__always_valid(X) ].
read_rules(4): X >= t__first may_be_deduced_from
[ t__always_valid(X) ].
read_rules(5): t__always_valid(s__tail(X)) may_be_deduced_from
[ t__always_valid(X) ].
read_rules(6): t__size >= 0 may_be_deduced.
read_rules(7): t__first may_be_replaced_by 0.
read_rules(8): t__last may_be_replaced_by 65535.
Rules 3, 4, 7 and 8 allow C2 and C3 above to be fully proven by the Simplifier.
Sometimes, one of the hypotheses for a VC will be demonstrably false or the hypotheses will be mutually contradictory. This can only arise from the existence of a non-executable path through the code: either because of a branch which can never be taken or because a previous statement will always generate a run-time error. In the latter case there will always be a preceding VC with a provably false conclusion. All lines following the VC with a false conclusion are non-executable in the sense that they can never be reached.
The proof of a RTC VC obtained from the Examiner shows that the error it was generated to guard against cannot occur. Ideally we will wish to prove all the VCs generated to show that the entire SPARK source is free from most potential run-time errors as specified in section 6.1. The Examiner will produce a large number of VCs; however, many of these are of relatively simple form. The Simplifier should therefore routinely be applied to the VCs produced and which will typically reduce them very significantly. Where a VC cannot be proved this may indicate a possible run-time error or that the VC is true but beyond the capability of the Simplifier tool. The most common cases where the Simplifier will not be able to prove a VC are:
· The VC depends on the properties of a predefined type or a base type for which no replacement rule is available. Suitable rules for the predefined integer and real types and various system values can be generated by specifying a configuration file for the target platform as described in [1].
· The VC includes a quantifier describing the behaviour of a structured object.
· Proof of the VC requires more information about the contents of particular elements of a structured constant than is available from the proof rules generated from such constants.
In some cases the provision of additional proof rules will allow automatic simplification. VCs which cannot be simplified automatically may be provable with the assistance of the Proof Checker or by use of rigorous argument.
Note that if the Simplifier detects false or contradictory hypotheses, it will conclude that the VC is proven by contradiction: this will always indicate a non-executable path as described in section 6.5.5 above.
6.7 Strategies for Eliminating Run-time Errors
Elimination of run-time errors requires the SPARK code to be considered procedure by procedure in a mostly bottom-up order showing that each is exception-free. Where the proof process shows a subprogram to contain a potential run-time error there are a number of approaches that can be used to eliminate it or show that the risk it poses is not significant.
6.7.1 Strengthening specifications
One way of removing a potential run-time error from a subprogram is to strengthen its specification with a precondition which disallows calling it under the conditions which would cause it to produce a run-time error. For example the Inc procedure at section 2.3 can be made safe from run-time errors by adding the precondition --# pre X < T’Last; The presence of a suitable precondition provides additional hypotheses allowing the VCs to be proved. Where a subprogram is annotated in this way the Examiner will generate an additional VC in all the places from which it is called so that it can be proved that it is being called within the limits permitted by its precondition.
Alternatively, it may sometimes be useful to strengthen the postcondition of a called subprogram in order to provide the information needed to show that the caller is free from run-time errors; an example of this approach is given in section 6.7.1.5 below.
The ease with which a suitable precondition can be expressed for a subprogram depends on the nature of the imports and exports it manipulates. If these are all of concrete Ada types then a simple expression can be used. If, however, they are of private types then they can only be expressed in terms of a proof function. Finally, if the subprogram manipulates truly abstract state contained in a package implementing an abstract state machine then it may not be possible to express a precondition at all unless additional Ada functions are introduced. All three cases are illustrated below using a stack package as an example.
6.7.1.1 Concrete imports and exports
package Stack
--# own Vector, Ptr;
is
type Index is range 1..10;
type Vectors is array(Index) of Integer;
Ptr : Index;
Vector : Vectors;
procedure Push(X : in Integer);
--# global Vector, Ptr;
--# derives Vector from Vector, Ptr, X &
--# Ptr from Ptr;
--# pre Ptr < Index’Last;
end Stack;
With the state of the stack package visible and expressed in concrete Ada terms we can express a precondition as a SPARK expression.
6.7.1.2 Private imports and exports
package Stack
is
type Stacks is private;
--# function NotFull(S : Stacks) return Boolean;
procedure Push(S : in out Stacks;
X : in Integer);
--# derives S from S, X;
--# pre NotFull(S);
private
...
end Stack;
Where the push operation modifies an abstract data type in the form of a private type the precondition can only be expressed in terms of a suitably-declared proof function (or by use of a suitable SPARK function as in the following example).
6.7.1.3 Abstract imports and exports
package Stack
--# own State;
is
function NotFull return Boolean;
--# global State;
procedure Push(X : in Integer);
--# global State;
--# derives State from State, X;
--# pre NotFull(State);
end Stack;
Where the stack is in the form of an abstract state machine a precondition can only be expressed if there is a suitable SPARK function available. In any case it would not be possible for users of the push operation to check that they met the precondition if such a function was not available. Here function NotFull has been declared and exported and the precondition of Push expressed in terms of the implicitly declared proof function associated with it. See section 3.3.1.2 for a discussion of implicitly declared proof functions.
The ability to announce abstract own variables as being of a named proof type may provide another means of expressing preconditions in this case; see section 3.3.3.2.
Where a formal parameter of a subprogram is an unconstrained array the size of the array is determined by the size of the actual parameter in the calling environment.
Checks on the validity of index expressions which are made inside the body of the subprogram will be in terms of constants representing ‘First and ‘Last of the actual constrained size of the array for a particular call. In general proof contexts have to written in terms of array attributes to be successful and not in terms of the unconstrained array index type.
Attributes such as ‘First, 'Last and ‘Length of the array will not have a constant value for proof purposes since the value will vary from call to call depending on the actual parameter passed.
For example:
|
type Atype is array(Integer range <>) of Integer;
|
|
|
procedure P(A : in out Atype) --# derives A from A; --# pre A’First <= 99 and --# A’Last >= 99; is ... ........A(99)......... ... end P; |
VCs for the index expression here will be a__index__subtype__1__first £ 99 £ a__index__subtype__1__last and in order to complete a general proof of the absence of run-time errors the pre condition in terms of A’First and A’Last is required. |
6.7.1.5 Strengthened Postcondition
When performing a Push operation using the stack package from section 6.7.1.2 we would have to show that the precondition — NotFull(State) — is true at the point of call. Given the code sequence:
...
Stack.Pop(TheStack, X);
...
Stack.Push(TheStack, Y);
....
We could obtain the necessary information by strengthening the postcondition of Pop as follows:
--# post NotFull(State);
which states that “a stack from which something has just been popped cannot be full”.
An alternative to strengthening the specification of a subprogram is to make it exception-free under all calling circumstances. This may involve the addition of checks in the form of conditional statements inside the subprogram to guard against error conditions. The use of conditionals in this way is sometimes known as defensive programming: the RTC VCs generated by the Examiner provide a focused way of applying this technique. Three examples of defensive programming, using the Inc subprogram of section 6.3 follow. In each case the addition of a guard on the statement which increments the variable X makes the subprogram free of run-time errors under all circumstances where it is successfully called.
6.7.2.1 Indicating failures to the calling environment
procedure Inc(X : in out T;
Overflow : out Boolean)
--# derives X, Overflow from X;
is
begin
if X = T’Last then
Overflow := True;
else
X := X + 1;
Overflow := False;
end if;
end Inc;
6.7.2.2 Diversion of control to an error handler
procedure Inc(X : in out T)
--# global ErrorHandler.State;
--# derives X, ErrorHandler.State from *, X;
is
begin
if X = T’Last then
ErrorHandler.FatalError(ErrorHandler.OverflowInInc);
else
X := X + 1;
end if;
end Inc;
6.7.2.3 Limiting or saturation of operations
procedure Inc(X : in out T)
--# derives X from X;
is
begin
if X < T’Last then
X := X + 1;
end if;
end Inc;
In some cases a potential run time error can be shown by system-level argument not to pose a risk in practice. Examples include counters that are incremented at a rate which precludes the possibility of overflow because the limit could not be reached during the life of the system. For example a counter in an aircraft system, implemented as a 32-bit integer and incremented once per second from a start value of zero, would take over 63 years to overflow; this is likely to exceed the maximum flight time (or even service life) of the aircraft! Such system-level arguments justify leaving a particular VC unproved; they should of course be carefully documented and form part of the safety justification for a system.
The validity of a proof constructed using the SPARK tools depends on some important assumptions and limitations; these are discussed below.
7.1 Absence of data-flow errors
It is essential that all variables referenced are given well-defined values before use; this condition is achieved if the program concerned is free from data flow errors. The data flow error messages which might invalidate run-time check generation are listed below. Of particular significance is the initialization of objects of structured types. The Examiner generates RTCs on the basis that all elements of such an object are defined and lie within the appropriate subtype range; this assumption is valid if the Examiner has not reported a data flow error because, for example, the object has been fully initialized with an aggregate. There are two common cases where the Examiner will report a data flow error in connection with structured objects and these require special care.
7.1.1 Array initialization in a loop
If an array is initialized in a loop, rather than with an aggregate, the Examiner will report a data flow error on the first write to the array. This is because the value of the array after the write is considered to be its value beforehand with one element overridden to a new value. Therefore the final value of the array depends on its initial value. Often this data flow error can safely be ignored provided all required elements of the array are actually correctly initialized. If the validity of the proof of absence of run-time errors is not to be compromised there is an obligation to show that the initialization is complete. It is recommended that array objects are initialized with an aggregate wherever possible.
7.1.2 Semantically unnecessary initialization
There are cases where the initialization of a structured object is unnecessary because of the way in which it will be used. For example, a stack might be implemented as an array and a stack pointer. Provided operations are limited to push and pop and that popping an empty stack is prohibited then the stack can safely be emptied by initializing the stack pointer without the need to write to all elements of the array. Any element of the array read by a pop operation must previously have been well-defined by a preceding push operation and the undefined array elements can never be accessed. If this approach is taken then there is an obligation to show that each array element is defined before it is accessed; the Examiner will continue to assume that all array elements are well-defined and will not provide automatic assistance in the discharge of this obligation.
7.1.3 Significant data-flow error messages
The following data error messages indicate errors which may invalidate the assumptions required for the effective generation of run-time checks. The messages are listed by their section and reference number in the Examiner User Manual [1].
· Section 8.3.1 Data-flow errors: errors 20, 23, 501, 504; these errors indicate the possible presence of random data values which invalidate the run-time checks for the subprogram in which they appear.
· When generating run-time checks involving procedure call statements, the Examiner assumes that exports from the called procedure are valid, in-type values. This assumption may be invalid if the called subprogram contains data flow errors of the kind listed in the previous bullet. Error 602 from Section 8.3.4 of [1] indicates that an export, which the Examiner assumes is valid, depends on some undefined (random) value.
· Section 8.3.5, Error 34 indicates that a parameter or global which has been identified as an import only has actually been redefined. Run-time checks of any caller of the subprogram which exhibits this error may be invalid.
· Section 8.3.6, Error 31 indicates that a parameter or global is an export of a subprogram but that it has not been given a value. Run-time checks of any caller may be invalid.
7.2 Assumption that called subprograms return
As described above, checks are generated for each subprogram call that imported actual parameters are in the range of the corresponding formals and meet any precondition applied to the called subprogram. On return, assumptions are provided that either the exported actual parameters or the function return value are in range. Any post condition or return annotation is also assumed to be satisfied by the imported and exported values. Implicit in these assumptions is that the called subprogram terminates. Generally a proof requires a bottom-up analysis with each subprogram being shown to satisfy its specification before checking uses of it. For instance, in checking for absence of run-time errors, the body of each subprogram must be shown to be exception-free (or adequately guarded against the calling conditions that would cause a run-time error) before checking uses of it.
7.3 Effects of concurrency when using RavenSPARK
Proof of absence of run-time errors is largely unaffected by concurrency; however, care is needed where multiple tasks communicate via shared data. This is especially true where the shared data is a protected variable of a pragma Atomic type. Consider the case where Task A generates shared data which Task B consumes. An error in task A, such as returning an invalid value form an external variable, may result in a run-time error occurring in Task B even though it has been possible to prove the body of Task B to be exception-free. In this case it will not have been possible to prove Task A to be free from errors. The situation is directly analogous to sequential code where a similar error in a called subprogram may be revealed by an exception in the caller. For sequential code we can protect against this by a bottom-up analysis as described in the preceding section. For concurrent programs we need to extend this to included not just called subprograms but concurrent tasks that share data. In the example given, we need to prove exception freedom for both task A and B to be sure that neither is adversely affected by the other.
Ada real number arithmetic is inexact. For this reason run-time checks for expressions and statements involving real numbers cannot be generated to the same degree of precision as for other scalar types. In particular, cumulative rounding errors may cause run-time errors to occur. The Examiner issues a warning when such expressions and statements are encountered.
Users for whom RTC proof involving real numbers is important should contact Altran Praxis for advice.
VCs cannot be generated for programs containing cyclic paths unless these are first “cut” with a suitable assertion in the form of a loop-invariant. Because the Examiner is intended to operate on code containing only the mandatory annotations of SPARK the required loop invariant may not be present. To enable generation of VCs to continue, the Examiner inserts a default loop invariant at the head of any loop in which a user-inserted assertion is not found. When this is done a suitable warning is issued stating where the assertion has been placed.
The default assertion states the subprogram’s precondition is satisfied (decorating variables which are both imported and exported with ~ to show that the precondition is satisfied in terms of the their initial values) and that any imported variables were within their types on entry to the subprogram. If the subprogram does not use unchecked conversions or directly read an external variable and there are no data-flow errors of the sort described in section 7.1.3, local variables of the subprogram are considered to be in-type. In the case of for loops, the invariant also states that the loop counter is in its subtype. If a subprogram has neither precondition nor imports or suitable local variables, the default assertion reduces to “true”.
There are two limitations concerning the automatic cutting of loops: incorrect detection of an uncut cyclic path, and the incomplete propagation of information through an assertion. The last of these applies wherever an assertion occurs and is covered later in this section.
The Examiner uses a simple search of the syntax tree to try to find a user-supplied loop-invariant, stopping as soon as one is found. Nested loops are not entered in order to prevent a loop-invariant in an inner loop obscuring the need for one on the outer loop. This simple mechanism should provide the desired behaviour for most common situations; however, there are two situations in which the user needs to be careful.
7.5.2 Failure to detect an uncut cyclic path
The first situation occurs when a loop contains an assertion but this does not cut all possible paths through the loop body as shown in the example below. The simple search will find the assertion in the body of the loop but does not know that it does not cover all possible paths within the loop so no default assertion will be inserted. If this occurs the VC file for the subprogram concerned will contain an error message as described in [1].
while i < 10
loop
if j > 5 then
j := j + 1;
else
--# assert j < 20;
j := j + 2;
end if;
i := i + 1;
end loop;
7.5.3 Insertion of an unnecessary assertion
The second situation involves user-supplied assertions within nested loops which occur before any exit conditions of the inner loop as in the example below. The simple search does not enter the inner loop and will not find the user-supplied assertion so adds a default assertion at the outer loop head; however, this addition is strictly unnecessary since the position of the user-supplied assertion is such as to cut all paths through both the inner and outer loop. Note that a warning message is always generated when a default assertion is inserted.
while i < 10
loop
loop
--# assert j < 20;
j := j + 1;
exit when j > 10;
end loop;
i := i + 1;
end loop;
7.6 Incomplete propagation of information through asserts
Because an assertion is considered as a cut in the control flow graph of a subprogram, information known before the assertion is not known after it. A discussion of this can be found in section 3.5.1. Where there is a user-supplied loop cutting assertion the Examiner will conjoin with it the type and precondition information used as the default assertion which was described in section 7.5.1. Where this information is insufficient to prove VCs occurring after the assertion it will be necessary to strengthen it appropriately. In the case of an automatically-inserted, default assertion it may be necessary to replace it with a suitable user-supplied one.
The Examiner generates replacement rules enabling the Simplifier to reason about properties of user-defined types such as their bounds. Rules cannot be generated for predefined types such as integer because their bounds are compiler dependent and are consequently not visible to the Examiner. Where a SPARK source makes use of predefined types the Simplifier may not be able to prove the VCs that result. It is possible to obtain values for the bounds of predefined types from the compiler and make them available to the Examiner using a configuration file for the target platform as described in [1].
7.8 Package initialization parts
The Examiner does not generate VCs for package initialization parts. Statically-determinable constraint errors will be detected during well-formation checking of package initialization.
7.9 Aggregates of multi-dimensional arrays
VCs cannot be generated from aggregates of multi-dimensional arrays. The Examiner issues a suitable warning when this is attempted but still generates VCs. VCs associated with the aggregate will contain references to an identifier unknown_cell_kind, or an illegal Prolog variable, which will cause the Simplifier to report type checking failures.
8 The Representation of SPARK in FDL
When producing VCs the Examiner maps SPARK language constructs (including proof contexts) into their FDL equivalents, which then appear in the VC output files. This section describes the details of this mapping from SPARK to FDL.
All literals are converted by removing any underscores within them, converting to base 10 and removing any exponent.
Example:
16#FFFF_FFFF# becomes 4294967295
1e3 becomes 1000
Real literals are represented as a rational pair; if the divisor is 1 it is omitted.
Examples:
0.5 becomes (1/2)
1.0e3 becomes 1000
SPARK identifiers are represented in FDL by mapping them to lower case and replacing the dot in any package prefix by a double underscore.
Examples:
Speed becomes speed
Air_Speed becomes air_speed
Doppler.GroundSpeed becomes doppler_ _groundspeed
(Doppler is the name of the package from which GroundSpeed is being selected)
(Suitable FDL declarations for these newly-created identifiers are generated and placed in the FDL file automatically by the Examiner.)
The FDL type system is simpler than that of SPARK. The FDL equivalent of SPARK's types are as follows:
Integer types. All integer types from the program being modelled are treated as being of FDL's integer type which behave as integers in the mathematical sense. Checking that the values of these integers remain within the bounds of their original SPARK types is achieved by proof of the RTC VCs generated by the Examiner.
Real types. All SPARK fixed and floating point types are modelled as FDL real numbers; again these behave as the mathematical real numbers. The semantics of real, especially floating-point, arithmetic are such as to make the proof process difficult or impossible. The following warning is issued at the end of each subprogram where such expressions have been found:
--- VCs for statements including real numbers are approximate
Enumeration types. SPARK's enumeration types are directly replaced by their FDL equivalents. Suitable declarations are placed in FDL file. Note that enumeration literals declared in other packages will each be prefixed by their package name and two underscores.
Array types. SPARK arrays are represented by directly-equivalent FDL arrays. Suitable FDL declarations are automatically produced. Access to and updating of elements of array objects is modelled by predefined FDL functions.
Record types. SPARK records are represented by directly-equivalent FDL records. Suitable FDL declarations are automatically produced. Access to and updating of fields of record objects is modelled by predefined FDL functions.
Tagged records. The modelling of inherited fields in extended record types is modelled explicitly using a field called “inherit” in the FDL records used. For example, given the Ada declarations:
type PT is tagged record -- in package P
X, Y : Integer;
end record;
type QT is new PT with record -- in package Q
B : Boolean;
end record;
type RT is new QT with record -- in package R
F : Float;
I : Integer;
N : Natural;
end record;
the FDL equivalent is:
type p__pt = record
x, y : integer
end record;
type q__qt = record
inherit : p__pt;
b : boolean
end record;
type rt = record
inherit : q__qt;
f : float;
i : integer;
n : natural
end record;
8.4.1 Arrays access and update
The declaration of array type A introduces element and update functions as described in the chapter on FDL. Thus for instance, the SPARK statement
M(I, J) := M(J, K) + 2;
is modelled by
m := update(m, [i, j], element(m, [j, k]) + 2);
It is worth emphasising the different way in which multi-dimensional arrays and arrays of arrays are handled using this notation.
Multi-dimensional arrays: Arr(I, J) becomes element(arr, [i, j]).
Array of arrays: Arr(I)(J) becomes element(element(arr, [i]),[j]) which can be read as element j of the array which is element i of array arr.
(Although SPARK supports the declaration of multi-dimensional arrays and aggregates of them it is recommended that arrays of arrays are used in preference to them at present where proof is to be attempted.)
The declaration of a record type R introduces field access and update functions as described in the chapter on FDL. The following example illustrates their use to model SPARK record operations.
Example: Given the SPARK declaration of the record-type Date
type DayNumber is 1 .. 31;
type MonthName is
(Jan,Feb,Mar,Apr,May,Jun,Jul,Aug,Sep,Oct,Nov,Dec);
type YearNumber is 0 .. 2000;
type Date is record
Day : DayNumber;
Month : MonthName;
Year : YearNumber
end record;
the following FDL functions are implicitly declared
function fld_day(date) : daynumber;
function upf_day(date, daynumber) : date;
function fld_month(date) : monthname;
function upf_month(date, monthname) : date;
function fld_year(date) : yearnumber;
function upf_year(date, yearnumber) : date;
The extraction and assignment of field values, for records of type Date, is illustrated by the following:
mon := fld_month(dat); {SPARK equivalent: Mon := Dat.Month;}
dat := upf_day(dat, 14); {SPARK equivalent: Dat.Day := 14; }
dat := upf_month(dat, jul); {SPARK equivalent: Dat.Month := Jul; }
dat := upf_year(dat, 1789); {SPARK equivalent: Dat.Year := 1789; }
A SPARK array aggregate, using either named or positional association, is represented in FDL by its mk__ function which is implicitly declared for each array type. The arguments of this function are read from left to right with any default value arising from a SPARK others => clause appearing as first argument, followed by a sequence of value assignments.
8.4.3.1 Named association
When named association is used, the associations given in the SPARK aggregate are directly mapped on to the arguments of the mk__ function. For example, given
type Index is 1..4;
type A is array(Index) of Integer;
A'(1=>1,2=>2,3=>3,4=>4) becomes mk__a([1]:=1, [2]:=2, [3]:=3, [4]:=4)
A'(1 => 1, others => 0) becomes mk__a(0, [1]:=1)
A'(others => 0) becomes mk__a(0)
A'(Index => 0) becomes mk__a([index__first .. (index__last)]
:= 0)
A'(Index range 1..4 => 0 becomes mk__a([1 .. 4] := 0)
A'(1..4 => 0) becomes mk__a([1 .. 4] := 0)
A'(1 | 2 | 3 | 4 => 0) becomes mk__a([1] & [2] & [3] & [4] := 0)
8.4.3.2 Positional association
When positional association is used, the arguments needed by the mk__ function are constructed as expressions based on the bounds of the index type and the element's position number. Given the same declarations as above
A'(1, 2, 3, 4) becomes mk__a([index__first]:=1,
[index__first+1]:=2,
[index__first+2]:=3,
[index__first+3]:=4)
which the Simplifier will reduce, given the value of index__first which it reads from the rule-file generated by the Examiner, to
mk__a([1]:=1, [2]:=2, [3]:=3, [4]:=4)
If the Index type were instead
type Index is (red, yellow, green, blue)
then
A'(1, 2, 3, 4) would become
mk__a([index__first]:=1,
[succ(index__first)]:=2,
[succ(succ(index__first))]:=3,
[succ(succ(succ(index__first)))]:=4)
which the Simplifier will reduce, using its knowledge of the enumeration type and the succ function and again using the value of index__first from the rule-file generated by the Examiner, to
mk__a([red]:=1, [yellow]:=2, [green]:=3, [blue]:=4)
8.4.3.3 Unconstrained array aggregates
The unqualified array aggregate in an unconstrained array assignment is modelled in the same way as for a normal, qualified, array aggregate. So in the context of an assignment involving an unconstrained array of Integers named T:
(others => 0) becomes mk__t(0)
Unconstrained array aggregates may appear in annotations, in which case they must be qualified with a type mark, thus:
T’(others => 0) becomes mk__t(0)
8.4.4 Record aggregates
Record aggregates behave very much in the same way as the arrays described above but are simpler because they may not contain others clauses, ranges or choices: each field simply appears once either by name or by position. An FDL mk__ function is implicitly declared for each record type.
For example, given
type R is record
B1,
B2 : Boolean;
I : Integer;
end record;
the record aggregates
R'(B1 => True, B2 => False, I => 0);
R'(True, False, 0);
both become
mk__r(b1 := true, b2 := false, i := 0)
Where aggregates and extension aggregates involving extended records are used, the FDL model will make use of the “inherit” fields described in Section 8.3.
8.4.5 Attributes
SPARK attributes are handled in one of three ways, considered below. The Examiner also generates proof rules to express properties of attributes and these are also described below.
8.4.5.1 Attributes ’Succ and ’Pred
'succ and 'pred of numeric types are modelled using addition and subtraction. For enumerated types, the attribute is mapped directly on to its FDL equivalent functions succ and pred. Given the declarations
type Int is range 1..10;
type Colour is (Red, Yellow, Green);
the attribute expressions
Int'Succ(X);
Colour'Succ(Y);
are respectively represented by
x + 1
succ(y)
8.4.5.2 Constant attributes
Attributes which return a constant value such as 'first are replaced with an FDL constant for which a suitable declaration is placed in the .FDL file. The constant name is created by joining the attribute prefix and attribute identifier together with a double underbar character. Thus Colour'First becomes colour__first. Where the value of this constant can be determined by the Examiner a suitable replacement rule is written to the .RLS file.
Function attributes such as 'pos are replaced with an FDL function for which a suitable declaration is placed in the .FDL file. The function name is created by joining the attribute prefix and attribute identifier together with a double underbar character. Thus Colour'Pos(Red) becomes colour__pos(red). The same representation is used for both Ada function attributes and the SPARK proof attributes 'Append and 'Tail (see Section 3.3.1.3).
In SPARK2005 the Examiner, for a numeric type S, models the functional attribute S’Mod (<Universal Integer>) as <universal Integer> mod S’Modulus.
8.4.5.4 Enumeration proof rules
For enumeration types the Examiner automatically generates a number of proof rules that are written to the .RLS file. These rules embody properties of various attributes, such as the result of combining 'succ or 'pred with 'pos or 'val.
8.4.6 Operators
Most SPARK operators have an FDL equivalent; however, there are some differences including differences in operator precedence. These are illustrated below. Given X and Y of a numeric type, I and J of an integer type and A and B of Boolean type,
|
abs X + Y
|
becomes |
abs(x) + y |
(abs is a function in FDL not an operator) |
|
I / J
|
becomes |
i div j |
(remains x / y for real types) |
|
I rem J
|
becomes |
i - i div j * j |
(FDL does not have the rem operator) |
|
X /= Y
|
becomes |
x <> y |
|
|
not A = B
|
becomes |
(not a) = b |
(not binds more loosely in FDL than in SPARK) |
|
A xor B
|
becomes |
(a or b) and (not (a and b)) |
(FDL does not have the xor operator) |
Modular types become normal integers in FDL. To capture the modular behaviour of their operators, a suitable mod operator is appended to all expressions involving such types. For example, if X and Y are variables of a modular type T then the SPARK expression X + Y becomes (x + y) mod t__modulus in FDL.
Modular types also allow use of bitwise binary operators (and, or and xor); these are modelled using FDL functions bit__and, bit__or and bit__xor. These general functions are used for all modular types. Unary bitwise “not X” for a modular type T is modelled as T’Last - X.
Logical operators between one-dimensional arrays of Booleans also have an FDL equivalent. For a given SPARK Boolean array type, each of the logical operators (not, and, or and xor) is modelled as an FDL function that takes argument(s) of the SPARK type and returns a Boolean array of the same type. The names of the FDL functions are formed by appending ‘_ _ op’ (where op is one of: not, and, or, xor) to the array type name. The Examiner also automatically generates a proof rule for each function, which defines the value of elements of the array returned by the function. These proof rules are written to the .RLS file.
Given two one-dimensional Boolean arrays A and B of SPARK type BoolArrayT (whose index type’s first and last elements are l and u), the following table lists the FDL translation of the various array operators, together with the associated proof rules.
|
SPARK |
FDL Translation |
Proof Rule for FDL Function |
|
not A
|
boolarrayt__not(a) |
element(boolarrayt__not(X), [I]) may_be_replaced_by not element(X, [I]) if [l <= I, I <= u] |
|
A and B
|
boolarrayt__and(a,b) |
element(boolarrayt__and(X,Y), [I]) may_be_replaced_by element(X, [I]) and element(Y, [I]) if [l <= I, I <= u] |
|
A or B
|
boolarrayt__or(a,b) |
element(boolarrayt__or(X,Y), [I]) may_be_replaced_by element(X, [I]) or element(Y, [I]) if [l <= I, I <= u] |
|
A xor B
|
boolarrayt__xor(a,b) |
element(boolarrayt__xor(X,Y), [I]) may_be_replaced_by (element(X, [I]) or element(Y, [I])) and (not (element(X, [I]) and element(Y, [I]))) if [l <= I, I <= u] |
Care must be taken when using the binary Boolean-array and modular bitwise operators (and, or and xor) in SPARK proof contexts. This is because the binding powers of the operators, and the overloading of ‘and’ and ‘or’ with logical operators on predicates, can result in the Examiner wrongly treating operators as operators on predicates, depending on the use of parentheses. For example, if A, B and C are all Boolean arrays of the same type, then a postcondition of:
--# post A = B and C;
will be parsed by the Examiner as:
--# post (A = B) and C;
resulting in a semantic error (as there is no operator ‘and’ between predicates and Boolean arrays that returns a predicate!). To specify the intended postcondition, that A is the pairwise-conjunction of the two arrays B and C, the user must write:
--# post A = (B and C);
Note that the above problem does not arise with the unary operator not, as it binds very tightly and so there is no problem of ambiguity.
8.4.7 Short-circuit forms
The SPARK short-circuit forms of conjunction and disjunction and then and or else are replaced in FDL with their logical equivalents and and or. (For proof of absence of run-time errors, the short-circuit forms are not directly equivalent because the second half of the expression may not be evaluated; however, the Examiner inserts the correct check statements in these cases) .
As in Ada, a membership test, in and not in, is either a range membership test, expressed in terms of the lower and upper bounds of a range, or it is a subtype membership test, with a typemark. In the verification conditions produced by the Examiner, a membership test is always expressed in terms of two inequalities, relating the value of the simple expression of the membership test to the least and greatest values of the range (or type). For example
|
X in Itype; |
becomes |
(x >= itype__first) and (x <= itype__last) |
|
X in 3..7; |
becomes |
(x >= 3) and (x <= 7) |
|
Y in Etype; |
becomes |
(y >= etype__first) and (y <= etype__last) |
|
Y in red..yellow; |
becomes |
(y >= red) and (y <= yellow) |
|
X not in Itype; |
becomes |
(x < itype__first) or (x > itype__last) |
|
X not in 3..7; |
becomes |
(x < 3) or (x > 7) |
|
Y not in Etype; |
becomes |
(y < etype__first) or (y > etype__last) |
|
Y not in red..yellow; |
becomes |
(y < red) or (y > yellow) |
SPARK functions may reference (but not update) global data whereas FDL functions are pure functions in the mathematical sense. To enable the modelling of SPARK functions with globals in FDL the Examiner implicitly declares an FDL proof function for each SPARK function in the source text. The signature of this implicitly declared proof function contains all the arguments of its matching SPARK function followed by an additional argument for each global referenced by the SPARK function. Because the rules of SPARK prevent functions having side-effects the SPARK function and the implicitly declared proof function are in precise correspondence for number and type of data objects read and returned.
For example, given the SPARK function declaration
function Add(X : Integer) return Integer;
--# global Increment;
the call Add(X); becomes Add(x, increment);.
For VC generation a function call is modelled by:
1 a check statement to show that all actual parameters are in-in type (global variables of a function are assumed to be in-type as they are checked prior to the function call;
2 a check statement to show that the pre-condition of the called function is satisfied by the actual parameters used and the current values of the called function’s global variables;
3 an assumption that the returned value is in-type; and
4 an assumption (which appears in the hypotheses of VCs for paths which traverse the function call) that the function’s return annotation holds for the given actual parameters including global variables.
For example the following function declaration, F1, with an explicit return annotation gives the VCs shown when it is called by function F2.
function F1 (X : Integer) return Integer;
--# pre X * X <= Integer'Last and
--# X * X >= 0 ;
--# return X * X;
6 function F2 ( Y : Integer) return Integer;
7 --# pre Y * Y <= Integer'Last and
8 --# Y * Y >= 0;
9 --# return Y * Y
10 begin
11 return F1 (Y);
12 end F2;
For path(s) from start to precondition check associated with statement of line 11:
function_f2_1.
H1: y * y <= integer__last .
H2: y * y >= 0 .
H3: y >= integer__first .
H4: y <= integer__last .
->
C1: y * y <= integer__last .
C2: y * y >= 0 .
C3: y >= integer__first .
C4: y <= integer__last .
For path(s) from start to finish:
function_f2_2.
H1: y * y <= integer__last .
H2: y * y >= 0 .
H3: y >= integer__first .
H4: y <= integer__last .
H5: y * y <= integer__last .
H6: y * y >= 0 .
H7: y >= integer__first .
H8: y <= integer__last .
H9: f1(y) >= integer__first .
H10: f1(y) <= integer__last .
H11: f1(y) = y * y .
->
C1: f1(y) = y * y .
C2: f1(y) >= integer__first .
C3: f1(y) <= integer__last .
In VC f2_1 the conclusions C1 and C2 are derived from the check of the pre conditions of F1 and C3 from the check that the actual parameter, Y, is in-type. This VC has to be proved to show that the preconditions of F1 are satisfied by this call.
The hypotheses in VC f2_2; H3 and H4 follow from the in-type check of the actual parameter Y, H5 and H6 follow from the precondition check for the call to F1, H9 and H10 are the assumptions that the returned value from F1 is in-type and H11 is the assumption that the return annotation of F1 is satisfied.
The facility for declaring different integer types and subtypes in Ada (and SPARK) provides protection through two quite different forms of type-checking. Firstly, we have rules of type consistency such as the rule that, in an assignment statement, the type of the expression must be the same as the (base) type of the assigned variable. Compliance with such static-semantic rules is checked by the Examiner, as it parses a text. (Such checks are also performed, prior to code generation, by compilers).
The other important aspect of the integer types and subtypes is that they impose range constraints on the values of variables — which values could in other respects be considered as all belonging to the same predefined integer type.
A type conversion — between integer types or subtypes — whilst it may be important to meeting static-semantic rules, is of no relevance to a partial proof of correctness of an algorithm where we assume that the program terminates normally and therefore that all values have remained within their permitted bounds. Where we wish to show that this is indeed the case, we must take into account the constraint introduced by the type conversion; the proof obligations associated with it are automatically inserted by the Examiner.
Type conversions between different real types, or between real types and integer types and subtypes, are more complex. At present, the Examiner ignores the semantic effects of type conversions between different real types. For conversion from a real type to an integer type the Examiner inserts an application of the proof function round__(real) : integer; this records the fact that such a conversion takes place, but it should be noted that it does not capture the full semantics of the conversion for the particular real types involved.
8.4.11 Quantified expressions
SPARK quantified expressions (see Section 3.2.3) are simply translated to the corresponding FDL quantified expressions (see Section 4.4.3). However, FDL quantified expressions do not include range constraints on the type of the quantified variable, so any SPARK range constraints are converted into predicates as follows.
|
A SPARK quantifier of the form for some x in atype range l..u => (E)
|
is translated into FDL as for_some (x_ : atype, l <= x_ and x_ <= u and E_)†
|
|
A SPARK quantifier of the form for all x in atype range l..u => (E) |
is translated into FDL as for_all (x_ : atype, (l <= x_ and x_ <= u) -> E_)†
|
† Where E_ is E with all occurrences of x replaced by x_
Note that the names of the FDL quantified variables end with an underscore: ‘_’. This ensures that the quantified variable names are distinct from all Ada names and so avoids the possibility of any name clashes occurring (when SPARK proof annotations are hoisted through code to generate VCs).
For semantic analysis, the for-loop and while-loop iteration schemes are treated as follows.
|
A while-loop of the form while E loop S; end loop; |
is treated as loop exit when not E; S; end loop; |
|
A for-loop of the form for I in atype range L..U loop S; end loop;
|
is treated as if L <= U then I := L; loop S; exit when I = U[10]; I := I + 1; -- or ‘succ for enumerations end loop; end if; |
|
A for-loop of the form for I in atype loop S; end loop;
|
is treated as I := L; loop S; exit when I = U; I := I + 1; -- or ‘succ for enumerations end loop; because SPARK does not allow a type to be empty. |
|
A for-loop of the form for I in reverse atype range L..U loop S; end loop;
|
is treated as if L <= U then I := U; loop S; exit when I = L; I := I - 1; -- or ‘pred for enumerations end loop; end if; |
|
A for-loop of the form for I in Boolean loop S; end loop; |
is treated as I := False; loop S; exit when I; -- that is, I = True I := not I; end loop; because SPARK does not allow ordering of Booleans |
|
A plain loop of the form loop S; end loop; |
is treated as loop S; exit when False; end loop; ; to provide a syntactic exit point for flow analysis purposes |
Thus, viewing the above models it is apparent that two of the four for-loop constructs have a syntactically-possible path through them (when L > U) in which the loop-body is not executed (and similarly, though more obviously, for the while-loop). Such paths are reflected in verification conditions for code containing such loop constructs.
8.4.13 Expression ordering
For VCs associated with overflow checks it is important to know the order in which sub-expressions are evaluated. A compiler is permitted to re-order expressions containing operators of equal precedence even if a run-time error results. The Examiner assumes left to right evaluation of such expressions but issues a warning if it detects an expression vulnerable to re-ordering. Such expressions should be parenthesised to avoid the possibility of re-ordering.
--- This expression may be re-ordered by a compiler.
Left to right
evaluation was assumed for RTC generation.
When generating VCs, a call to a procedure is modelled as
1 a check statement to show that the pre-condition of the called procedure is satisfied by the actual parameters used and the current values of imported global variables;
2 a series of assignments to each of the exports from the procedure; and
3 an assumption (which appears in the hypotheses of VCs for paths which traverse the procedure call) that the procedure's post condition holds for the actual parameters returned and the values of exported global variables.
The Examiner automatically creates new unique identifiers to represent the return value of each export and it is these identifiers which are substituted into the post condition expression to generate the assumption described in point 3 above. The names are generated by appending a double underscore character and a number to the identifier concerned.
For example the following code shows a simple procedure which doubles its integer parameter. This procedure is used to define another procedure, which multiplies its parameter by four.
8 procedure Double(X : in out Integer)
9 --# derives X from X;
10 --# post X = X~ * 2;
11 is
12 begin
13 X := X * 2;
14 end Double;
15
16 procedure Quad(X : in out Integer)
17 --# derives X from X;
18 --# post X = X~ * 4;
19 is
20 begin
21 Double(X);
22 Double(X);
23 end Quad;
The VCs generated for procedure Quad are as follows:
For path(s) from start to finish:
procedure_quad_1.
H1: true .
H2: x >= integer__first .
H3: x <= integer__last .
H4: x__1 = x * 2 .
H5: x__2 = x__1 * 2 .
->
C1: x__2 = x * 4 .
The VC shows the procedure export variables generated by the Examiner to model the effect of calls to procedure Double: x__1 is the value of X returned by the first call to Double and x__2 that by the second call. The hypotheses of the third VC are generated by the substitution of these variables into the post-condition of Double and the conclusion to be proved is the post-condition of Quad. The hypotheses also include information about the imports to Quad deduced from the Ada type system; in this case that X is in the permitted range of integer. Note that additional VCs would be generated if procedure Double had any precondition that needed to be checked prior to the call.
8.6 Refinement integrity VC generation
This section gives a comprehensive description of refinement VCs. It defines the:
1. built-in refinement abstraction relation;
2. generation of implicit proof functions for Ada functions;
3. precondition refinement integrity VC;
4. postcondition refinement integrity VC;
5. return annotation refinement integrity VC;
6. nested refinement resulting from embedded and/or child packages.
7. generation of refinement VCs for private types.
Unless otherwise explicitly stated, the contents of this section apply equally to SPARK83, SPARK95, and SPARK2005.
8.6.1 Built-in refinement abstraction relation
An abstraction relation specifies the formal relationship between abstract and concrete variables. With an own variable of an abstract proof type the Examiner provides a fixed abstraction relation, for refinement VCs internal to the package. The abstract proof type is modelled in FDL as a record, with one field for each of the variables that the abstract own variable is refined by.
So given a package specification that includes:
package P
--# own X : XType;
is
--# type XType is abstract;
...
and a corresponding own variable annotation in the package body of:
--# own X is X1, X2, ... Xn;
the Examiner generates the following FDL declaration:
type xtype = record
x1 : x1type;
x2 : x2type;
...
xn : xntype
end;
For each refinement VC the Examiner includes hypotheses to make the formal link between abstract and concrete variables. These hypotheses are equality predicates written in terms of the concrete variables and take the following form:
x1~ = fld_x1(x~) . (<-> is used in place of = if the fields are Boolean)
x1 = fld_x1(x) .
...
8.6.2 Implicit proof functions for Ada functions
The refinement of Ada functions raises a complication when generating the corresponding implicit proof functions. Namely that the implicit proof function for an Ada function (say P.Fn) can have a different type in the package specification and body. For example, in P’s specification Fn’s global list may include an abstract variable A, whereas in the body its global list may include a concrete variable C1. Hence the type of the own variable argument, to the corresponding implicit proof function, is different in each case. In fact even the number of arguments could change (eg if Fn in its implementation reads more than one of the concrete variables that A is refined by).
Furthermore, in the body of a package both the abstract and concrete forms of an Ada function’s implicit proof function may be in scope at the same time. For example, a procedure may use respectively the abstract and concrete versions of an Ada function in the procedure’s abstract and concrete preconditions. Consequently, the weaken precondition refinement VC for the procedure needs to refer to both abstract and concrete forms of the implicit proof function.
The solution to this is to distinguish the abstract proof function in the package body by always using the package name as a prefix. Hence, the abstract implicit proof function of a package P’s Ada function Fn, always appears in VCs as ‘p__fn’ (even in VCs internal to the package P). Conversely, the concrete implicit proof function always appears in VCs as just ‘fn’.
8.6.3 Precondition refinement integrity VC
A precondition refinement VC is generated for every subprogram that imports or exports an abstract own variable. The VC is simply that the abstract precondition implies the concrete precondition, with the additional hypotheses from the abstraction relation for the imported variables. So the precondition refinement VC takes the following form:
H1: abstract precondition .
H?: imported abstraction relation hypotheses .
->
C1: concrete precondition .
(Note that for clarity we have omitted the standard ‘variables in type’ hypotheses.)
8.6.4 Postcondition refinement integrity VC
A postcondition refinement VC is generated for every procedure that imports or exports an abstract own variable. The VC is basically that the concrete postcondition implies the abstract postcondition. However, there are additional hypotheses for:
· the abstract and concrete preconditions;
· the abstraction relations for the imported and exported variables.
So the postcondition refinement VC takes the following form:
H1: abstract precondition .
H?: concrete precondition .
H?: imported abstraction relation hypotheses .
H?: exported abstraction relation hypotheses .
H?: concrete postcondition .
->
C1: abstract postcondition .
(Again for clarity we have omitted the standard ‘variables in type’ hypotheses.)
8.6.5 Return annotation refinement integrity VC
A return annotation refinement VC is generated for every function that imports an abstract own variable. Such VCs are similar to postcondition refinement VCs, but are different for the following reasons:
· functions have no exports so there are no abstraction relation hypotheses for exported variables;
· both abstract and concrete forms of an implicit proof function return a variable of the same type (unlike abstract and concrete forms of procedures that export variables of different types);
· return annotations can be either explicit or implicit (or indeed omitted) so an appropriate predicate (loosely equivalent to a procedure's postcondition) has to be constructed, depending on the form of annotation.
The basic form of a return annotation refinement VC is that whatever constraints are placed on the function’s return value by the concrete annotation, they must be sufficient to establish any constraints placed on the return value by the abstract annotation. So the return annotation refinement VC takes the following form:
H1: abstract precondition .
H?: concrete precondition .
H?: imported abstraction relation hypotheses .
H?: concrete return annotation predicate .
->
C1: abstract return annotation predicate .
(Again for clarity we have omitted the standard ‘variables in type’ hypotheses.)
It remains to define what the return annotation predicates are in the VC. For both the abstract and concrete return annotations there are three cases, depending on the form of the annotation.
1 If an annotation is omitted then the return annotation predicate is ‘true’.
2 If an annotation is an explicit return annotation of the form:
--# return Exp;
then the return annotation predicate is ‘return = Exp’, where ‘return’ is an FDL variable (see below).
3 If an annotation is an implicit return annotation of the form:
--# return E => Pred (..., E, ...);
then the return annotation predicate is ‘Pred (..., return, ...)’ (ie the predicate from the annotation, with all instances of E replaced by return).
Note that the Examiner automatically generates an FDL declaration of the variable ‘return’, whose type matches the return type of the Ada function. This variable is used (as appropriate) in both the concrete and abstract return annotation predicates, to make the formal link in the refinement VC between the constraints specified by the two return annotations (ie both return annotations specify constraints on the same return value). ‘return’ is used as the variable name as it is a reserved word of SPARK. This guarantees that there is no possibility of the name clashing with any identifiers from the SPARK code.
A useful technique is to use a function’s implicitly-declared proof function as its abstract return annotation (see section 3.4.2) together with some more specific concrete annotation in the package body. For example:
package R
--# own State;
--# initializes State ;
is
function Extract return Integer;
--# global State;
--# return Extract (State); -- implicit proof function
end R;
package body R
--# own State is X;
is
X : Integer := 0;
function Extract return Integer
--# global X;
--# return X; -- refined return annotation
is
begin
return X;
end Extract;
end R;
The refinement proof will be of the form:
function_extract_3.
H?: x = fld_x(state) .
H?: return = x .
->
C1: return = r__extract(state) .
Which can be proved by providing suitable proof rules for implicit proof function r__extract. This technique does not directly simplify reasoning about external uses of function Extract because proof rules written in terms of package R’s abstract state will be needed for this purpose; however, it will clarify the relationship between the abstract and refined state and make those rules easier to formulate and understand. Advice on refinement proof rules is at section 10.7.5.
8.6.6 Nested refinement resulting from embedded and/or child packages
An abstract own variable (P.X, say) may be refined to variables of embedded, private child or the parent of public child packages. If the variables of the embedded/child/parent packages are concrete then the refinement proofs work exactly as described above (see also the stack example in section 10.6). This is because within the body of package P, the types of the concrete variables can be made visible (if necessary by using type announcement in the embedded/child/parent packages) and hence VCG within P works as already described.
If some of the variables of the embedded/child/parent packages are also abstract, then a nested refinement results. Within P, a record type is created for X and the types of the appropriate components are abstract (as is the type of X external to P). Reasoning about these components within P is conceptually no different from reasoning about P.X external to P. Hence, within P the user proof rules (which define the abstract proof functions relating to X) simply refer to proof functions of the embedded/child/ parent packages that characterise the abstract components of X.
8.6.7 Private type refinement
The preceding parts of section 8.6 describe own variable refinement proofs. The situation for private type refinement is essentially the same except that there is no refinement abstraction relation (as described in 8.6.1) because the same variables appear in both the abstract and refined view.
A simple example of abstract type refinement follows:
package P
is
type T is private;
-- proof functions on the private type
--# function IsValid (X : T) return Boolean;
--# function IntValOf (X : T) return Integer;
procedure Get (X : in T;
Y : out Integer);
--# derives Y from X;
--# pre IsValid (X); -- abstract constraint
--# post Y = IntValOf (X);
private
type T is record
Valid : Boolean;
Value : Integer;
end record;
end P;
package body P
is
procedure Get (X : in T;
Y : out Integer)
-- a second flow relation is neither required nor allowed
--# pre X.Valid; -- concrete constraint
--# post Y = X.Value;
is
begin
Y := X.Value;
end Get;
end P;
Calls to get from outside package P will use the abstract constraint; those from inside will use the concrete (refined) one.
The VCs generated for Get are as follows (standard ‘variables in type’ hypotheses have been omitted):
For path(s) from start to finish:
procedure_get_1.
H1: fld_valid(x) .
->
C1: fld_value(x) = fld_value(x) .
For checks of refinement integrity:
procedure_get_2.
H1: isvalid(x) .
->
C1: fld_valid(x) .
procedure_get_3.
H1: isvalid(x) .
H2: fld_valid(x) .
H3: y = fld_value(x) .
->
C1: y = intvalof(x) .
8.7 Simplification of trivially true VCs by the Examiner
It is quite common for VCs to have a conclusion of true, eg when generating run-time check (RTC) VCs for code that does not have pre- or postconditions. However, the hypotheses of such VCs can still be very large so we often get VCs of the form:
a_very_long_list_of_hypotheses
->
true .
Although the Simplifier readily discharges the proof
obligation, it has to read and parse the long list of hypotheses before finding
they are not needed; this wastes a significant amount of time. The Examiner
identifies such trivially true VCs and replaces the whole VC with:
*** true . /* trivially true VC removed by Examiner */
This format is recognised by the Simplifier, which does not process the VC further.
8.8 Traceability between VCs and their source
To enable the comparison of VCs against the corresponding source code, the Examiner inserts traceability comments in VC files that state what the ‘kinds’ of VCs are and which portions of the code they are generated from.
The Examiner generates a VC for each path between two cutpoints (see Section 2.4). The VCs for all the paths between two cutpoints are grouped together, with a single comment before them that has the general form:
For path(s) from XXX to YYY:
where XXX and YYY denote the proof contexts of the two cutpoints. The following table lists the possible values of XXX (with explanations).
|
start |
proof context at the start of the subprogram, ie its precondition |
|
assertion of line NN |
user-defined assert statement at line NN |
|
default assertion of line NN |
loop invariant assert statement inserted by the Examiner, at line NN, for RTC VCs |
The following table lists the possible values of YYY (with explanations).
|
assertion of line NN |
user-defined assert statement at line NN |
|
default assertion of line NN |
loop invariant assert statement inserted by the Examiner, at line NN, for RTC VCs |
|
check associated with statement of line NN |
user-defined check statement at line NN |
|
run-time check associated with statement of line NN |
Examiner generated check statement for a RTC VC for a SPARK statement at line NN |
|
precondition check associated with statement of line NN |
precondition of the subprogram called at line NN |
|
finish |
proof context at the end of the subprogram, ie its postcondition or return annotation |
The sole exceptions to the above traceability commenting of VCs are as follows:
Refinement integrity VCs (whose cutpoints are the abstract and concrete proof contexts of subprograms). The pair of refinement VCs for a single subprogram is prefixed by the comment:
For checks of refinement integrity:
Extended , tagged type subtype checks as described in Section 2.8.5.1 and illustrated in Section 10.8. The pair of VCs generated is prefixed by the comment:
For checks of subclass inheritance integrity
9 The Proof Process with SPARK
The process of developing provable SPARK code involves consideration of the following:
· The annotate-prove cycle and the effect of specification and code changes on proofs performed.
· Use of the tools to facilitate this process.
· The definition of proof functions, and the proof of properties of proof functions.
· Independent assessment activities.
· Configuration management of proofs.
9.2 Annotation and proof of SPARK code
As we have already noted, proof annotations should ideally be derived from a formal specification. In a practical project, however, this specification will be subject to change: errors or omissions may be found in it (perhaps through attempting code proof), requirements may change or a more efficient approach may suggest changes to the specification and/or the code.
9.2.1 Changes to called subprograms
Each subprogram can be thought of as having two definitions: its formal specification (the “what”) in the form of a precondition and a postcondition, visible to the outside world, and its implementation (the “how”), in the form of executable code.
In what ways, typically, can a subprogram Called, called by a higher-level subprogram Caller, change?
· A change to Called's body, but not to its specification.
· A change to Called's specification, perhaps as a result of an attempt to prove the code, but not to the code:
· A change to Called's specification and to its code.
· More fundamentally, it may disappear entirely if the changes to Caller are sufficiently wide-ranging. (In this case, there is little general advice that we can offer to cope with such changes.)
9.2.2 Changing only the body of a called subprogram
This is the most benign change of all, from the point of view of bottom-up verification. If Called's visible specification is unchanged, the only proof work necessary as a result of the change is to modify internal assertions and check statements as appropriate for the code change carried out, then to generate VCs for Called and prove these.
Where the code change is small, it may be possible to replay some or all of an earlier proof of the routine by using the Proof Checker's execute facility, provided command scripts have been kept. However, in general, this may involve editing the script; eg
· hypothesis and/or conclusion numbering may change if internal annotations are altered;
· the content of hypotheses may also change, so that the commands need to be modified accordingly;
· additional conclusions resulting from internal annotation changes will also need to be proved.
Further information on the use of the Proof Checker in this way can be found in the Proof Checker User Manual [4].
9.2.3 Changing only the specification of a called subprogram
In this case, Called will need to be reproved; depending on the scale of the changes, replay of existing proof command scripts for the subprogram may succeed with appropriate changes, as for the code-change-only case.
Suppose we have the following:
procedure OldCalled (...); procedure NewCalled (...);
--# pre OldPre; --# pre NewPre;
--# post OldPost; --# post NewPost;
If we can prove that OldPre NewPre, and only the precondition has changed, then we do not need to reprove Caller, since whenever Caller called Called it did so while satisfying the stronger precondition OldPre which suffices to show NewPre holds, too.
If we can prove that NewPost OldPost, then, again, it may not be necessary to reprove Caller. In such a case, however, where the postcondition of Called has effectively been strengthened, it is likely that this we will want this change to ripple up (into Caller's postcondition, etc.)
If the specification of Called has changed in some other way, eg an additional parameter, we will almost certainly need to reverify Caller as well. Where the change is slight, and a strong argument can be made to contain the change (eg a strengthening of the precondition of Called for a single variable), we may be able to carry out a limited reproof (eg in this example, adding a check statement in Caller to check the stronger precondition constraint before each call of Called, and carrying out only proofs of VCs leading to this check statement).
In general, though, reproof of Caller will be necessary, perhaps with changes to its specification and consequent ripple-up. Nevertheless, the command scripts and proof logs of earlier proofs can be very helpful in carrying out the reproofs in less time than the original proofs.
9.2.4 Changing both the body and the code of a called subprogram
This will necessitate reproof of Called. Again, previous proof logs and command scripts can help to carry out such reproofs in less time than the original proofs, the extent to which this is the case depending on the scale of the changes carried out.
Again, reproof of the calling environment Caller is also highly likely to be necessary. As for the previous case, for relatively minor changes it may be possible to construct a rigorous argument that reproof is unnecessary, but these cases are relatively rare.
As for the previous case, too, such changes, if they affect the visible specification of Caller, may also ripple up the calling hierarchy, requiring a number of reproofs to accommodate the change.
9.3 Use of the Examiner and other proof tools
As already noted, when used to generate VCs, the Examiner generates them for all suitable subprograms in the file(s) submitted to it.
Care must therefore be taken to ensure that previous versions of VC files generated are not overwritten when the Examiner is run, making comparison between old and new VC files to determine the extent of changes impossible.
The Simplifier and Proof Checker also overwrite the log and script files that they create when they are re-run on the same filename in the same subdirectory. However, there is the slight protection on the Sun platform that the previous version (eg myproof.plg) is renamed (to myproof.plg-), though the previous-previous version, if any, will still be lost. Be warned also that a proof carried out in multiple sessions will, by default, overwrite logs of previous sessions.
The POGS tool helps with the management of proof work by providing a summary of VCs, indicating their source and current proof status. This summary also identifies any proof work done by either the Simplifier or Proof Checker that is out of date, due to VCs having been re-generated since the proofs were produced.
9.4 Definition of proof functions
Where a proof function has been used in the annotations of a subprogram, it will require definition in a proof rule file. Such definitions should ideally be the subject of independent scrutiny, both to ensure conformance with the relevant specification items (if any), and to check that the definition is well-founded.
As well as definitional rules, it may also be advantageous to specify some properties of such proof functions; in this case, these properties should be rigorously shown to follow from the definition: this can be done with the Proof Checker, with suitable editing, provided the necessary definitions are first-order. (The means of proving such property rules is described in the Proof Checker Rules Manual [4]).
Particular care must be taken when defining proof rules for functions used in abstract own variable refinement, see Section 10.7.5 for further details.
To reduce the risk of early mistakes having wider impact, regular independent assessment of the annotation, coding and verification activities is to be recommended. This assessment can check, in addition to the scrutiny of proof function definitions referred to earlier:
· that property proof rules have been proven to follow from the definitional rules;
· that the data and algorithmic refinements carried out in moving from specification to code seem appropriate and properly documented, and that the required functionality has been properly expressed in the annotations;
· that all necessary proof documentation is being retained, under suitable control;
· that, by selecting a sample routine, for instance, proofs can be replayed and are therefore up-to-date and consistent with the accompanying rule files.
The following examples show the generation of VCs from SPARK code. Small examples, to illustrate particular points, are followed by a larger example that includes elements of a real-time, embedded controller.
The following procedure simply increments the integer parameter passed to it. Parameter X is both imported and exported and the postcondition may therefore make use of the ~ decoration to indicate its initial value.
Line
1 package P
2 is
3 pragma Elaborate_Body (P);
4 end P;
5
6 package body P
7 is
8 procedure Inc(X : in out Integer)
9 --# derives X from X;
10 --# post X = X~ + 1;
11 is
12 begin
13 X := X + 1;
14 end Inc;
+++ Flow analysis of subprogram Inc performed: no
errors found.
15
16 end P;
Running the Examiner, with VC-generation selected, produces the following VCs for procedure Inc.
For path(s) from start to run-time check associated with statement of line 13:
procedure_inc_1.
H1: true .
H2: x >= integer__first .
H3: x <= integer__last .
->
C1: x + 1 >= integer__first .
C2: x + 1 <= integer__last .
For path(s) from start to finish:
procedure_inc_2.
H1: true .
H2: x >= integer__first .
H3: x <= integer__last .
H4: x + 1 >= integer__first .
H5: x + 1 <= integer__last .
->
C1: x + 1 = x + 1 .
The first VC relates to the run-time check to ensure that incrementing X does not exceed the range of its subtype. In the second VC, which relates to the postcondition, there are no useful hypotheses but the single conclusion is clearly true showing that the procedure correctly implements its specification. Straightforward VCs are automatically eliminated by either the Examiner (see Section 8.7) or the Simplifier.
Three examples follow of a simple procedure that exchanges the values of its two parameters. The first is correct, the second shows the unprovable VCs which occur when the code is incorrectly implemented and the third shows that VCs can still be generated for code which contains flow errors.
Line
1 package P
2 is
3 pragma Elaborate_Body (P);
4 end P;
5
6 package body P
7 is
8 procedure Swap(X, Y : in out Integer)
9 --# derives X from Y &
10 --# Y from X;
11 --# post X = Y~ and Y = X~;
12 is
13 T : Integer;
14 begin
15 T := X;
16 X := Y;
17 Y := T;
18 end Swap;
+++ Flow analysis of subprogram Swap performed: no
errors found.
19
20 end P;
Again the VCs are trivially correct. (Duplicate hypotheses have been omitted here for clarity, as have the first three VCs which are associated with run-time checks and are also trivially true.)
For path(s) from start to finish:
procedure_swap_4.
H1: true .
H2: x >= integer__first .
H3: x <= integer__last .
H4: y >= integer__first .
H5: y <= integer__last .
->
C1: y = y .
C2: x = x .
This version of Swap contains a semantic error which does not affect the flow analysis of the subprogram since the dependencies described by its derives annotation remain correct.
Line
1 package P
2 is
3 pragma Elaborate_Body (P);
4 end P;
5
6 package body P
7 is
8 procedure Swap(X, Y : in out Integer)
9 --# derives X from Y &
10 --# Y from X;
11 --# post X = Y~ and Y = X~;
12 is
13 T : Integer;
14 begin
15 T := X;
16 X := Y;
17 Y := T + 1; -- error, but information flow unaffected
18 end Swap;
+++ Flow analysis of subprogram Swap performed: no
errors found.
19
20 end P;
The following VC results, with C2 being clearly unprovable.
For path(s) from start to finish:
procedure_swap_4.
H1: true .
H2: x >= integer__first .
H3: x <= integer__last .
H4: y >= integer__first .
H5: y <= integer__last .
->
C1: y = y .
C2: x + 1 = x .
Where VCs are not provable in their entirety, the Simplifier may still be able to prove parts of them and make other simplifications. For example, running the Simplifier on the above VC proves C1 and shows that C2 is not just unprovable but actually false.
For path(s) from start to finish:
procedure_swap_4.
H1: x >= integer__first .
H2: x <= integer__last .
H3: y >= integer__first .
H4: y <= integer__last .
->
C1: false .
The final example shows the importance of considering the significance of flow errors before embarking on a possibly labour-intensive proof process. An error in the code leads to an assignment statement becoming ineffective.
Line
1 package P
2 is
3 pragma Elaborate_Body (P);
4 end P;
5
6 package body P
7 is
8 procedure Swap(X, Y : in out Integer)
9 --# derives X from Y &
10 --# Y from X;
11 --# post X = Y~ and Y = X~;
12 is
13 T : Integer;
14 begin
15 T := X;
^1
!!! ( 1) Flow Error : Ineffective statement.
16 X := Y;
17 Y := X;
18 end Swap;
!!! ( 2) Flow Error : Importation of the
initial value of variable X is
ineffective.
!!! ( 3) Flow Error : The variable T is
neither referenced nor exported.
!!! ( 4) Flow Error : The imported value of
X is not used in the derivation of Y.
??? ( 5) Warning : The imported value of
Y may be used in the derivation of Y.
19
20 end P;
VCs can still be generated but again C2 is not provable.
For path(s) from start to finish:
procedure_swap_4.
H1: true .
H2: x >= integer__first .
H3: x <= integer__last .
H4: y >= integer__first .
H5: y <= integer__last .
(additional hypotheses not shown)
->
C1: y = y .
C2: y = x .
Unlike the previous example, C2 is not actually false because there are some circumstances in which it is true. The Simplifier reduces the VC to
For path(s) from start to finish:
procedure_swap_4.
H1: x >= integer__first .
H2: x <= integer__last .
H3: y >= integer__first .
H4: y <= integer__last .
(additional hypotheses not shown)
->
C1: y = x .
showing that the VC can be proved only for the case where the values to be swapped are equal!
This example makes use of the (correct) Swap procedure defined above and uses it to implement a procedure that does nothing, by swapping its parameters twice. To show how a check is made that a called procedure satisfies its precondition, a precondition has been introduced for procedure Swap. To ensure that Swap can be called without breaking its precondition, a similar one is required for procedure DoNothing.
Line
1 package P
2 is
3 pragma Elaborate_Body (P);
4 end P;
5
6 package body P
7 is
8 procedure Swap(X, Y : in out Integer)
9 --# derives X from Y &
10 --# Y from X;
11 --# pre X /= Y;
12 --# post X = Y~ and Y = X~;
13 is
14 T : Integer;
15 begin
16 T := X;
17 X := Y;
18 Y := T;
19 end Swap;
+++ Flow analysis of subprogram Swap
performed: no errors found.
20
21 procedure DoNothing(X, Y : in out Integer)
22 --# derives X from X &
23 --# Y from Y;
24 --# pre not (X = Y);
25 --# post X = X~ and Y = Y~;
26 is
27 begin
28 Swap(X, Y);
29 Swap(X, Y);
30 end DoNothing;
+++ Flow analysis of subprogram DoNothing
performed: no errors found.
31 end P;
VCs are produced for procedures Swap and DoNothing. Those for Swap are as before except that the precondition (X /= Y) appears as a hypothesis. The VCs for DoNothing are as follows.
For path(s) from start to precondition check associated with statement of line 28:
procedure_donothing_1.
H1: not (x = y) .
H2: x >= integer__first .
H3: x <= integer__last .
H4: y >= integer__first .
H5: y <= integer__last .
->
C1: y >= integer__first .
C2: y <= integer__last .
C3: x >= integer__first .
C4: x <= integer__last .
C5: x <> y .
For path(s) from start to run-time check associated with statement of line 28:
procedure_donothing_2.
H1: not (x = y) .
H2: x >= integer__first .
H3: x <= integer__last .
H4: y >= integer__first .
H5: y <= integer__last .
H6: y >= integer__first .
H7: y <= integer__last .
H8: x >= integer__first .
H9: x <= integer__last .
H10: x <> y .
H11: x__1 = y .
H12: y__1 = x .
H13: x__1 >= integer__first .
H14: x__1 <= integer__last .
H15: y__1 >= integer__first .
H16: y__1 <= integer__last .
->
C1: y__1 >= integer__first .
C2: y__1 <= integer__last .
C3: x__1 >= integer__first .
C4: x__1 <= integer__last .
For path(s) from start to precondition check associated with statement of line 29:
procedure_donothing_3.
H1: not (x = y) .
H2: x >= integer__first .
H3: x <= integer__last .
H4: y >= integer__first .
H5: y <= integer__last .
H6: y >= integer__first .
H7: y <= integer__last .
H8: x >= integer__first .
H9: x <= integer__last .
H10: x <> y .
H11: x__1 = y .
H12: y__1 = x .
H13: x__1 >= integer__first .
H14: x__1 <= integer__last .
H15: y__1 >= integer__first .
H16: y__1 <= integer__last .
H17: y__1 >= integer__first .
H18: y__1 <= integer__last .
H19: x__1 >= integer__first .
H20: x__1 <= integer__last .
->
C1: y__1 >= integer__first .
C2: y__1 <= integer__last .
C3: x__1 >= integer__first .
C4: x__1 <= integer__last .
C5: x__1 <> y__1 .
For path(s) from start to run-time check associated with statement of line 29:
procedure_donothing_4.
H1: not (x = y) .
H2: x >= integer__first .
H3: x <= integer__last .
H4: y >= integer__first .
H5: y <= integer__last .
H6: y >= integer__first .
H7: y <= integer__last .
H8: x >= integer__first .
H9: x <= integer__last .
H10: x <> y .
H11: x__1 = y .
H12: y__1 = x .
H13: x__1 >= integer__first .
H14: x__1 <= integer__last .
H15: y__1 >= integer__first .
H16: y__1 <= integer__last .
H17: y__1 >= integer__first .
H18: y__1 <= integer__last .
H19: x__1 >= integer__first .
H20: x__1 <= integer__last .
H21: y__1 >= integer__first .
H22: y__1 <= integer__last .
H23: x__1 >= integer__first .
H24: x__1 <= integer__last .
H25: x__1 <> y__1 .
H26: x__2 = y__1 .
H27: y__2 = x__1 .
H28: x__2 >= integer__first .
H29: x__2 <= integer__last .
H30: y__2 >= integer__first .
H31: y__2 <= integer__last .
->
C1: y__2 >= integer__first .
C2: y__2 <= integer__last .
C3: x__2 >= integer__first .
C4: x__2 <= integer__last .
For path(s) from start to finish:
procedure_donothing_5.
H1: not (x = y) .
H2: x >= integer__first .
H3: x <= integer__last .
H4: y >= integer__first .
H5: y <= integer__last .
H6: y >= integer__first .
H7: y <= integer__last .
H8: x >= integer__first .
H9: x <= integer__last .
H10: x <> y .
H11: x__1 = y .
H12: y__1 = x .
H13: x__1 >= integer__first .
H14: x__1 <= integer__last .
H15: y__1 >= integer__first .
H16: y__1 <= integer__last .
H17: y__1 >= integer__first .
H18: y__1 <= integer__last .
H19: x__1 >= integer__first .
H20: x__1 <= integer__last .
H21: y__1 >= integer__first .
H22: y__1 <= integer__last .
H23: x__1 >= integer__first .
H24: x__1 <= integer__last .
H25: x__1 <> y__1 .
H26: x__2 = y__1 .
H27: y__2 = x__1 .
H28: x__2 >= integer__first .
H29: x__2 <= integer__last .
H30: y__2 >= integer__first .
H31: y__2 <= integer__last .
H32: y__2 >= integer__first .
H33: y__2 <= integer__last .
H34: x__2 >= integer__first .
H35: x__2 <= integer__last .
->
C1: x__2 = x .
C2: y__2 = y .
VCs 1 and 3 are associated with the two calls to procedure Swap and are necessary to show that Swap’s precondition is met at the point of call. VCs 2 and 4 relate to run-time checks and are clearly provable. The final VC is for the entire operation of DoNothing and is to show that its postcondition follows from its precondition and code.
The Simplifier can be applied to these VCs giving
For path(s) from start to precondition check associated with statement of line 28:
procedure_donothing_1.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 28:
procedure_donothing_2.
*** true . /* all conclusions proved */
For path(s) from start to precondition check associated with statement of line 29:
procedure_donothing_3.
*** true . /* all conclusions proved */
For path(s) from start to run-time check associated with statement of line 29:
procedure_donothing_4.
*** true . /* all conclusions proved */
For path(s) from start to finish:
procedure_donothing_5.
*** true . /* all conclusions proved */
The following example extends the idea of a Swap procedure to illustrate the use of the update notation in SPARK proof contexts. This version of Swap takes an array and exchanges the two elements selected by indices passed in as parameters. The postcondition can be read as array A is the original array A with its Ith element replaced by its original Jth element and its Jth element replaced by its original Ith element.
Line
1 package P
2 is
3 pragma Elaborate_Body (P);
4 type Index is range 1..10;
5 type Atype is array(Index) of Integer;
6 end P;
7
8 package body P
9 is
10 procedure SwapElement(I, J : in Index;
11 A : in out Atype)
12 --# derives A from A, I, J;
13 --# post A = A~[I => A~(J); J => A~(I)];
14 is
15 temp : Integer;
16 begin
17 temp := A(I);
18 A(I) := A(J);
19 A(J) := temp;
20 end SwapElement;
+++ Flow analysis of subprogram SwapElement
performed: no errors found.
21 end P;
The Examiner generates four VCs for this subprogram, the first three of which relate to run-time checks. The final VC illustrates the modelling of the array accesses and updates using FDL’s element and update functions.
For path(s) from start to finish:
procedure_swapelement_4.
H1: true .
H2: i >= index__first .
H3: i <= index__last .
H4: j >= index__first .
H5: j <= index__last .
H6: for_all(i___1: index, ((i___1 >= index__first) and (
i___1 <= index__last)) -> ((element(a, [i___1]) >=
integer__first) and (element(a, [i___1]) <=
integer__last))) .
H7: element(a, [i]) >= integer__first .
H8: element(a, [i]) <= integer__last .
H9: i >= index__first .
H10: i <= index__last .
H11: element(a, [j]) >= integer__first .
H12: element(a, [j]) <= integer__last .
H13: j >= index__first .
H14: j <= index__last .
H15: i >= index__first .
H16: i <= index__last .
H17: element(a, [i]) >= integer__first .
H18: element(a, [i]) <= integer__last .
H19: element(a, [i]) >= integer__first .
H20: element(a, [i]) <= integer__last .
H21: j >= index__first .
H22: j <= index__last .
->
C1: update(update(a, [i], element(a, [j])), [j], element(
a, [i])) = update(update(a, [i], element(a, [j])), [
j], element(a, [i])) .
The Simplifier is able to discharge all the VCs for this subprogram, thus demonstrating that no run-time exceptions will be raised and that the postcondition is satisfied.
This example uses the naive integer square root algorithm introduced earlier to illustrate the generation of VCs for SPARK code containing a loop.
Line
1 package P
2 is
3 pragma Elaborate_Body (P);
4 end P;
5
6 package body P
7 is
8 procedure IntRoot(N : in Natural;
9 Root : out Natural)
10 --# derives Root from N;
11 --# pre N >= 0;
12 --# post (Root * Root <= N) and
13 --# (N < (Root + 1) * (Root + 1));
14 is
15 R : Natural := 0;
16 S, T : Natural := 1;
17 begin
18 loop
19 --# assert (T = 2 * R + 1) and
20 --# (S = (R + 1) * (R + 1)) and
21 --# (R * R <= N);
22 exit when S > N;
23
24 R := R + 1;
25 T := T + 2;
26 S := S + T;
27 end loop;
28 Root := R;
29 end IntRoot;
+++ Flow analysis of subprogram IntRoot
performed: no errors found.
30 end P;
VCs are generated from the start of the subprogram to the assert statement (loop invariant); from the assert statement round the loop back to the assert statement; and from the assert statement to the subprogram end. (There are additional VCs for RTCs which we will not consider here.) Note that the precondition N >= 0 is strictly unnecessary because this restriction is already enforced by the choice of type Natural for the input parameter to the procedure.
For path(s) from start to assertion of line 19:
procedure_introot_1.
H1: n >= 0 .
H2: n >= natural__first .
H3: n <= natural__last .
->
C1: 1 = 2 * 0 + 1 .
C2: 1 = (0 + 1) * (0 + 1) .
C3: 0 * 0 <= n .
C4: n >= natural__first .
C5: n <= natural__last .
C6: n >= 0 .
For path(s) from assertion of line 19 to assertion of line 19:
procedure_introot_2.
H1: t = 2 * r + 1 .
H2: s = (r + 1) * (r + 1) .
H3: r * r <= n .
H4: n >= natural__first .
H5: n <= natural__last .
H6: n >= 0 .
H7: s >= natural__first .
H8: s <= natural__last .
H9: not (s > n) .
H10: r >= natural__first .
H11: r <= natural__last .
H12: r + 1 >= natural__first .
H13: r + 1 <= natural__last .
H14: t >= natural__first .
H15: t <= natural__last .
H16: t + 2 >= natural__first .
H17: t + 2 <= natural__last .
H18: s >= natural__first .
H19: s <= natural__last .
H20: t + 2 >= natural__first .
H21: t + 2 <= natural__last .
H22: s + (t + 2) >= natural__first .
H23: s + (t + 2) <= natural__last .
->
C1: t + 2 = 2 * (r + 1) + 1 .
C2: s + (t + 2) = (r + 1 + 1) * (r + 1 + 1) .
C3: (r + 1) * (r + 1) <= n .
C4: n >= natural__first .
C5: n <= natural__last .
C6: n >= 0 .
For path(s) from assertion of line 19 to finish:
procedure_introot_7.
H1: t = 2 * r + 1 .
H2: s = (r + 1) * (r + 1) .
H3: r * r <= n .
H4: n >= natural__first .
H5: n <= natural__last .
H6: n >= 0 .
H7: s >= natural__first .
H8: s <= natural__last .
H9: s > n .
H10: r >= natural__first .
H11: r <= natural__last .
H12: r >= natural__first .
H13: r <= natural__last .
->
C1: r * r <= n .
C2: n < (r + 1) * (r + 1) .
The Simplifier easily proves all three VCs shown above. Two of the RTC VCs remain unproven – these relate to showing that the assignments to T and S on lines 25 and 26 will not exceed the range of Natural.
In Section 3.2.3 we note that quantified expressions are a convenient way to express constraints about array data structures. One of the examples given is the following function, which returns the index of the first occurrence in a table (array) of an input value Sought.
type Index is range 1..1000;
type Table is array(Index) of Integer;
function FindSought(A : Table;
Sought : Integer) return Index;
--# pre for some M in Index => ( A(M) = Sought );
--# return Z => (( A(Z) = Sought) and
--# (for all M in Index range 1 .. (Z-1) =>
--# (A(M) /= Sought)));
The precondition of the function ensures that it is only called if Sought is definitely present in the table.
The following code gives a body for the function, which uses a loop to search through the table from its first element until Sought is found.
function FindSought(A : Table;
Sought : Integer) return Index
is
Z : Index := Index'first;
begin
while A(Z) /= Sought and Z < Index'last loop
--# assert for all I in Index range 1 .. Z
--# => (A(I) /= Sought);
Z := Z + 1;
end loop;
return Z;
end FindSought;
The assert statement gives the loop invariant that Sought does not occur in any of the values already searched, ie any values whose index is less than or equal to Z.
The VCs remaining for this function body, after simplification by the Simplifier, are:
For path(s) from assertion of line 22 to run-time check associated with
statement of line 24:
function_findsought_5.
H1: for_all(i_ : integer, 1 <= i_ and i_ <= z -> element(a, [i_]) <> sought) .
H2: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1000 -> integer__first
<= element(a, [i___1]) and element(a, [i___1]) <= integer__last) .
H3: sought >= integer__first .
H4: sought <= integer__last .
H5: for_some(m_ : integer, m_ >= 1 and m_ <= 1000 and element(a, [m_]) =
sought) .
H6: z >= 1 .
H7: z <= 1000 .
H8: integer__size >= 0 .
H9: integer__first <= integer__last .
H10: integer__base__first <= integer__base__last .
H11: integer__base__first <= integer__first .
H12: integer__base__last >= integer__last .
H13: index__size >= 0 .
H14: index__base__first <= index__base__last .
H15: index__base__first <= 1 .
H16: index__base__last >= 1000 .
->
C1: z <= 999 .
For path(s) from assertion of line 22 to finish:
function_findsought_7.
H1: for_all(i_ : integer, 1 <= i_ and i_ <= z -> element(a, [i_]) <> sought)
.
H2: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1000 -> integer__first
<= element(a, [i___1]) and element(a, [i___1]) <= integer__last) .
H3: sought >= integer__first .
H4: sought <= integer__last .
H5: for_some(m_ : integer, m_ >= 1 and m_ <= 1000 and element(a, [m_]) =
sought) .
H6: z >= 1 .
H7: z <= 999 .
H8: element(a, [z + 1]) = sought or 999 <= z .
H9: integer__size >= 0 .
H10: integer__first <= integer__last .
H11: integer__base__first <= integer__base__last .
H12: integer__base__first <= integer__first .
H13: integer__base__last >= integer__last .
H14: index__size >= 0 .
H15: index__base__first <= index__base__last .
H16: index__base__first <= 1 .
H17: index__base__last >= 1000 .
->
C1: element(a, [z + 1]) = sought .
VC number 5 is for the check that incrementing Z does not exceed the range of Index. Strengthening the assertion to state that Z < Index’Last enables the Simplifier to discharge this VC. The final VC above is for the code from the loop invariant to the end of the function, when the while-loop condition no longer holds. Conclusion C2 follows immediately from H1, but conclusion C1 is unprovable as H2 is not quite strong enough. The real problem is that the loop invariant does not include the function’s precondition and so the precondition does not appear as a hypothesis in the VC. Adding the precondition to the loop invariant results in another hypothesis in the VC (the same as H1 in the first VC above) which combined with the existing hypotheses is sufficient to prove C1. [RPM – It isn’t clear to me that this is true.] This illustrates the importance of including enough information in invariants.
10.7 Abstract own variable refinement for a Stack
This section uses a simple example to provide an introduction to abstract own variable refinement proofs. The presentation of the example consists of:
· an abstract stack specification using an abstract proof type;
· the corresponding concrete implementation;
· the VCs that are generated to prove the refinement;
· an illustration of how the abstract stack specification can be used in other packages that make use of the stack.
10.7.1 Abstract Stack Package Specification
A complete abstract package specification for a stack is as follows.
package Stack
--# own State : StackType; -- type announced abstract variable
--# initializes State;
is
--# type StackType is abstract; -- SPARK proof annotation
-- (declares a new proof type)
function IsEmpty return Boolean;
--# global State;
function NotFull return Boolean;
--# global State;
--# function Append(S : StackType; X : Integer) -- use of proof
--# return StackType; -- type
procedure Push(X : in Integer);
--# global in out State;
--# derives State from State, X;
--# pre NotFull(State); -- abstract precondition
--# post State = Append(State~, X); -- abstract postcondition
procedure Pop(X : out Integer);
--# global in out State;
--# derives State, X from State;
--# pre not IsEmpty(State); -- abstract precondition
--# post State~ = Append(State, X); -- abstract postcondition
procedure Clear;
--# global out State;
--# derives State from ;
--# post IsEmpty(State); -- abstract postcondition
end Stack;
Although the type StackType can only be used in SPARK proof annotations, the Examiner generates an ‘illegal redeclaration’ error if an Ada object with the same name is declared in any scope where the proof type is visible. Furthermore, as the type announcement for the variable State uses an abstract proof type, there must not be a concrete declaration of State in the package. In addition if there is more than one abstract variable, then each must have its own abstract proof type (because of the meaning that the built-in abstraction relation gives to abstract types – see Section 10.7.3).
In the above example the abstract proof type has the same meaning for the Examiner as if the user had typed:
package Stack
--# own State : StackType;
--# initializes State;
is
type StackType is private;
...
private
--# hide Stack;
end Stack;
So the only information given about the type StackType is that it is possible to compare two variables of that type for equality.
10.7.2 Concrete Stack Implementation
The package body for the stack example is straightforward.
package body Stack
--# own State is Ptr, Vector;
is
MaxStackSize : constant := 100;
type Ptrs is range 0..MaxStackSize;
subtype Indexes is Ptrs range 1..Ptrs’last;
type Vectors is array (Indexes) of Integer;
Ptr : Ptrs := 0;
Vector : Vectors := Vectors'(Indexes => 0);
function IsEmpty return Boolean
--# global Ptr;
--# return (Ptr = 0); -- concrete return annotation
is
begin
return Ptr = 0;
end IsEmpty;
function NotFull return Boolean
--# global Ptr;
--# return Ptr < MaxStackSize; -- concrete return annotation
is
begin
return Ptr < MaxStackSize;
end NotFull;
procedure Push(X : in Integer)
--# global in out Vector, Ptr;
--# derives Ptr from Ptr &
--# Vector from Vector, Ptr, X;
--# pre Ptr < MaxStackSize; -- corresponds to NotFull
--# post Ptr = Ptr~ + 1 and
--# Vector = Vector~[Ptr => X]; -- corresponds to Append
is
begin
Ptr := Ptr + 1;
Vector(Ptr) := X;
end Push;
procedure Pop(X : out Integer)
--# global in Vector;
--# in out Ptr;
--# derives Ptr from Ptr &
--# X from Vector, Ptr;
--# pre Ptr > 0;
--# post Ptr = Ptr~ - 1 and X = Vector(Ptr~);
is
begin
X := Vector(Ptr);
Ptr := Ptr - 1;
end Pop;
procedure Clear
--# global out Ptr;
--# derives Ptr from ;
--# post Ptr = 0;
-- flow error: inconsistency with abstract flow annotation as Vector is unchanged
is
begin
Ptr := 0;
end Clear;
end Stack;
Note that the subprograms have concrete proof annotations, in addition to the abstract annotations in the package specification. This is exactly analogous to the abstract and concrete global and derives flow annotations.
When generating VCs for the package body the Examiner produces the following FDL definition for the proof type StackType.
type stacktype = record
vector : vectors;
ptr : ptrs
end;
The Examiner also generates an abstraction relation between the concrete and abstract variables, where the concrete variables (Vector and Ptr) are the appropriate fields of the abstract variable (State).[11]
Generating the refinement VCs is a simple matter of:
· extracting the abstract and concrete pre- and postconditions for ‘weaken pre’ and ‘strengthen post’ VCs (as appropriate);
· adding abstraction relation hypotheses for any concrete variables which are imported and/or exported (as given by the flow annotations in the package body).
Consider the procedure Push. The ‘-vcg’ option of the Examiner produces five VCs. (One VC for the code against the concrete pre/post specification, two RTC VCs and two refinement VCs.) The precondition refinement VC is as follows.
procedure_push_4.
H1: stack__notfull(state) .
H2: vector = fld_vector(state) .
H3: ptr = fld_ptr(state) .
H4: x >= integer__first .
H5: x <= integer__last .
H6: for_all(i___1: ptrs, ((i___1 >= indexes__first) and (
i___1 <= indexes__last)) -> ((element(vector, [
i___1]) >= integer__first) and (element(vector, [
i___1]) <= integer__last))) .
H7: ptr >= ptrs__first .
H8: ptr <= ptrs__last .
->
C1: ptr < maxstacksize .
Hypothesis H1 is the abstract precondition and conclusion C1 the concrete precondition. H2 and H3 are the abstraction relation hypotheses that relate the abstract and concrete variables. (H4 to H8 are the standard ‘variables in type’ hypotheses, typically used for RTC proofs.)
The postcondition refinement VC is as follows.
procedure_push_5.
H1: stack__notfull(state~) .
H2: ptr~ < maxstacksize .
H3: vector~ = fld_vector(state~) .
H4: vector = fld_vector(state) .
H5: ptr~ = fld_ptr(state~) .
H6: ptr = fld_ptr(state) .
H7: x >= integer__first .
H8: x <= integer__last .
H9: for_all(i___1: ptrs, ((i___1 >= indexes__first) and (
i___1 <= indexes__last)) -> ((element(vector~, [
i___1]) >= integer__first) and (element(vector~, [
i___1]) <= integer__last))) .
H10: ptr~ >= ptrs__first .
H11: ptr~ <= ptrs__last .
H12: for_all(i___1: ptrs, ((i___1 >= indexes__first) and (
i___1 <= indexes__last)) -> ((element(vector, [
i___1]) >= integer__first) and (element(vector, [
i___1]) <= integer__last))) .
H13: ptr >= ptrs__first .
H14: ptr <= ptrs__last .
H15: ptr = ptr~ + 1 .
H16: vector = update(vector~, [ptr], x) .
->
C1: state = append(state~, x) .
Hypotheses H15 and H16 are the concrete postcondition and conclusion C1 the abstract postcondition. H1 and H2 are the abstract and concrete preconditions. H3 to H6 are the abstraction relation hypotheses that relate the abstract and concrete variables, for both the initial and final states. (H7 to H14 are the standard ‘variables in type’ hypotheses.)
To formally prove the refinement VCs, proof rules must be supplied that give definitions of the abstract proof functions in terms of the concrete variables. As these rules are only used internally to the Stack package, they can assume the FDL definition of StackType as a record. For example:
stack__isempty(S) may_be_replaced_by fld_ptr(S) = 0 .
stack__notfull(S) may_be_replaced_by
fld_ptr(S) < maxstacksize .
append(S,X) may_be_replaced_by
mk__stacktype(vector := update(fld_vector(S),
[fld_ptr(S)+1], X),
ptr := fld_ptr(S)+1) .
The last two of these rules are sufficient to enable the two refinement VCs for Push to be proved.[12]
10.7.4 Use of Abstract Stack in Other Packages
We can use the stack package to give an alternative implementation of the swap procedure introduced in Section 10.2.
procedure Swap (X, Y : in out Integer)
--# global in out Stack.State;
--# derives Stack.State, X, Y from Stack.State, X, Y;
--# pre Stack.NotFull(Stack.Append(Stack.State, X));
--# post X = Y~ and Y = X~;
is
begin
Stack.Push(X);
Stack.Push(Y);
Stack.Pop(X);
Stack.Pop(Y);
end Swap;
Note that with this implementation, Swap must have a precondition to ensure that there is room to push at least two elements onto the stack. The precondition uses the (public) proof functions of Stack to state the required property of the abstract Stack.State. We shall now consider some of the VCs of Swap to illustrate how the abstract specification of Stack can be used in proof.
The first VC for Swap is to establish the precondition of the first call to Stack.Push. When a suitable target configuration file is provided to supply type information, and after Simplification, the VC looks like this.
procedure_swap_1.
H1: stack__notfull(stack__append(stack__state, x)) .
H2: x >= - 2147483648 .
H3: x <= 2147483647 .
H4: y >= - 2147483648 .
H5: y <= 2147483647 .
H6: integer__size >= 0 .
->
C1: stack__notfull(stack__state) .
Intuitively this VC is true as if a stack with a number appended is not full, then the stack without the element appended cannot be full either.
To actually complete the proof (eg using the Proof Checker) a proof rule has to be given for the required property of the abstract proof functions. For example:
stack__notfull(S) may_be_deduced_from
[stack__notfull(stack__append(S, X))].
As with any user supplied proof rule, there is obligation to verify that this property is valid. That is, to show that the property is true for the concrete implementation of the Stack package. This can be expressed as the following VC (with suitable FDL declarations of variables s and x):
H1: stack__notfull(stack__append(s, x)) .
->
C1: stack__notfull(s) .
Using the previously defined proof rules, for proofing the refinement VCs internal to the Stack package, this expands to:
H1: fld__ptr(mk__stacktype(vector :=
update(fld_vector(s),
[fld_ptr(s)+1], x),
ptr := fld_ptr(s)+1))
< maxstacksize.
->
C1: fld__ptr(s) < maxstacksize .
which after simplification is trivially true.
The third VC for Swap is to establish the precondition of the first call to Stack.Pop. After simplification by the Simplifier this is:
procedure_swap_3.
H1: stack__notfull(stack__append(stack__state, x)) .
H2: x >= - 2147483648 .
H3: x <= 2147483647 .
H4: y >= - 2147483648 .
H5: y <= 2147483647 .
H6: stack__notfull(stack__state) .
H7: stack__notfull(stack__append(stack__state, x)) .
H8: integer__size >= 0 .
->
C1: not stack__isempty(stack__append(stack__append(stack__state, x), y)) .
This can be proved immediately with the following proof rule:
not stack__isempty(stack__append(S, X)) may_be_deduced.
Again this proof rule needs to be justified in terms of the concrete definitions of the stack proof functions.
The Simplified output for VC 5 is:
procedure_swap_5.
H1: stack__notfull(stack__append(stack__state, x)) .
H2: x >= - 2147483648 .
H3: x <= 2147483647 .
H4: y >= - 2147483648 .
H5: y <= 2147483647 .
H6: stack__notfull(stack__state) .
H7: stack__notfull(stack__append(stack__state, x)) .
H8: stack__append(stack__state__3, x__3) = stack__append(stack__append(
stack__state, x), y) .
H9: not stack__isempty(stack__append(stack__state__3, x__3)) .
H10: x__3 >= - 2147483648 .
H11: x__3 <= 2147483647 .
H12: integer__size >= 0 .
->
C1: not stack__isempty(stack__state__3) .
This VC relates to the second Pop. To discharge this VC we need to show that two Pushes followed by one Pop cannot leave the stack empty, thus satisfying the precondition for the second call to Pop.
The final VC for Swap is the establishment of its postcondition. After simplification by the Simplifier this is:
procedure_swap_7.
H1: stack__notfull(stack__append(stack__state, x)) .
H2: x >= - 2147483648 .
H3: x <= 2147483647 .
H4: y >= - 2147483648 .
H5: y <= 2147483647 .
H6: stack__notfull(stack__state) .
H7: stack__notfull(stack__append(stack__state, x)) .
H8: stack__append(stack__append(stack__state__4, y__4), x__3) =
stack__append(stack__append(stack__state, x), y) .
H9: not stack__isempty(stack__append(stack__append(stack__state__4, y__4),
x__3)) .
H10: x__3 >= - 2147483648 .
H11: x__3 <= 2147483647 .
H12: not stack__isempty(stack__append(stack__state__4, y__4)) .
H13: y__4 >= - 2147483648 .
H14: y__4 <= 2147483647 .
H15: integer__size >= 0 .
->
C1: x__3 = y .
C2: y__4 = x .
This can be proved with the following proof rules:
X = Y may_be_deduced_from
[stack__append(S,X) = stack__append(T,Y)].
V = W may_be_deduced_from
[stack__append(stack__append(S,V),X) =
stack__append(stack__append(T,W),Y)].
10.7.5 Guidance on refinement proof rules
For any reasoning involving refinement to be sound, each user supplied proof rule, for the proof functions used in a package's abstract specification, must be satisfied by the concrete implementation. As we have seen above, there are two kinds of proof rules for refinement proof functions:
1 The internal definitions of abstract functions in terms of concrete variables.
2 The external properties of abstract functions used by callers.
The internal definitions can be proved to be consistent with the actual concrete implementation, by discharging the refinement integrity VCs generated by the Examiner. However, the external properties should be proved consistent with the internal definitions and this can be difficult to establish. For example, consider the following possible rule for the proof function Stack.Append.
S = T may_be_deduced_from
[stack__append(S,X) = stack__append(T,Y)].
This formalises the intuitive property that:
if two stacks (S and T) are the same after each has had an item appended, then they must have been the same before the items were appended.[13]
However, is this consistent with the implementation in the package body of Stack? To try to prove this consistency we can state the proof rule as the following VC:
H1: stack__append(s,x) = stack__append(t,y) .
->
C1: s = t .
Using the internal definition of stack__append this expands to:
H1: mk__stacktype(vector := update(fld_vector(s),
[fld_ptr(s)+1], x),
ptr := fld_ptr(s)+1)
=
mk__stacktype(vector := update(fld_vector(t),
[fld_ptr(t)+1], y),
ptr := fld_ptr(t)+1) .
->
C1: s = t .
By the definition of record equality H1 and C1 can both be replaced by two predicates:
H1: update(fld_vector(s), [fld_ptr(s)+1], x)
= update(fld_vector(t), [fld_ptr(t)+1], y) .
H2: fld_ptr(s) + 1 = fld_ptr(t) + 1 .
->
C1: fld_vector(s) = fld_vector(t) .
C2: fld_ptr(s) = fld_ptr(t) .
This simplifies to:
H1: update(fld_vector(s), [fld_ptr(s)+1], x)
= update(fld_vector(t), [fld_ptr(s)+1], y) .
->
C1: fld_vector(s) = fld_vector(t) .
which cannot be proved as the values of the vector components of s and t may differ at the position fld_ptr(s) + 1. Hence the proof rule is not strictly consistent with the implementation – as the initial values overwritten by appending X and Y can be different, with the final stacks still being equal.
We can (informally) argue that the potential discrepancy, in the initial values of the two stacks’ arrays, is irrelevant as it is impossible to observe any values in the arrays beyond the current end of the stacks (as defined by the values of the ptr variables). However, in more complex refinements it may be much harder to justify that any such observable behaviours, on which the validity of proof rules depend, really do hold.
Great care therefore needs to be taken when defining proof rules for proof functions used in refinement. Ideally all such rules should be proved against the internal (concrete) definitions of the proof functions, as used in the refinement VC proofs within a package.
10.8 Behavioural subtyping of extended types
This section provides an example of type extension and shows the additional VCs that are generated to show that operations on extended types are true behavioural subtypes as described in Section 2.8.5.1. The Example is made up of an Accumulator which keeps a running total of values added to it and an extension that also keeps a count of the number of items added.
10.8.1 Root “class” specification
package Accumulator
is
type T is tagged record
TheValue : Integer;
end record;
subtype Small is Integer range 1 .. 10;
procedure Clear (O : out T);
--# derives O from ;
--# post O.TheValue = 0;
procedure Put (O : in out T;
Value : in Integer);
--# derives O from O, Value;
--# pre Value in Small;
--# post O.TheValue = O~.TheValue + Value;
function Get (O : T) return Integer;
--# return O.TheValue;
end Accumulator;
10.8.2 Root “class” implementation
package body Accumulator
is
procedure Clear (O : out T)
is
begin
O.TheValue := 0;
end Clear;
procedure Put (O : in out T;
Value : in Integer)
is
begin
O.TheValue := O.TheValue + Value;
end Put;
function Get (O : T) return Integer
is
begin
return O.TheValue;
end Get;
end Accumulator;
10.8.3 Type extension specification
with Accumulator;
--# inherit Accumulator;
package AccumulatorWithCount
is
type T is new Accumulator.T with record
CallCount : Integer;
end record;
subtype Large is Integer range 1 .. 100;
-- overriding operations
procedure Clear (O : out T);
--# derives O from ;
--# post O.TheValue = 0 and O.CallCount = 0;
-- Note that this postcondition is written in the form:
-- “root postcondition” and “new term”
procedure Put (O : in out T;
Value : in Integer);
--# derives O from O, Value;
--# pre Value in Large;
--# post O = O~[TheValue => O~.TheValue + Value;
--# CallCount => O~.CallCount + 1];
-- Note that this postcondition is written in a completely different form to
-- that used on Accumulator.Put
-- Get is inherited unchanged
-- New function
function GetCallCount (O : T) return Integer;
--# return O.CallCount;
end AccumulatorWithCount;
10.8.4 Type extension implementation
package body AccumulatorWithCount
is
procedure Clear (O : out T)
is
begin
O.TheValue := 0;
O.CallCount := 0;
end Clear;
procedure Put (O : in out T;
Value : in Integer)
is
begin
O.TheValue := O.TheValue + Value;
O.CallCount := O.CallCount + 1;
end Put;
function GetCallCount (O : T) return Integer
is
begin
return O.CallCount;
end GetCallCount;
end AccumulatorWithCount;
10.8.5 Additional VCs for overridden Clear operation
The unsimplified VCs for behavioural subtyping of AccumulatorWithCount.Clear are:
For checks of subclass inheritance integrity:
procedure_clear_4.
*** true . /* trivially true VC removed by Examiner */
procedure_clear_5.
H1: fld_thevalue(fld_inherit(o)) = 0 .
H2: fld_callcount(o) = 0 .
->
C1: fld_thevalue(fld_inherit(o)) = 0 .
The Clear operation does not have a precondition so the first of these VCs, to show it “requires less” is trivially true. The second, to show that it “promises more”, is also clearly true since H1 and C1 are identical.
10.8.6 Additional VCs for overridden Put operation
The unsimplified VCs for behavioural subtyping of AccumulatorWithCount.Put are:
For checks of subclass inheritance integrity:
procedure_put_4.
H1: value >= accumulator__small__first .
H2: value <= accumulator__small__last .
->
C1: value >= large__first .
C2: value <= large__last .
procedure_put_5.
H1: o = upf_callcount(upf_inherit(o~, upf_thevalue(fld_inherit(
o~), fld_thevalue(fld_inherit(o~)) + value)), fld_callcount(
o~) + 1) .
->
C1: fld_thevalue(fld_inherit(o)) = fld_thevalue(fld_inherit(
o~)) + value .
In this case we do have a check that the precondition of the overriding operation is not stronger than the operation it overrides. This is readily provable since the “small” integer subtype is smaller than the “large” integer subtype as shown by the Examiner-generated proof rules:
put_rules(9): accumulator__small__first may_be_replaced_by 1.
put_rules(10): accumulator__small__last may_be_replaced_by 10.
put_rules(17): large__first may_be_replaced_by 1.
put_rules(18): large__last may_be_replaced_by 100.
Because of the different form used to express the postcondition of the extended version of Put, the postcondition VC is less obviously true than was the case with Clear; however, it is readily discharged by the Simplifier.
10.9 Unconstrained formal parameters
Generally it does not make any sense to make use of exported parameters in preconditions. Where, however, the parameter is of an unconstrained array type we may wish to assert properties that the actual parameter must have for the call to function correctly.
For example, consider a string copy routine which copies one unconstrained parameter to another. We may wish to assert that the exported string is the same length as the imported one.
procedure Copy (S : in String;
D : out String)
--# derives D from S;
--# pre D'Length = S'Length; -- note use of export D in precondition
is
begin
for I in Positive range S'Range loop
D (I) := S(I);
end loop;
end Copy;
If we use this routine to initialize a string of a particular subtype:
subtype Index5 is Positive range 1 ..5;
subtype String5 is String (Index5);
procedure MakeOk (D : out String5)
--# derives D from ;
is
begin
Copy ("Hello", D);
end MakeOk;
then the Examiner generates a precondition check associated with the call to Copy.
procedure_makeok_1.
H1: true .
->
C1: index5__last - index5__first + 1 = positive__5__last -
positive__5__first + 1 .
This is readily provable using the rules generated for the user-defined type Index5 and the Examiner-generated type positive_ _5 (which is created by counting the number of characters in the string literal).
makeok_rules(11): index5__first may_be_replaced_by 1.
makeok_rules(12): index5__last may_be_replaced_by 5.
makeok_rules(16): positive__5__first may_be_replaced_by 1.
makeok_rules(17): positive__5__last may_be_replaced_by 5.
SPARK includes notations designed to simplify descriptions of systems which import values from or export values to the external environment. Own variables with modes (similar to parameter modes) are used for this purpose; they are known as external variables. Section 10.10.1 below describes a method of dealing with ports that pre-dates external variables. It is followed, in Section 10.10.2, by what is essentially the same material except that it is implemented using external variables. A larger example follows these two sections.
When values are read from input ports, care needs to be taken in the way such operations are annotated so as to indicate their behaviour to the Examiner. The usual way this is done is to consider the input port to be monitoring a “stream” of input values. Reading a value removes it from the head of the stream so that a subsequent read appears, to the Examiner, to return a (possibly) different value. The usual way of annotating such port read operations is to introduce an abstract own variable to represent the input stream. For example:
package Sensor
--# own Stream;
--# initializes Stream;
is
procedure Read(X : out Integer);
--# global Stream;
--# derives X, Stream from Stream;
end Sensor;
The Examiner is a concrete proof tool and it is not possible to express a postcondition for the Read operation in terms of its abstract type (which might be regarded, for example, as an arbitrarily large sequence of integers). A method must be found where the postcondition can be expressed in terms of variables having concrete Ada types.
It is possible to regard the abstract own variable (eg Stream) as representing the most recently read value itself. Type announcement can be used to give the own variable the correct type and a suitable postcondition added.
package Sensor
--# own Stream : Integer;
--# initializes Stream;
is
procedure Read(X : out Integer);
--# global Stream;
--# derives X, Stream from Stream;
--# post X = Stream~;
end Sensor;
This annotated form can then be used to define other parts of the code. For example, consider a procedure which returns the Boolean value true if the sensor reading exceeds a certain value.
procedure AboveLimit(Result : out Boolean)
--# global Sensor.Stream;
--# derives Result, Sensor.Stream from Sensor.Stream;
--# post Result <-> (Sensor.Stream~ > 100);
is
Limit : constant Integer := 100;
Reading : Integer;
begin
Sensor.Read(Reading);
Result := Reading > Limit;
end AboveLimit;
VCs can now be generated
For path(s) from start to run-time check associated with statement of line 23:
procedure_abovelimit_1.
H1: true .
H2: reading__1 = sensor__stream .
H3: reading__1 >= integer__first .
H4: reading__1 <= integer__last .
->
C1: reading__1 >= integer__first .
C2: reading__1 <= integer__last .
For path(s) from start to finish:
procedure_abovelimit_2.
H1: true .
H2: reading__1 = sensor__stream .
H3: reading__1 >= integer__first .
H4: reading__1 <= integer__last .
H5: reading__1 >= integer__first .
H6: reading__1 <= integer__last .
H7: reading__1 >= integer__first .
H8: reading__1 <= integer__last .
->
C1: (reading__1 > limit) <-> (sensor__stream > 100) .
and simplified
For path(s) from start to run-time check associated with statement of line 23:
procedure_abovelimit_1.
*** true . /* all conclusions proved */
For path(s) from start to finish:
procedure_abovelimit_2.
*** true . /* all conclusions proved */
The method can be extended to deal with procedures which need more than one read of a port by introducing a proof function to model the way reading from a port is considered to be consuming a sequence of possible input values and then using this to re-specify the read operation as follows:
package Sensor
--# own Stream : Integer;
--# initializes Stream;
is
--# function NextReading(S : Integer) return Integer;
procedure Read(X : out Integer);
--# global Stream;
--# derives X, Stream from Stream;
--# post X = Stream~ and Stream = NextReading(Stream~);
end Sensor;
Consider a procedure that determines whether the sensor value is rising:
procedure Rising(Result : out Boolean)
--# global Sensor.Stream;
--# derives Result, Sensor.Stream from Sensor.Stream;
--# post Result <-> Sensor.NextReading(Sensor.Stream~) >
--# Sensor.Stream~;
is
Reading1,
Reading2 : Integer;
begin
Sensor.Read(Reading1);
Wait.Ten;
Sensor.Read(Reading2);
Result := Reading2 > Reading1;
end Rising;
Giving the following VC (run-time check VCs are not shown here).
For path(s) from start to finish:
procedure_rising_3.
H1: true .
H2: reading1__1 = sensor__stream .
H3: sensor__stream__1 = sensor__nextreading(sensor__stream) .
H4: reading1__1 >= integer__first .
H5: reading1__1 <= integer__last .
H6: reading1__1 >= integer__first .
H7: reading1__1 <= integer__last .
H8: reading2__2 = sensor__stream__1 .
H9: sensor__stream__2 = sensor__nextreading(sensor__stream__1) .
H10: reading2__2 >= integer__first .
H11: reading2__2 <= integer__last .
H12: reading2__2 >= integer__first .
H13: reading2__2 <= integer__last .
H14: reading1__1 >= integer__first .
H15: reading1__1 <= integer__last .
H16: reading2__2 >= integer__first .
H17: reading2__2 <= integer__last .
->
C1: (reading2__2 > reading1__1) <-> (sensor__nextreading(
sensor__stream) > sensor__stream) ..
The Simplifier discharges this VC and, with a suitable target configuration file, the RTC VCs.
Although workable, this approach is not recommended because Stream is not really an integer but some abstract object which might be considered to be a sequence of integers. Announcing it to be an integer can be considered sleight of hand which confuses the precision which proof permits.
In general, it is better completely to separate operations on the abstract stream of input values and the actual values returned. One way to do this is to poll sensors outside those parts of the code for which proof is to be attempted, store the read values in suitable variables which are then passed as parameters to, or accessed globally by, subprograms implementing algorithms which are free of outside-world objects. There is then no need to type announce the sensor stream to be of some concrete Ada type, it can remain abstract as it really is.
Such a pure version of AboveLimit would be
procedure AboveLimit(Reading : in Integer;
Result : out Boolean)
--# derives Result from Reading;
--# post Result <-> (Reading > 100);
is
Limit : constant Integer := 100;
begin
Result := Reading > Limit;
end AboveLimit;
A check that the sensor was above limit would be implemented by polling the sensor and passing the value obtained to the new, clean and provable, AboveLimit procedure.
This technique is illustrated further in the example at Section 10.11.
10.10.2 Using external variables
When values are read from input ports, care needs to be taken in the way such operations are annotated so as to indicate their behaviour to the Examiner. The usual way this is done is to consider the input port to be monitoring a “stream” of input values. Reading a value removes it from the head of the stream so that a subsequent read appears, to the Examiner, to return a (possibly) different value. SPARK permits a mode (either IN or OUT but not IN OUT) to be included in the declaration of an own variable or refinement constituent. The mode indicates communication with the external environment. Once annotated in this way no further special steps are required to obtain an accurate model of the volatile behaviour of input/output. For example:
package Sensor
--# own in Stream;
is
procedure Read(X : out Integer);
--# global Stream;
--# derives X from Stream;
end Sensor;
For proofs that rely on just the single (most recent) value read from an external variable, it is possible to regard the external abstract variable (e.g. Stream) as representing the most recently read value itself. Type announcement can be used to give the external own variable the correct type and a suitable postcondition added.
package Sensor
--# own in Stream : Integer;
is
procedure Read(X : out Integer);
--# global Stream;
--# derives X from Stream;
--# post X = Stream~;
end Sensor;
This annotated form can then be used to define other parts of the code. For example, consider a procedure which returns the Boolean value true if the sensor reading exceeds a certain value.
procedure AboveLimit(Result : out Boolean)
--# global Sensor.Stream;
--# derives Result from Sensor.Stream;
--# post Result <-> (Sensor.Stream~ > 100);
is
Limit : constant Integer := 100;
Reading : Integer;
begin
Sensor.Read(Reading);
Result := Reading > Limit;
end AboveLimit;
VCs can now be generated (the RTC VC is not shown here).
For path(s) from start to finish:
procedure_abovelimit_2.
H1: true .
H2: reading__1 = sensor__stream .
H3: reading__1 >= integer__first .
H4: reading__1 <= integer__last .
H5: reading__1 >= integer__first .
H6: reading__1 <= integer__last .
H7: reading__1 >= integer__first .
H8: reading__1 <= integer__last .
->
C1: (reading__1 > limit) <-> (sensor__stream > 100) .
C2: true .
The Simplifier discharges both this VC and, given a target configuration file, the RTC VC.
Where procedures need more than one read of a port, the Examiner generates proof attribute functions (see Section 8.4.5.3) to capture their volatile behaviour. For an external variable of mode in, the proof function ’Tail models the way reading from a port is considered to be consuming a sequence of possible input values. We can use this to re-specify the read operation as follows:
package Sensor
--# own in Stream : Integer;
is
procedure Read(X : out Integer);
--# global Stream;
--# derives X from Stream;
--# post X = Stream~ and Stream = Stream’Tail(Stream~);
end Sensor;
Consider a procedure that determines whether the sensor value is rising:
procedure Rising(Result : out Boolean)
--# global Sensor.Stream;
--# derives Result from Sensor.Stream;
--# post Result <-> Sensor.Stream’Tail(Sensor.Stream~) >
--# Sensor.Stream~;
is
Reading1,
Reading2 : Integer;
begin
Sensor.Read(Reading1);
Wait.Ten;
Sensor.Read(Reading2);
Result := Reading2 > Reading1;
end Rising;
Giving the following VCs (excluding two RTC VCs).
For path(s) from start to finish:
procedure_rising_3.
H1: true .
H2: reading1__1 = sensor__stream .
H3: sensor__stream__1 = sensor__stream__tail(
sensor__stream) .
H4: reading1__1 >= integer__first .
H5: reading1__1 <= integer__last .
H6: reading1__1 >= integer__first .
H7: reading1__1 <= integer__last .
H8: reading2__2 = sensor__stream__1 .
H9: sensor__stream__2 = sensor__stream__tail(sensor__stream__1) .
H10: reading2__2 >= integer__first .
H11: reading2__2 <= integer__last .
H12: reading2__2 >= integer__first .
H13: reading2__2 <= integer__last .
H14: reading1__1 >= integer__first .
H15: reading1__1 <= integer__last .
H16: reading2__2 >= integer__first .
H17: reading2__2 <= integer__last .
->
C1: (reading2__2 > reading1__1) <-> (sensor__stream__tail(
sensor__stream) > sensor__stream) .
C2: true .
Again, the Simplifier discharges this VC and will also discharge the RTC VCs if the Examiner is presented with a target configuration file.
For values written to external variables of mode out, the ’Append proof attribute (see Section 3.3.1.3) is used showing that the written value is appended to the sequence of values seen by the external environment.
A mixture of the approaches described in Sections 10.10.1 and 10.10.2 may be needed where an abstract own variable without a mode is refined onto constituents which are moded external variables. In this case, the proof attributes will be applicable inside the package body and other, user-supplied proof functions will be needed in the abstract, external view.
This example forms part of a environmental control system designed to maintain the temperature of some environment between set limits.
The system consists of a clock to determine operating times, a temperature sensor, a mode switch and an actuator that turns a heating system on or off. The requirement is for the heating to be on only when within the operating time range and when the temperature is below some target temperature.
External variables have been used for the interfaces but the control algorithm (PerformModeOperations) has been kept separate from the reading of sensors and writing of actuators as described at the end of Section 10.10.1.
The entire operation can then be described by the schema disjunction
From the specification it is clear that the post condition will consist of three disjunctions: one each for ModeOff, ModeContinuous and ModeTimed. We also have to consider the refinements used in producing SPARK equivalents to elements of the Z specification. For example, the variable AboveTemp is the refinement of the Z thermostat? = aboveTemp. By this process we can arrive at the postcondition for the PerformModeOperation operation which is
--# post
--# (Mode = ModeSwitch.off and not Heating) or
--# (Mode = ModeSwitch.cont and (Heating <-> not AboveTemp)) or
--# (Mode = ModeSwitch.timed and
--# (Heating <->
--# (not AboveTemp and Time > OnTime and Time < OffTime)));
The annotated code for the heating controller can now be completed.
-------------------------------------------------------
-- 1. INTERFACES TO THE REAL WORLD --
-------------------------------------------------------
package Clock
--# own in TimeSeq;
is
subtype Times is Integer range 0 .. 86399;
procedure Read (T: out Times);
--# global in TimeSeq;
--# derives T from TimeSeq;
-- return the current time
end Clock;
package Thermostat
--# own in TempSeq;
is
procedure Read (AboveTemp: out Boolean);
--# global in TempSeq;
--# derives AboveTemp from TempSeq;
-- AboveTemp is true iff temperature is >= required level
end Thermostat;
package ModeSwitch
--# own in ModeSwitchSeq;
is
type Modes is (off, cont, timed);
procedure Read (M: out Modes);
--# global in ModeSwitchSeq;
--# derives M from ModeSwitchSeq;
-- reads setting of ModeSwitch and returns its current state
end ModeSwitch;
package Actuator
--# own out ActSeq;
is
procedure Write(TurnOn: in Boolean);
--# global out ActSeq;
--# derives ActSeq from TurnOn;
-- activates heating if true passed in, deactivates if false
end Actuator;
with Thermostat,
Actuator,
Clock,
ModeSwitch;
--# inherit Thermostat,
--# Actuator,
--# Clock,
--# ModeSwitch;
--# main_program
procedure HeatingSystem
--# global out Actuator.ActSeq;
--# in Thermostat.TempSeq,
--# Clock.TimeSeq,
--# ModeSwitch.ModeSwitchSeq;
--# derives Actuator.ActSeq from Thermostat.TempSeq,
--# Clock.TimeSeq,
--# ModeSwitch.ModeSwitchSeq;
is
OnTime : constant Clock.Times := 32400;
OffTime : constant Clock.Times := 61200;
OldHeating : Boolean := False; -- initial value from Actuator package
Heating : Boolean;
Mode: ModeSwitch.Modes;
AboveTemp: Boolean;
Time: Clock.Times;
-------------------------------------------------------
-- 2. IMPLEMENTATION OF THE Z SPECIFICATION --
-------------------------------------------------------
function IsInOperatingPeriod(Time : Clock.Times) return Boolean
--# return Time > OnTime and Time < OffTime;
is
begin
return Time > OnTime and Time < OffTime;
end IsInOperatingPeriod;
procedure PerformModeOperation
--# global out Heating; in Mode, AboveTemp, Time;
--# derives Heating from Mode, AboveTemp, Time;
--# post
--# (Mode = ModeSwitch.off and not Heating) or
--# (Mode = ModeSwitch.cont and (Heating <-> not AboveTemp)) or
--# (Mode = ModeSwitch.timed and
--# (Heating <->
--# (not AboveTemp and Time>OnTime and Time<OffTime)));
is
begin
case Mode is
when ModeSwitch.off =>
Heating := False;
when ModeSwitch.cont =>
Heating := not AboveTemp;
when ModeSwitch.timed =>
Heating := not AboveTemp and
IsInOperatingPeriod(Time);
end case;
end PerformModeOperation;
begin -- HeatingSystem
loop
Clock.Read(Time);
Thermostat.Read(AboveTemp);
ModeSwitch.Read(Mode);
PerformModeOperation;
if Heating /= OldHeating then
Actuator.Write(Heating);
end if;
OldHeating := Heating;
end loop;
end HeatingSystem;
10.11.4 Verification conditions
The verification conditions for PerformModeOperation are as follows.
For path(s) from start to run-time check associated with statement of line 108:
procedure_performmodeoperation_1.
H1: true .
H2: mode >= modeswitch__modes__first .
H3: mode <= modeswitch__modes__last .
H4: true .
H5: time >= clock__times__first .
H6: time <= clock__times__last .
H7: mode = modeswitch__timed .
->
C1: time >= clock__times__first .
C2: time <= clock__times__last .
For path(s) from start to finish:
procedure_performmodeoperation_2.
H1: true .
H2: mode >= modeswitch__modes__first .
H3: mode <= modeswitch__modes__last .
H4: true .
H5: time >= clock__times__first .
H6: time <= clock__times__last .
H7: mode = modeswitch__off .
->
C1: ((mode = modeswitch__off) and (not false)) or (((
mode = modeswitch__cont) and (false <-> (not
abovetemp))) or ((mode = modeswitch__timed) and (
false <-> ((not abovetemp) and ((time > ontime) and (
time < offtime)))))) .
procedure_performmodeoperation_3.
H1: true .
H2: mode >= modeswitch__modes__first .
H3: mode <= modeswitch__modes__last .
H4: true .
H5: time >= clock__times__first .
H6: time <= clock__times__last .
H7: mode = modeswitch__cont .
->
C1: ((mode = modeswitch__off) and (not (not abovetemp))) or (((
mode = modeswitch__cont) and ((not abovetemp) <-> (not
abovetemp))) or ((mode = modeswitch__timed) and ((not
abovetemp) <-> ((not abovetemp) and ((time >
ontime) and (time < offtime)))))) .
procedure_performmodeoperation_4.
H1: true .
H2: mode >= modeswitch__modes__first .
H3: mode <= modeswitch__modes__last .
H4: true .
H5: time >= clock__times__first .
H6: time <= clock__times__last .
H7: mode = modeswitch__timed .
H8: time >= clock__times__first .
H9: time <= clock__times__last .
H10: true .
->
C1: ((mode = modeswitch__off) and (not ((not abovetemp) and
isinoperatingperiod(time)))) or (((mode =
modeswitch__cont) and (((not abovetemp) and
isinoperatingperiod(time)) <-> (not abovetemp))) or ((
mode = modeswitch__timed) and (((not abovetemp) and
isinoperatingperiod(time)) <-> ((not abovetemp) and ((
time > ontime) and (time < offtime)))))) .
The VCs can be extensively simplified by the Simplifier.
For path(s) from start to run-time check associated with statement of line 108:
procedure_performmodeoperation_1.
*** true . /* all conclusions proved */
For path(s) from start to finish:
procedure_performmodeoperation_2.
*** true . /* all conclusions proved */
procedure_performmodeoperation_3.
*** true . /* all conclusions proved */
procedure_performmodeoperation_4.
H1: time >= 0 .
H2: time <= 86399 .
H3: integer__size >= 0 .
H4: clock__times__size >= 0 .
H5: modeswitch__modes__size >= 0 .
->
C1: not abovetemp and isinoperatingperiod(time) <-> not abovetemp and (time
> 32400 and time < 61200) .
Only the final VC is not proved by the Simplifier; this is because the code implements the check for being within the operating period by means of a call to the function IsInOperatingPeriod rather by direct inequalities as used in the specification. Within the Proof Checker, substitution for this function with a suitable proof rule would be enough to complete the proof.
10.11.6 The use of proof functions
To illustrate a use of proof functions, the postcondition used above has here been expressed in terms of the following proof function.
--# function IntendedSetting(T : Clock.Times;
--# M : ModeSwitch.Modes;
--# Hot : Boolean) return Boolean;
The postcondition then becomes
--# post Heating <-> IntendedSetting(Time, Mode, AboveTemp);
The VCs generated from this revised code are as follows.
For path(s) from start to run-time check associated with statement of line 113:
procedure_performmodeoperation_1.
H1: true .
H2: mode >= modeswitch__modes__first .
H3: mode <= modeswitch__modes__last .
H4: true .
H5: time >= clock__times__first .
H6: time <= clock__times__last .
H7: mode = modeswitch__timed .
->
C1: time >= clock__times__first .
C2: time <= clock__times__last .
For path(s) from start to finish:
procedure_performmodeoperation_2.
H1: true .
H2: mode >= modeswitch__modes__first .
H3: mode <= modeswitch__modes__last .
H4: true .
H5: time >= clock__times__first .
H6: time <= clock__times__last .
H7: mode = modeswitch__off .
->
C1: false <-> intendedsetting(time, mode, abovetemp) .
procedure_performmodeoperation_3.
H1: true .
H2: mode >= modeswitch__modes__first .
H3: mode <= modeswitch__modes__last .
H4: true .
H5: time >= clock__times__first .
H6: time <= clock__times__last .
H7: mode = modeswitch__cont .
->
C1: (not abovetemp) <-> intendedsetting(time, mode,
abovetemp) .
procedure_performmodeoperation_4.
H1: true .
H2: mode >= modeswitch__modes__first .
H3: mode <= modeswitch__modes__last .
H4: true .
H5: time >= clock__times__first .
H6: time <= clock__times__last .
H7: mode = modeswitch__timed .
H8: time >= clock__times__first .
H9: time <= clock__times__last .
H10: true .
->
C1: ((not abovetemp) and isinoperatingperiod(time)) <->
intendedsetting(time, mode, abovetemp) .
Proof of these VCs would require use of the Proof Checker and establishment of suitable substitution rules for the proof function. Informally, the hypotheses can be read as a traversal condition for a particular path and the conclusion as an action. Consider the second VC: this can be read as “when the mode switch is off, the code can be regarded as correct provided the intended heating setting under these circumstances is false”.
This approach allows an interrogative use of the VC Generator: suitable proof functions, for the exports of interest, can be determined from the derives annotation and used to write a skeletal postcondition. The VCs generated can then be interpreted as above.
For example:
--# derives X from X, Y &
--# Y from Y &
--# Z from X, Y, Z;
would suggest proof functions:
--# function Xout(X : Xtype; Y : Ytype) return Xtype;
--# function Yout(Y : Ytype) return Ytype;
--# function Zout(X : Xtype; Y : Ytype; Z : Ztype) return
Ztype;
allowing construction of the following postcondition:
--# post X = Xout(X~, Y~) and
--# Y = Yout(Y~) and
--# Z = Zout(X~, Y~, Z~);
(the ~ is needed because X, Y and Z are all both imported and exported).
None of this retrospective delving is a substitute for first specifying the code, then asserting (through proof contexts) its behaviour and proving it. For example, there may be circumstances in which we wish to investigate the behaviour of a subset of the exports of a subprogram. Consider the procedure SumAndDiff which returns the sum and difference of two integer numbers.
procedure SumAndDiff(X, Y : in Integer;
S, D : out Integer)
--# derives S, D from X, Y;
is
begin
S := X + Y;
D := X - Y;
end SumAndDiff;
If we were just interested in the behaviour of S we could define a proof function
--# function Sout (X, Y : Integer) return Integer;
and use it to specify a post condition
--# post S = Sout(X, Y);
VCs can now be generated which we may use to enhance our understanding of how export S behaves (but which tell us nothing about D).
For path(s) from start to finish:
procedure_sumanddiff_1.
H1: true .
H2: x >= integer__first .
H3: x <= integer__last .
H4: y >= integer__first .
H5: y <= integer__last .
->
C1: x + y = sout(x, y) .
Document Control and References
Altran Praxis Limited, 20 Manvers Street, Bath BA1 1PX, UK.
Copyright Altran Praxis Limited 2010. All rights reserved.
svn/userdocs/Examiner_GenVCs.doc (was previously S.P0468.73.31)
Issue 0.1: (18th September 1995) Initial version
Issue 0.2: (6th October 1995) After review by ION and JAH
Issue 0.3: (1st November 1995) Conversion to Praxis Standard Document by SGB
Issue 0.4: (8th November 1995) Incorporation of final comments by ION
Issue 2.0: (1st July 1997) Conversion to new standard document format
Issue 2.1: (27th August 1997) Updated for Examiner Release 3.0, made provisional
Issue 3.0: (2nd September 1997) After formal review
Issue 3.1: (21st June 2000) Draft update for Examiner Release 5.0
Issue 4.0: (10th July 2000) Updated to definitive after review.
Issue 4.1: (10th July 2001) Draft update for Release 6.0
Issue 6.0: (24th August 2001) After review by JARH
Issue 6.01: (6th February 2002) CFR 993—Added documentation of type assertion annotation
Issue 6.02: (24th May 2002) Description of FDL representation of tagged records
Issue 6.10: (24th June 2002) Updates resulting from review S.60468.79.77
Issue 6.11: (29th October 2002) Addition of Liskov-Wing rules
Issue 6.2: (30th October 2002) After review
Issue 7.0: (14th April 2003) Updated to new template format
Issue 8.0: (29th May 2003) Changes to new template, final format
Issue 8.1: (3rd Jun 2003) Addition of unconstrained formal parameters, concurrency issues and final tidy up.
Issue 8.2: (29th April 2004) Addition of % operator.
Issue 8.3: (9th July 2004) Describe private type refinement.
Issue 8.4: (2nd November 2004) Describe composite constant rule policy.
Issue 8.5: (23rd November 2004) Change company name only.
Issue 8.6: (5th January 2005) Definitive issue following review S.P0468.79.88.
Issue 8.7: (11th February 2005) Added note that explicit range is not permitted in quantified expressions over type Boolean. (SEPR 1779).
Issue 8.8: (22nd November 2005) Changed Line Manager.
Issue 8.9: (21st August 2008): Added “real” as an FDL reserved identifier (SEPR 2437)
Issue 8.10: (7th January 2009): Factored out contact details.
Issue 8.11: (2nd February 2009): Modify copyright notice.
Issue 8.12: (8th July 2009): Updates for unconstrained array aggregates (SEPR 2723).
Issue 8.13: (30th October 2009): Updates description of private type refinement VCs (SEPR 2780).
Issue 8.14: (2nd November 2009): Added specification for SPARK2005’s S’Mod (SEPR 2786).
Issue 8.15: (20th November 2009): Remove all reference to path functions [IA17-027].
Issue 9.0: (5th January 2010): Merged with the GenRTCs manual [I929-007].
Issue 9.1: (12th January 2010): Actions from review [I929-007].
Issue 9.2: (21st January 2010): Added information about function call model [I915-022].
Issue 9.3: (3rd February 2010): Rebrand to Altran Praxis Limited
Issue 9.4: (11th February 2010): Minor corrections following review to [I915-022] and set to definitive.
Issue 9.5: (1st March 2010): Added abstract to FDL reserved words list.
Issue 9.6: (12th October 2010): Correct references to the Examiner.
Issue 9.7: (1st November 2010): Corrected reference to the Simplifier user manual.
Issue 9.8: (9th November 2010): Updated to cover new behaviour of ‘Always_Valid [J917-028].
Issue 9.9: (24th February 2011): Updated to cover application of ‘Always_Valid to types [J917-008].
Issue 10.0: (30th March 2011): Updated for derived numeric types [K223-020].
Issue 10.1: (6th May 2011): Reverted changes from issue 9.9 [J917-008].
Issue 10.2: (1st November 2011): Corrected FDL examples in section 4 [K401-011].
None.
1 Examiner User Manual, Examiner_UM.pdf
2 SPARK Simplifier User Manual, Simplifier_UM.pdf
3 SPARK Proof Checker Rules Manual, Checker_Rules.pdf
4 SPARK Proof Checker User Manual, Checker_UM.pdf
5 POGS User Manual, Pogs_UM.pdf
6 SPARK FDL Manual, SPADE_FDL.pdf