5. Statements
SPARK restricts the use of some statements, and adds a number of pragmas which are used for verification, particularly involving loop statements.
5.1. Simple and Compound Statements - Sequences of Statements
SPARK excludes certain kinds of statements that complicate verification.
Legality Rules
A
simple_statement
shall not be arequeue_statement
, anabort_statement
, or acode_statement
.A
compound_statement
shall not be anaccept_statement
or aselect_statement
.A statement is only in SPARK if all the constructs used in the statement are in SPARK.
5.2. Assignment Statements
No extensions or restrictions.
5.3. If Statements
No extensions or restrictions.
5.4. Case Statements
No extensions or restrictions.
5.5. Loop Statements
5.5.1. User-Defined Iterator Types
Legality Rules
The generic package Ada.Iterator_Interfaces shall not be referenced. [In particular, Ada.Iterator_Interfaces shall not be instantiated. An alternative mechanism for defining iterator types is described in the next section.]
5.5.2. Generalized Loop Iteration
Static Semantics
Ada’s generalized loop iteration is supported in SPARK, but only in a modified form. Ada’s existing generalized loop iteration is defined in terms of other constructs which are not in SPARK (e.g., access discriminants).
Instead, SPARK provides a new mechanism for defining an iterable container type (see Ada RM 5.5.1). Iteration over the elements of an object of such a type is then allowed as for any iterable container type (see Ada RM 5.5.2), although with dynamic semantics as described below. Similarly, SPARK provides a new mechanism for defining an iterator type (see Ada RM 5.5.1), which then allows generalized iterators as for any iterator type (see Ada RM 5.5.2). Other forms of generalized loop iteration are not in SPARK.
The type-related operational representation aspect Iterable may be specified for any non-array type. The
aspect_definition
for an Iterable aspect specification for a subtype of a type T shall follow the following grammar foriterable_specification
:iterable_specification ::= (First => name, Next => name, Has_Element => name[, Element => name])
If the aspect Iterable is visibly specified for a type, the (view of the) type is defined to be an iterator type (view). If the aspect Iterable is visibly specified for a type and the specification includes an Element argument then the (view of the) type is defined to be an iterable container type (view). [The visibility of an aspect specification is defined in Ada RM 8.8]. [Because other iterator types and iterable container types as defined in Ada RM 5.5.1 are necessarily not in SPARK, this effectively replaces, rather than extends, those definitions].
Legality Rules
Each of the four (or three, if the optional argument is omitted) names shall denote an explicitly declared primitive function of the type, referred to respectively as the First, Next, Has_Element, and Element functions of the type. All parameters of all four subprograms shall be of mode In.
The First function of the type shall take a single parameter, which shall be of type T. The “iteration cursor subtype” of T is defined to be result subtype of the First function. The First function’s name shall be resolvable from these rules alone. [This means the iteration cursor subtype of T can be determined without examining the other subprogram names]. The iteration cursor subtype of T shall be definite and shall not be limited.
The Next function of the type shall have two parameters, the first of type T and the second of the cursor subtype of T; the result subtype of the function shall be the cursor subtype of T.
The Has_Element function of the type shall have two parameters, the first of type T and the second of the cursor subtype of T; the result subtype of the function shall be Boolean.
The Element function of the type, if one is specified, shall have two parameters, the first of type T and the second of the cursor subtype of T; the default element subtype of T is then defined to be the result subtype of the Element function.
Reverse container element iterators are not in SPARK. The loop parameter of a container element iterator is a constant object.
A container element iterator shall only occur as the loop_parameter_specification of a quantified_expression[, and not as the iteration_scheme of a loop statement].
Dynamic Semantics
Iteration associated with a generalized iterator or a container element iterator proceeds as follows. An object of the iteration cursor subtype of T (hereafter called “the cursor”) is created and is initialized to the result of calling First, passing in the given container object. Each iteration begins by calling Has_Element, passing in the container and the cursor. If False is returned, execution of the associated loop is completed. If True is returned then iteration continues and the loop parameter for the next iteration of the loop is either (in the case of a generalized iterator) the cursor or (in the case of a container element iterator) the result of calling the Element function, passing in the container and the cursor. At the end of the iteration, Next is called (passing in the container and the cursor) and the result is assigned to the cursor.
5.5.3. Loop Invariants, Variants and Entry Values
Two loop-related pragmas, Loop_Invariant and Loop_Variant, and a loop-related
attribute, Loop_Entry are defined. The pragma Loop_Invariant is used to specify
the essential non-varying properties of a loop. Pragma Loop_Variant is intended
for use in ensuring termination. The Loop_Entry attribute is used to refer to
the value that an expression had upon entry to a given loop in much the same way
that the Old
attribute in a subprogram postcondition can be used to refer to
the value an expression had upon entry to the subprogram.
Syntax
loop_variant_parameters ::= structural_loop_variant_item | numeric_loop_variant_items
numeric_loop_variant_items ::= numeric_loop_variant_item {, numeric_loop_variant_item}
numeric_loop_variant_item ::= change_direction => expression
structural_loop_variant_item ::= Structural => expression
change_direction ::= Increases | Decreases
Static Semantics
Pragma Loop_Invariant is like a pragma Assert except it also acts as a cut point in formal verification. A cut point means that a prover is free to forget all information about modified variables that has been established within the loop. Only the given Boolean expression is carried forward.
Pragma Loop_Variant is used to demonstrate that a loop will terminate by specifying expressions that will increase or decrease as the loop is executed.
Legality Rules
Loop_Invariant is an assertion just like pragma Assert with respect to syntax of its Boolean actual parameter, name resolution, legality rules and dynamic semantics, except for extra legality rules given below.
Loop_Variant is an assertion and has an expected actual parameter which is a specialization of an Ada expression. Otherwise, it has the same name resolution and legality rules as pragma Assert, except for extra legality rules given below.
The following constructs are said to be restricted to loops:
A Loop_Invariant pragma;
A Loop_Variant pragma;
A
block_statement
whosesequence_of_statements
ordeclarative_part
immediately includes a construct which is restricted to loops.
A construct which is restricted to loops shall occur immediately within either:
the
sequence_of_statements
of aloop_statement
; orthe
sequence_of_statements
ordeclarative_part
of ablock_statement
.
The construct is said to apply to the innermost enclosing loop.
[Roughly speaking, a Loop_Invariant or Loop_Variant pragma shall only occur immediately within a loop statement except that intervening block statements are ignored for purposes of this rule.]
The expression of a
numeric_loop_variant_item
shall be either of a discrete type or of a subtype ofAda.Numerics.Big_Numbers.Big_Integers.Big_Integer
. In the second case, the associatedchange_direction
shall be Decreases.The expression of a
structural_loop_variant_item
shall denote a variable of an anonymous access-to-object type.Two Loop_Invariant or Loop_Variant pragmas which apply to the same loop shall occur in the same
sequence_of_statements
, separated only by [zero or more] other Loop_Invariant or Loop_Variant pragmas.
Dynamic Semantics
Other than the above legality rules, pragma Loop_Invariant is equivalent to pragma
Assert
. Pragma Loop_Invariant is an assertion (as defined in Ada RM 11.4.2(1.1/3)) and is governed by the Loop_Invariant assertion aspect [and may be used in an Assertion_Policy pragma].The elaboration of a Checked Loop_Variant pragma containing
numeric_loop_variant_items
begins by evaluating theexpressions
in textual order. For every expression whose type is a subtype ofAda.Numerics.Big_Numbers.Big_Integers.Big_Integer
, a check is performed that it is non-negative. For the first elaboration of the pragma within a given execution of the enclosing loop statement, no further action is taken. For subsequent elaborations of the pragma, one or more of these expression results are each compared to their corresponding result from the previous iteration as follows: comparisons are performed in textual order either until unequal values are found or until values for all expressions have been compared. In either case, the last pair of values to be compared is then checked as follows: if thechange_direction
for the associatedloop_variant_item
is Increases (respectively, Decreases) then a check is performed that the expression value obtained during the current iteration is greater (respectively, less) than the value obtained during the preceding iteration. The exception Assertions.Assertion_Error is raised if this check fails. All comparisons and checks are performed using predefined operations. Pragma Loop_Variant is an assertion (as defined in Ada RM 11.4.2(1.1/3)) and is governed by the Loop_Variant assertion aspect [and may be used in an Assertion_Policy pragma].
Verification Rules
The variable denoted by the expression of a
structural_loop_variant_item
shall be updated on all paths reentering the loop to a strict subcomponent of the structure it used to denote.No deep parts of the value designated by the variable denoted by the expression of a
structural_loop_variant_item
shall be written by the loop. [This ensures that the previous rule is sufficient to prove loop termination on acyclic data structures.]
Examples
The following example illustrates some pragmas of this section
1procedure Loop_Var_Loop_Invar is
2 type Total is range 1 .. 100;
3 subtype T is Total range 1 .. 10;
4 I : T := 1;
5 R : Total := 100;
6begin
7 while I < 10 loop
8 pragma Loop_Invariant (R >= 100 - 10 * I);
9 pragma Loop_Variant (Increases => I,
10 Decreases => R);
11 R := R - I;
12 I := I + 1;
13 end loop;
14end Loop_Var_Loop_Invar;
Note that in this example, the loop variant is unnecessarily complex,
stating that I
increases is enough to prove termination of this
simple loop.
5.5.3.1. Attribute Loop_Entry
Static Semantics
For a prefix X that denotes an object of a nonlimited type, the following attribute is defined:
X'Loop_Entry [(loop_name)]
X’Loop_Entry [(loop_name)] denotes a constant object of the type of X. [The value of this constant is the value of X on entry to the loop that is denoted by
loop_name
or, if noloop_name
is provided, on entry to the closest enclosing loop.]
Legality Rules
A Loop_Entry
attribute_reference
applies to aloop_statement
in the same way that anexit_statement
does (see Ada RM 5.7). For every rule aboutexit_statements
in the Name Resolution Rules and Legality Rules sections of Ada RM 5.7, a corresponding rule applies to Loop_Entryattribute_references
.In many cases, the language rules pertaining to the Loop_Entry attribute match those pertaining to the Old attribute (see Ada LRM 6.1.1), except with “Loop_Entry” substituted for “Old”. These include:
prefix name resolution rules (including expected type definition)
nominal subtype definition
accessibility level definition
run-time tag-value determination (in the case where X is tagged)
interactions with abstract types
interactions with anonymous access types
forbidden attribute uses in the prefix of the
attribute_reference
.
The following rules are not included in the above list; corresponding rules are instead stated explicitly below:
the requirement that an Old
attribute_reference
shall only occur in a postcondition expression;the rule disallowing a use of an entity declared within the postcondition expression;
the rule that a potentially unevaluated Old
attribute_reference
shall statically name an entity;the prefix of the
attribute_reference
shall not contain a Loop_Entryattribute_reference.
A
Loop_Entry
attribute_reference
shall occur within aLoop_Variant
orLoop_Invariant
pragma, or anAssert
,Assume
orAssert_And_Cut
pragma appearing in a position where aLoop_Invariant
pragma would be allowed.[Roughly speaking, a
Loop_Entry
attribute_reference
can occur in anAssert
,Assume
orAssert_And_Cut
pragma immediately within a loop statement except that intervening block statements are ignored for purposes of this rule.]The prefix of a Loop_Entry
attribute_reference
shall not contain a use of an entity declared within theloop_statement
but not within the prefix itself.[This rule is to allow the use of I in the following example:
loop pragma Assert (Boolean'(Var > Some_Function (Param => (for all I in T => F (I))))'Loop_Entry);
In this example the value of the inequality “>” that would have been evaluated on entry to the loop is obtained even if the value of Var has since changed].
The prefix of a Loop_Entry
attribute_reference
shall statically name an entity, or shall denote anobject_renaming_declaration
, ifthe
attribute_reference
is potentially unevaluated; orthe
attribute_reference
does not apply to the innermost enclosingloop_statement
.
[This rule follows the corresponding Ada RM rule for ‘Old: the prefix of an Old attribute_reference that is potentially unevaluated shall statically name an entity. This rule has the same rationale. If the following was allowed:
procedure P (X : in out String; Idx : Positive) is begin Outer : loop if Idx in X'Range then loop pragma Loop_Invariant (X(Idx) > X(Idx)'Loop_Entry(Outer));
this would introduce an exception in the case where Idx is not in X’Range.]
The prefix of a Loop_Entry
attribute_reference
shall not contain a Loop_Entryattribute_reference.
Dynamic Semantics
For each X’Loop_Entry other than one occurring within an Ignored assertion expression, a constant is implicitly declared at the beginning of the associated loop statement. The constant is of the type of X and is initialized to the result of evaluating X (as an expression) at the point of the constant declaration. The value of X’Loop_Entry is the value of this constant; the type of X’Loop_Entry is the type of X. These implicit constant declarations occur in an arbitrary order.
The previous paragraph notwithstanding, the implicit constant declaration is not elaborated if the
loop_statement
has aniteration_scheme
whose evaluation yields the result that thesequence_of_statements
of theloop_statement
will not be executed (loosely speaking, if the loop completes after zero iterations).[Note: This means that the constant is not elaborated unless the loop body will execute (or at least begin execution) at least once. For example, a while loop
while <condition> do sequence_of_statements; -- contains Loop_Entry uses end loop;
may be thought of as being transformed into
if <condition> then declare ... implicitly declared Loop_Entry constants begin loop sequence_of_statements; exit when not <condition>; end loop; end; end if;
The rule also prevents the following example from raising Constraint_Error:
declare procedure P (X : in out String) is begin for I in X'Range loop pragma Loop_Invariant (X(X'First)'Loop_Entry >= X(I)); X := F(X); -- modify X end loop; end P; Length_Is_Zero : String := ""; begin P (Length_Is_Zero); end; -- ...]
5.6. Block Statements
No extensions or restrictions.
5.7. Exit Statements
No extensions or restrictions.
5.8. Goto Statements
Legality Rules
A
goto_statement
shall be located before the target statement in the innermostsequence_of_statements
enclosing the target statement.
5.9. Proof Pragmas
This section discusses the pragmas Assert_And_Cut and Assume.
Two SPARK pragmas are defined, Assert_And_Cut and Assume. Each is an
assertion and has a single Boolean parameter (an assertion expression)
and may be used wherever pragma Assert is allowed, with the additional
restriction that pragma Assert_And_Cut must be part of a
sequence_of_statements
.
Assert_And_Cut may be used when the given expression
sums up all the work done so far in the enclosing sequence_of_statements
,
so that the rest of the enclosing body can be verified (informally or formally)
while treating the whole prefix preceding Assert_And_Cut as a single
opaque (local) subprogram call, with post-condition provided by the
Assert_And_Cut expression. This allows dividing up a subprogram into
sections for the purposes of testing or formal verification. The pragma
also serves as useful documentation.
A Boolean expression which is an actual parameter of pragma Assume can be assumed to be True for the remainder of the subprogram. If the Assertion_Policy is Check for pragma Assume and the Boolean expression does not evaluate to True, the exception Assertions.Assertion_Error will be raised. However, in proof, no verification of the expression is performed and in general it cannot. It has to be used with caution and is used to state axioms.
Static Semantics
Pragma Assert_And_Cut is an assertion the same as a pragma Assert except it also acts as a cut point in formal verification. The cut point means that a prover is free to forget all information about modified variables that has been established from the statement list before the cut point. Only the given Boolean expression is carried forward.
Pragma Assume is an assertion the same as a pragma Assert except that there is no verification condition to prove the truth of the Boolean expression that is its actual parameter. [Pragma Assume indicates to proof tools that the expression can be assumed to be True.]
Legality Rules
Pragmas Assert_And_Cut and Assume have the same syntax for their Boolean actual parameter, name resolution rules and dynamic semantics as pragma Assert.
Verification Rules
The verification rules for pragma Assume are significantly different to those of pragma Assert. [It would be difficult to overstate the importance of the difference.] Even though the dynamic semantics of pragma Assume and pragma Assert are identical, pragma Assume does not introduce a corresponding verification condition. Instead the prover is given permission to assume the truth of the assertion, even though this has not been proven. [A single incorrect Assume pragma can invalidate an arbitrarily large number of proofs - the responsibility for ensuring correctness rests entirely upon the user.]
Examples
1-- The up-time timer is updated once a second
2package Up_Timer
3 with SPARK_Mode
4is
5 type Time_Register is limited private;
6 type Times is range 0 .. 2**63 - 1;
7
8 procedure Inc (Up_Time : in out Time_Register);
9
10 function Get (Up_Time : Time_Register) return Times;
11
12private
13 type Time_Register is record
14 Time : Times := 0;
15 end record;
16end Up_Timer;
1package body Up_Timer
2 with SPARK_Mode
3is
4 procedure Inc (Up_Time : in out Time_Register) is
5 begin
6 -- The up timer is incremented every second.
7 -- The system procedures require that the system is rebooted
8 -- at least once every three years - as the Timer_Reg is a 64 bit
9 -- integer it cannot reach Times'Last before a system reboot.
10 pragma Assume (if Times'Last = 2**63 - 1 then Up_Time.Time < Times'Last);
11
12 -- Without the previous assume statement it would not be possible
13 -- to prove that the following addition would not overflow.
14 Up_Time.Time := Up_Time.Time + 1;
15 end Inc;
16
17 function Get (Up_Time : Time_Register) return Times is (Up_Time.Time);
18end Up_Timer;