Implementation Defined Annotations
This appendix lists all the uses of aspect or pragma Annotate for
GNATprove. Aspect or pragma Annotate can also be used to control other
AdaCore tools. The uses of such annotations are explained in the User’s Guide
of each tool.
Annotations in GNATprove are useful in two cases:
for justifying check messages using Direct Justification with Pragma Annotate, typically using a pragma rather than an aspect, as the justification is generally associated to a statement or declaration.
for influencing the generation of proof obligations, typically using an aspect rather than a pragma, as the annotation is generally associated to an entity in that case. Some of these uses can be seen in SPARK Libraries for example. Some of these annotations introduce additional assumptions which are not verified by the GNATprove tool, and thus should be used with care.
When the annotation is associated to an entity, both the pragma and aspect form can be used and are equivalent, for example on a subprogram:
function Func (X : T) return T
with Annotate => (GNATprove, <annotation name>);
or
function Func (X : T) return T;
pragma Annotate (GNATprove, <annotation name>, Func);
In the following, we use the aspect form whenever possible.
Annotation for Justifying Check Messages
You can use annotations of the form
pragma Annotate (GNATprove, False_Positive,
"message to be justified", "reason");
to justify an unproved check message that cannot be proved by other means. See
the section Direct Justification with Pragma Annotate for more details
about this use of pragma Annotate.
Annotation for Skipping Parts of the Analysis for an Entity
Subprograms, packages, tasks, entries and protected subprograms can be annotated to skip flow analysis, and to skip generating proof obligations for their implementation, and the implementations of all such entities defined inside.
procedure P
with Annotate => (GNATprove, Skip_Proof);
procedure P
with Annotate => (GNATprove, Skip_Flow_And_Proof);
If an entity is annotated with Skip_Proof, no messages related to possible
run-time errors and functional contracts are issued for this entity and any
contained entities. This is similar to specifying --mode=flow on the command
line (see Effect of Mode on Output), except that the effect is limited
to this entity (and enclosed entities).
If an entity is annotated with Skip_Flow_And_Proof, in addition, no messages
related to global contracts, initialization and dependency relations are issues
for this entity and any contained entities. This is similar to specifying
--mode=check-all on the command line, expect that the effect is limited to
this entity (and enclosed entities).
Note that the Skip_Proof annotation cannot be used if an enclosing
subprogram already has the Skip_Flow_And_Proof annotation.
Annotation for Handling Modular Types as Integers in All Provers
Modular types are handled as a special bitvector type in some provers, which
may lead to more difficult automatic proofs when such values are combined with
integers that come from signed integers in SPARK or Big_Integers from the
SPARK Library.
In such a case, it is possible to request that a modular type is handled like an integer in all provers, by using annotations of the form:
type T is mod 2**32
with Annotate => (GNATprove, No_Bitwise_Operations);
or on a derived type:
type T is new U
with Annotate => (GNATprove, No_Bitwise_Operations);
This annotation is inherited by derived types. It must be specified on a type
declaration (and cannot be specified on a subtype declaration). The following
bitwise operations are not allowed on such a type: or, and, xor,
not, Shift_Left, Shift_Right, Shift_Right_Arithmetic,
Rotate_Left, Rotate_Right.
Annotation for Overflow Checking on Modular Types
The standard semantics of arithmetic on modular types is that operations wrap around, hence GNATprove issues no overflow checks on such operations. You can instruct it to issue such checks (hence detecting possible wrap-around) using annotations of the form:
type T is mod 2**32
with Annotate => (GNATprove, No_Wrap_Around);
or on a derived type:
type T is new U
with Annotate => (GNATprove, No_Wrap_Around);
This annotation is inherited by derived types. It must be specified on a type
declaration (and cannot be specified on a subtype declaration). All four binary
arithmetic operations + - * ** are checked for possible overflows. Division
cannot lead to overflow. Unary negation is checked for possible non-nullity of
its argument, which leads to overflow. The predecessor attribute 'Pred and
successor attribute 'Succ are also checked for possible overflows.
Annotation for Simplifying Iteration for Proof
The translation presented in Aspect and Pragma Iterable
may produce complicated proofs,
especially when verifying complex properties over sets. The GNATprove
annotation Iterable_For_Proof can be used to change the way for ... of
quantification is translated. More precisely, it allows to provide GNATprove
with a Contains function, that will be used for quantification. For example,
on our sets, we could write:
function Mem (S : Set; E : Element_Type) return Boolean;
pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Mem);
With this annotation, the postcondition of Intersection is translated in a
simpler way, using logic quantification directly over elements:
(for all E : Element_Type =>
(if Mem (Intersection'Result, E) then Mem (S1, E) and Mem (S2, E)))
and (for all E : Element_Type =>
(if Mem (S1, E) then
(if Mem (S2, E) then Mem (Intersection'Result, E))))
Note that care should be taken to provide an appropriate function contains,
which returns true if and only if the element E is present in S. This
assumption will not be verified by GNATprove.
The annotation Iterable_For_Proof can also be used in another case.
Operations over complex data structures are sometimes specified using operations
over a simpler model type. In this case, it may be more appropriate to translate
for ... of quantification as quantification over the model’s cursors. As an
example, let us consider a package of linked lists that is specified using a
sequence that allows accessing the element stored at each position:
package Lists with SPARK_Mode is
type Sequence is private with
Ghost,
Iterable => (...,
Element => Get);
function Length (M : Sequence) return Natural with Ghost;
function Get (M : Sequence; P : Positive) return Element_Type with
Ghost,
Pre => P <= Length (M);
type Cursor is private;
type List is private with
Iterable => (...,
Element => Element);
function Position (L : List; C : Cursor) return Positive with Ghost;
function Model (L : List) return Sequence with
Ghost,
Post => (for all I in 1 .. Length (Model'Result) =>
(for some C in L => Position (L, C) = I));
function Element (L : List; C : Cursor) return Element_Type with
Pre => Has_Element (L, C),
Post => Element'Result = Get (Model (L), Position (L, C));
function Has_Element (L : List; C : Cursor) return Boolean with
Post => Has_Element'Result = (Position (L, C) in 1 .. Length (Model (L)));
procedure Append (L : in out List; E : Element_Type) with
Post => length (Model (L)) = Length (Model (L))'Old + 1
and Get (Model (L), Length (Model (L))) = E
and (for all I in 1 .. Length (Model (L))'Old =>
Get (Model (L), I) = Get (Model (L'Old), I));
function Init (N : Natural; E : Element_Type) return List with
Post => length (Model (Init'Result)) = N
and (for all F of Init'Result => F = E);
Elements of lists can only be accessed through cursors. To specify easily the
effects of position-based operations such as Append, we introduce a ghost
type Sequence, that is used to represent logically the content of the linked
list in specifications.
The sequence associated to a list can be constructed using the Model
function. Following the usual translation scheme for quantified expressions, the
last line of the postcondition of Init is translated for proof as:
(for all C : Cursor =>
(if Has_Element (Init'Result, C) then Element (Init'Result, C) = E));
Using the definition of Element and Has_Element, it can then be refined
further into:
(for all C : Cursor =>
(if Position (Init'Result, C) in 1 .. Length (Model (Init'Result))
then Get (Model (Init'Result), Position (Init'Result, C)) = E));
To be able to link this property with other properties specified directly on
models, like the postcondition of Append, it needs to be lifted to iterate
over positions instead of cursors. This can be done using the postcondition of
Model that states that there is a valid cursor in L for each position of
its model. This lifting requires a lot of quantifier reasoning from the prover,
thus making proofs more difficult.
The GNATprove Iterable_For_Proof annotation can be used to provide
GNATprove with a Model function, that will be to translate quantification on
complex containers toward quantification on their model. For example, on our
lists, we could write:
function Model (L : List) return Sequence;
pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Entity => Model);
With this annotation, the postcondition of Init is translated directly as a
quantification on the elements of the result’s model:
(for all I : Positive =>
(if I in 1 .. Length (Model (Init'Result)) then
Get (Model (Init'Result), I) = E));
Like with the previous annotation, care should be taken to define the model
function such that it always return a model containing exactly the same elements
as L.
Note
It is not possible to specify more than one Iterable_For_Proof annotation
per container type with an Iterable aspect.
Annotation for Inlining Functions for Proof
Contracts for functions are generally translated by GNATprove as axioms on otherwise undefined functions. As an example, consider the following function:
function Increment (X : Integer) return Integer with
Post => Increment'Result >= X;
It will be translated by GNATprove as follows:
function Increment (X : Integer) return Integer;
axiom : (for all X : Integer. Increment (X) >= X);
For internal reasons due to ordering issues, expression functions are also defined using axioms. For example:
function Is_Positive (X : Integer) return Boolean is (X > 0);
will be translated exactly as if its definition was given through a postcondition, namely:
function Is_Positive (X : Integer) return Boolean;
axiom : (for all X : Integer. Is_Positive (X) = (X > 0));
This encoding may sometimes cause difficulties to the underlying solvers, especially for quantifier instantiation heuristics. This can cause strange behaviors, where an assertion is proven when some calls to expression functions are manually inlined but not without this inlining.
If such a case occurs, it is sometimes possible to instruct the tool to inline
the definition of expression functions using pragma Annotate
Inline_For_Proof. When such a pragma is provided for an expression
function, a direct definition will be used for the function instead of an
axiom:
function Is_Positive (X : Integer) return Boolean is (X > 0);
pragma Annotate (GNATprove, Inline_For_Proof, Is_Positive);
The same pragma will also allow to inline a regular function, if its postcondition is simply an equality between its result and an expression:
function Is_Positive (X : Integer) return Boolean with
Post => Is_Positive'Result = (X > 0);
pragma Annotate (GNATprove, Inline_For_Proof, Is_Positive);
In this case, GNATprove will introduce a check when verifying the body of
Is_Positive to make sure that the inline annotation is correct, namely, that
Is_Positive (X) and X > 0 always yield the same result. This check
may not be redundant with the verification of the postcondition of
Is_Positive if the = symbol on booleans has been overridden.
Note that, since the translation through axioms is necessary for ordering
issues, this annotation can sometimes lead to a crash in GNATprove. It is the
case for example when the definition of the function uses quantification over a
container using the Iterable aspect.
Annotation for Referring to a Value at the End of a Local Borrow
Local borrowers are objects of an anonymous access-to-variable type. At their declaration, the ownership of (a part of) an existing data-structure is temporarily transferred to the new object. The borrowed data-structure will regain ownership afterward. During the lifetime of the borrower, the borrowed object can be accessed indirectly through the borrower. It is forbidden to modify or even read the borrowed object during the borrow. As an example, let us consider a recursive type of singly-linked lists:
type List;
type List_Acc is access List;
type List is record
Val : Integer;
Next : List_Acc;
end record;
Using this type, let us construct a list X which stores the numbers from
1 to 5:
X := new List'(1, null);
X.Next := new List'(2, null);
X.Next.Next := new List'(3, null);
X.Next.Next.Next := new List'(4, null);
X.Next.Next.Next.Next := new List'(5, null);
We can borrow the structure designated by X in a local borrower Y:
declare
Y : access List := X;
begin
V := Y.Val; -- OK, ownership has been transferred to Y temporarily
V := X.Val; -- Illegal, X does not have ownership during the scope of Y
end;
While in the scope of Y, the ownership of the list designated by X is
transferred to Y, so that it is not allowed to access it from X
anymore. After the end of the declare block, ownership is restored to X,
which can again be accessed or modified directly.
During the lifetime of the borrower, the borrowed object can be modified indirectly through the borrower. Therefore, when the borrower goes out of scope and ownership is transferred back to the borrowed object, GNATprove needs to reconstruct the new value of the borrowed object from the value of the borrower at the end of the borrow. In general, it can be done entirely automatically. However, it can happen that the exact relation between the values of the borrowed object and the borrower at the end of the borrow is lost by the tool. In particular, it is the case when the borrower is created inside a (traversal) function, as proof is modular on a per subprogram basis. It also happens when the borrower is modified inside a loop, as analysing loops involves cutpoints. In this case, GNATprove relies on the user to adequately describe the link between the values of the borrowed object and the borrower at the end of the borrow inside annotations - postconditions of traversal functions or loop invariants.
To this effect, it is possible to refer to the value of a local borrower or a
borrowed expression at the end of the borrow using a ghost identity function
annotated with At_End_Borrow. Calls to these functions are interpreted by
the tool as markers of references to values at the end of the borrow:
function At_End_Borrow (E : access constant List_Acc) return access constant List_Acc is
(E)
with Ghost,
Annotate => (GNATprove, At_End_Borrow);
Note that the name of the function could be something other than
At_End_Borrow.
GNATprove will check that a function associated with the At_End_Borrow
annotation is a ghost expression function which takes a single parameter of an
access-to-constant type and returns it. At_End_Borrow functions can only be
called inside regular assertions or contracts, within a parameter of a call
to a lemma subprogram, or within the initialization of a (ghost) constant
of anonymous access-to-constant type.
When GNATprove encounters a call to such a function, it checks that the
actual parameter of the call is either a local borrower or an
expression which is borrowed in the current scope. It does not interpret it as
the current value of the expression, but rather as what is usually called a
prophecy variable in the literature, namely, an imprecise value
representing the value that the expression will have at the end of the borrow.
As GNATprove does not do any look-ahead, nothing will be known about the
actual value of a local borrower at the end of the borrow.
However, the tool will still
be aware of the relation between this final value and the final value of the
expression it borrows. As an example, consider a local borrower Y of the
list X as defined above. The At_End_Borrow function can be used
to give properties that are known to hold during the scope of Y.
For example, since Y and X designate the same value, GNATprove can
verify that no matter what happens during the scope of Y, at the end of the
borrow, the Val component of X will be the Val component of Y:
pragma Assert (At_End_Borrow (X).Val = At_End_Borrow (Y).Val);
However, even though at the beginning of the declare block, the first value of
X is 1, it is not correct to assert that it will necessarily be so at the
end of the borrow:
pragma Assert (Y.Val = 1); -- proved
pragma Assert (At_End_Borrow (X).Val = 1); -- incorrect
Indeed, Y could be modified later so that X.Val is not 1 anymore:
declare
Y : access List := X;
begin
Y.Val := 2;
end;
pragma Assert (X.Val = 2);
Note that the assertion above is invalid even if Y.Val is not modified in
the following statements. It needs to be provable only from the information
available at the assertion point, not knowing what will actually happen later
in the scope of the borrow. The analysis performed by GNATprove only
considers those statements that occur before the assertion to be proved;
GNATprove does not consider statements that occur later in the control flow.
In other words, there is no lookahead when an assertion is to be proved.
Note
Since At_End_Borrow functions are identity functions, the current values
of the borrower and borrowed expression are used when executing assertions
containing prophecy variables. This is sound. Indeed, GNATprove will show
that the assertion holds for all possible modifications of the borrower. As
not modifying the borrower is a valid senario, this is enough to ensure that
the assertion necessarily evaluates to True at runtime.
Let us now consider a case where X is not borrowed completely. In the
declaration of Y, we can decide to borrow only the last three elements of
the list:
declare
Y : access List := X.Next.Next;
begin
pragma Assert (At_End_Borrow (X.Next.Next).Val = At_End_Borrow (Y).Val);
pragma Assert (At_End_Borrow (X.Next.Next) /= null);
-- Proved, this follows from the relationship between X and Y
pragma Assert (At_End_Borrow (X.Next.Next.Val) = 3);
-- Incorrect, X could be modified through Y
X.Val := 42;
end;
Here, like in the previous example, we can state that, at the end of the borrow,
X.Next.Next.Val is Y.Val, and then X.Next.Next cannot be set to
null. We cannot assume anything about the
part of X designated by Y, so we won’t be able to prove that
X.Next.Next.Val will remain 3. Note that we cannot get the value at the
end of the borrow of an expression which is not borrowed in the current scope.
Here, even if X.Next.Next is borrowed, X and X.Next are not. As
a result, calls to At_End_Borrow on them will be rejected by the tool.
Inside the scope of Y, it is possible to modify the variable Y itself,
as opposed to modifying the structure it designates, so that it gives access to
a subcomponent of the borrowed structure. It is called a reborrow. During a
reborrow, the part of the structure designated by the borrower is reduced, so
the prophecy variable giving the value of the borrower at the end of the
borrow is reduced as well. The part of the borrowed expression which is no
longer accessible through the borrower cannot be modified anymore for the
rest of the borrow. It is said to be frozen and its final value is known. For
example, let’s use Y to borrow X entirely and then modify it to only
designate X.Next.Next:
declare
Y : access List := X;
begin
Y := Y.Next.Next; -- reborrow
pragma Assert (At_End_Borrow (X).Next.Next /= null);
pragma Assert (At_End_Borrow (X).Val = 1);
pragma Assert (At_End_Borrow (X).Next.Val = 2);
pragma Assert (At_End_Borrow (X).Next.Next.Val = 3); -- incorrect
pragma Assert (At_End_Borrow (X).Next.Next.Next /= null); -- incorrect
end;
After the reborrow, the part of X still accessible from the borrower is
reduced, but since X was borrowed entirely to begin with, the ownership
policy of SPARK still forbids direct access to any components of X while
in the scope of Y. As a result, we have more information about the
final value of X than in the previous case. We still know that X
will hold at least three elements, that is X.Next.Next /= null.
Additionally, the first and second components of X are no longer accessible
from Y, and since they cannot be accessed directly through X, we know
that they will keep their current values. This is why we can now assert that,
at the end of the borrow, X.Val is 1 and X.Next.Val is 2.
However, we still cannot know anything
about the part of X still accessible from Y as these properties
could be modified later in the borrow:
Y.Val := 42;
Y.Next := null;
During sequences of re-borrows, it is additionally possible to use constants of anonymous access-to-constant type in order to save prophecy variables for intermediate values of an access variable, as in the following example:
declare
Y : access List := X;
begin
Y := Y.Next; -- first reborrow
declare
Z : constant access constant List := At_End_Borrow (Y) with Ghost;
-- At_End_Borrow is Ghost, so Z too.
begin
Y := Y.Next; -- second reborrow
pragma Assert (At_End_Borrow (X).Next.Val = Z.Val);
-- Z match prophecy of first reborrow of Y
pragma Assert (Z.Next.Val = At_End_Borrow (Y).Val);
end
end
As Z serves to save a prophecy variable, it is subject to the same
usage restrictions as the corresponding At_End_Borrow (Y) call, in place
of the usual rules for local observers.
As said earlier, in general, GNATprove can handle local borrows without
any additional user written annotations. Therefore, At_End_Borrow functions
are mostly useful at places where information is lost by the tool: in
postconditions of borrowing traversal functions (which return a local
borrower of their first parameter) and in loop invariants if the
loop involves a reborrow (in this case the value of the borrower at the end
of the borrow is modified inside the loop and needs to be described in the
invariant). Let us consider the following example:
1with SPARK.Big_Integers; use SPARK.Big_Integers;
2with SPARK.Big_Intervals; use SPARK.Big_Intervals;
3with Lists; use Lists;
4
5procedure List_Borrows with SPARK_Mode is
6
7 function Length (L : access constant List) return Big_Natural is
8 (if L = null then 0 else Length (L.Next) + 1)
9 with Subprogram_Variant => (Structural => L);
10
11 function Get (L : access constant List; P : Big_Positive) return Integer is
12 (if P = Length (L) then L.Val else Get (L.Next, P))
13 with Subprogram_Variant => (Structural => L),
14 Pre => P <= Length (L);
15
16 function Eq (L, R : access constant List) return Boolean is
17 (Length (L) = Length (R)
18 and then (for all P in Interval'(1, Length (L)) => Get (L, P) = Get (R, P)))
19 with Annotate => (GNATprove, Inline_For_Proof);
20
21 function Tail (L : access List) return access List with
22 Contract_Cases =>
23 (L = null =>
24 Tail'Result = null and At_End_Borrow (L) = null,
25 others => At_End_Borrow (L).Val = L.Val
26 and Eq (L.Next, Tail'Result)
27 and Eq (At_End_Borrow (L).Next, At_End_Borrow (Tail'Result)));
28 -- No matter what is done later with the result of Tail, at the end of the
29 -- borrow L.Val will be the current value of L.Val and the remainder of the
30 -- list will be the (updated) value of Tail'Result.
31
32 function Tail (L : access List) return access List is
33 begin
34 if L = null then
35 return null;
36 else
37 return L.Next;
38 end if;
39 end Tail;
40
41 procedure Set_All_To_Zero (L : access List) with
42 Post => Length (L) = Length (L)'Old
43 and then (for all P in Interval'(1, Length (L)) => Get (L, P) = 0);
44
45 procedure Set_All_To_Zero (L : access List) is
46 X : access List := L;
47 C : Big_Natural := 0 with Ghost;
48 -- Number of traversed elements
49
50 begin
51 while X /= null loop
52 pragma Loop_Invariant (C = Length (X)'Loop_Entry - Length (X));
53 -- C is the number of traversed elements
54 pragma Loop_Invariant
55 (Length (At_End_Borrow (L)) = C + Length (At_End_Borrow (X)));
56 -- At the end of the borrow, L will have C more elements than X
57 pragma Loop_Invariant
58 (for all P in Interval'(1, Length (At_End_Borrow (L))) =>
59 (if P <= Length (At_End_Borrow (X))
60 then Get (At_End_Borrow (L), P) = Get (At_End_Borrow (X), P)
61 else Get (At_End_Borrow (L), P) = 0));
62 -- At the end of the borrow, the tail of L will be X and the rest
63 -- will contain zeros.
64
65 X.Val := 0;
66 X := X.Next; -- Reborrow
67 C := C + 1;
68 end loop;
69 end Set_All_To_Zero;
70
71 X : List_Acc :=
72 new List'(1, new List'(2, new List'(3, new List'(4, new List'(5, null)))));
73begin
74 declare
75 Y : access List := Tail (X.Next);
76 begin
77 Y.Val := 42;
78 end;
79
80 pragma Assert (X.Val = 1);
81 pragma Assert (X.Next.Val = 2);
82 pragma Assert (X.Next.Next.Val = 42);
83 pragma Assert (X.Next.Next.Next.Val = 4);
84end List_Borrows;
The function Tail is a borrowing traversal function. It
returns a local borrower of its parameter L. As GNATprove works modularly
on a per subprogram basis, it is necessary to specify in its postcondition how
the value of the borrowed parameter L can be reconstructed from the value
of the borrower Tail'Result at the end of the borrow. Otherwise, GNATprove
would not be able to recompute the value of the borrowed parameter after the
returned borrower goes out of scope in the caller.
The Tail function returns the Next component of a list if there is one,
and null otherwise. As pointer equality is not allowed in SPARK, we
define our own equality function Eq which compares the elements of the list
one by one. Note that the Get function indexes the list from the end (the
first element of the list is accessed by Get (L, Length (L))). This is
done to avoid arithmetic in the recursive definition of Get as it slows
the proofs down.
In the postcondition of Tail, we consider the two cases, and, in each case,
specify both the value returned by the function and how the
parameter L is related to the returned borrower:
If
LisnullthenTailreturnsnullandLwill staynullfor the duration of the borrow.Otherwise,
TailreturnsL.Next, the first element ofLwill stay as it was at the time of call, and the rest ofLstays equal to the object returned byTail.
Thanks to this postcondition, GNATprove can verify a program which borrows a
part of L using the Tail function and modifies L through this
borrower, as can be seen in the body of List_Borrows.
Postconditions of borrowing traversal functions systematically need to provide
two properties: one specifying the result, and another specifying how the
parameter is related to the borrower. This is generally redundant, as by
nature the parameter/borrower relation always holds at the
point of return of the function.
For example, on the post of Tail, Eq (L.Next, Tail'Result) repeats
Eq (At_End_Borrow (L).Next, At_End_Borrow (Tail'Result)).
The tool limits that redundancy by letting the user write only the
parameter/borrower relation. Properties of the result are automatically derived
by duplicating the postcondition, with calls to At_End_Borrow replaced by
their arguments. This covers most (if not all) properties of the result,
and additional properties of the result can be explicitly written if needed.
This means we get equivalent behavior for function Tail
by removing the second conjunct of the postcondition.
At_End_Borrow functions are also useful to write loop invariants in loops
involving reborrows. This is exemplified in the Set_All_To_Zero procedure
which traverses a list and sets all its elements to 0. The variable X
borrows the whole input list L at the beginning of the function. Inside the
loop, X is used to modify the structure designated by L. At the end of
the procedure, ownership is transferred back to L automatically. To
prove the postcondition of Set_All_To_Zero, GNATprove needs to know
precisely how to reconstruct the value of L at this point. As X is
reborrowed in the loop, the relation between its value and the value of L at
the end of the borrow (the end of the scope of X) changes at each iteration.
At the beginning of the loop, X is an alias of L, so the value
designated by L is equal to the value designated by X at the end of the
borrow. At each iteration, an element is dropped from X, so the value
designated by the current value of X at the end of the borrow shrinks. At
the same time, we get more information about the value designated by L at
the end of the borrow as more and more elements are frozen and therefore
definitely set to their current value, that is, 0.
Because proof uses cutpoints to reason about loops, it is necessary to supply
all this information in a loop invariant. This is what is done in the body of
Set_All_To_Zero. To help readability, a ghost variable C is introduced
to count the number of iterations in the loop. The first invariant is a regular
invariant, it maintains the value of C at each iteration. The two following
ones are used to describe how L can be reconstructed from X at the
end of the borrow: L will be made of C zeros followed by the final
value of X. Note that, in the invariant, no assumption is made about the
changes that can be made to X during the rest of the borrow, there is no
look ahead. Both Tail and Set_All_To_Zero can be entirely verified
by GNATprove:
1list_borrows.adb:7:13: info: implicit aspect Always_Terminates on "Length" has been proved, subprogram will terminate
2list_borrows.adb:8:24: info: predicate check proved
3list_borrows.adb:8:31: info: subprogram variant proved
4list_borrows.adb:8:31: info: predicate check proved
5list_borrows.adb:8:40: info: pointer dereference check proved
6list_borrows.adb:8:47: info: predicate check proved
7list_borrows.adb:8:49: info: predicate check proved
8list_borrows.adb:11:13: info: implicit aspect Always_Terminates on "Get" has been proved, subprogram will terminate
9list_borrows.adb:12:10: info: predicate check proved
10list_borrows.adb:12:14: info: predicate check proved
11list_borrows.adb:12:31: info: pointer dereference check proved
12list_borrows.adb:12:41: info: subprogram variant proved
13list_borrows.adb:12:41: info: precondition proved
14list_borrows.adb:12:47: info: pointer dereference check proved
15list_borrows.adb:14:13: info: predicate check proved
16list_borrows.adb:14:18: info: predicate check proved
17list_borrows.adb:16:13: info: implicit aspect Always_Terminates on "Eq" has been proved, subprogram will terminate
18list_borrows.adb:17:07: info: predicate check proved
19list_borrows.adb:17:20: info: predicate check proved
20list_borrows.adb:18:58: info: precondition proved
21list_borrows.adb:18:66: info: predicate check proved
22list_borrows.adb:18:71: info: precondition proved
23list_borrows.adb:18:79: info: predicate check proved
24list_borrows.adb:21:13: info: implicit aspect Always_Terminates on "Tail" has been proved, subprogram will terminate
25list_borrows.adb:23:18: info: contract case proved
26list_borrows.adb:25:18: info: contract case proved
27list_borrows.adb:25:38: info: pointer dereference check proved
28list_borrows.adb:25:46: info: pointer dereference check proved
29list_borrows.adb:26:20: info: pointer dereference check proved
30list_borrows.adb:27:36: info: pointer dereference check proved
31list_borrows.adb:37:18: info: dynamic accessibility check proved
32list_borrows.adb:37:18: info: pointer dereference check proved
33list_borrows.adb:42:14: info: predicate check proved
34list_borrows.adb:42:14: info: postcondition proved
35list_borrows.adb:42:37: info: predicate check proved
36list_borrows.adb:43:57: info: precondition proved
37list_borrows.adb:43:65: info: predicate check proved
38list_borrows.adb:47:26: info: predicate check proved
39list_borrows.adb:52:33: info: predicate check proved
40list_borrows.adb:52:33: info: loop invariant initialization proved
41list_borrows.adb:52:33: info: loop invariant preservation proved
42list_borrows.adb:52:47: info: predicate check proved
43list_borrows.adb:52:61: info: predicate check proved
44list_borrows.adb:55:13: info: predicate check proved
45list_borrows.adb:55:13: info: loop invariant initialization proved
46list_borrows.adb:55:13: info: loop invariant preservation proved
47list_borrows.adb:55:42: info: predicate check proved
48list_borrows.adb:55:46: info: predicate check proved
49list_borrows.adb:58:13: info: loop invariant preservation proved
50list_borrows.adb:58:13: info: loop invariant initialization proved
51list_borrows.adb:59:21: info: predicate check proved
52list_borrows.adb:59:26: info: predicate check proved
53list_borrows.adb:60:23: info: precondition proved
54list_borrows.adb:60:47: info: predicate check proved
55list_borrows.adb:60:52: info: precondition proved
56list_borrows.adb:60:76: info: predicate check proved
57list_borrows.adb:61:23: info: precondition proved
58list_borrows.adb:61:47: info: predicate check proved
59list_borrows.adb:65:11: info: pointer dereference check proved
60list_borrows.adb:66:16: info: pointer dereference check proved
61list_borrows.adb:67:15: info: predicate check proved
62list_borrows.adb:67:17: info: predicate check proved
63list_borrows.adb:67:19: info: predicate check proved
64
65list_borrows.adb:71:04: medium: resource or memory leak might occur at end of scope
66 71>| X : List_Acc :=
67 72 | new List'(1, new List'(2, new List'(3, new List'(4, new List'(5, null)))));
68list_borrows.adb:75:33: info: pointer dereference check proved
69 in reconstructed value at the end of the borrow at list_borrows.adb:75
70list_borrows.adb:77:08: info: pointer dereference check proved
71list_borrows.adb:80:19: info: assertion proved
72list_borrows.adb:80:20: info: pointer dereference check proved
73list_borrows.adb:81:19: info: assertion proved
74list_borrows.adb:81:20: info: pointer dereference check proved
75list_borrows.adb:81:25: info: pointer dereference check proved
76list_borrows.adb:82:19: info: assertion proved
77list_borrows.adb:82:20: info: pointer dereference check proved
78list_borrows.adb:82:25: info: pointer dereference check proved
79list_borrows.adb:82:30: info: pointer dereference check proved
80list_borrows.adb:83:19: info: assertion proved
81list_borrows.adb:83:20: info: pointer dereference check proved
82list_borrows.adb:83:25: info: pointer dereference check proved
83list_borrows.adb:83:30: info: pointer dereference check proved
84list_borrows.adb:83:35: info: pointer dereference check proved
Annotation for Accessing the Logical Equality for a Type
In Ada, the equality is not the logical equality in general. In particular, arrays are considered to be equal if they contain the same elements, even with different bounds, +0.0 and -0.0 are considered equal…
It is possible to use a pragma Annotate (GNATprove, Logical_Equal) to ask
GNATprove to interpret a function with an equality profile as the logical
equality for the type. If the function body is visible in
SPARK, a check will be emitted to ensure that it indeed checks for logical
equality as understood by the proof engine (which depends on the underlying
model used by the tool, see below).
It comes in handy for example to express that a (part of a) data-structure
is left unchanged by a procedure, as is done in the example below:
subtype Length is Natural range 0 .. 100;
type Word (L : Length := 0) is record
Value : String (1 .. L);
end record;
function Real_Eq (W1, W2 : String) return Boolean with
Ghost,
Import,
Annotate => (GNATprove, Logical_Equal);
type Dictionary is array (Positive range <>) of Word;
procedure Set (D : in out Dictionary; I : Positive; W : String) with
Pre => I in D'Range and W'Length <= 100,
Post => D (I).Value = W
and then (for all J in D'Range =>
(if I /= J then Real_Eq (D (J).Value, D'Old (J).Value)))
is
begin
D (I) := (L => W'Length, Value => W);
end Set;
The actual interpretation of logical equality is highly dependent on the underlying model used for formal verification. However, the following properties are always valid, no matter the actual type on which a logical equality function applies:
Logical equality functions are equivalence relations, that is, they are reflexive, symmetric, and transitive. This implies that such functions can always be used to express that something is preserved as done above.
There is no way to tell the difference between between two values which are logically equal. Said otherwise, all SPARK compatible functions will return the same result on logically equal inputs. Note that Ada functions which do not follow SPARK assumptions may not, for example, if they compare the address of pointers which are not modelled by GNATprove. Such functions should never be used inside SPARK code as they can introduce soundness issues.
Logical equality is handled efficiently, in a builtin way, by the underlying solvers. This is different from the regular Ada equality which is basically handled as a function call, using potentially complex defining axioms (in particular Ada equality over arrays involves quantifiers).
Note
In Ada, copying an expression might not necessarily return a logically equal value. This happens for example when a value is assigned into a variable or returned by a function. Indeed, such copies might involve for example sliding (for arrays) or a partial copy (for view conversions of tagged types).
It might happen that the underlying model of values of an Ada type contain
components which are not present in the Ada value. This makes it impossible to
implement a comparison function in Ada which would compute logical equality on
such types. This is the case in particular for arrays and discriminated
records with variant parts. More precisely, logical equality can be implemented
using the regular Ada equality for discrete types and fixed point types.
For floating point types, both the value and the sign need to be compared
(to tell the difference between +0.0 and -0.0). For pointers, as the address
is not modeled in SPARK, it is enough to check for nullity and compare the
designated value. Logical equality on untagged record with no variant parts can
be achieved by comparing the components. For other composite types, it cannot
be implemented and has to remain non-executable as in the example above.
Additionally, a user can safely annotate a comparison function on private types
whose full view is not in SPARK using the Logical_Equal annotation if it
behaves as expected, namely, it is an equivalence relation, and there is no way,
using the API provided in the public part of the enclosing package, to tell
the difference between two values on which this function returns True.
Note
For private types whose full view is not in SPARK, GNATprove will peek inside the full view to try and determine whether or not to interpret the primitive equality on such types as the logical equality.
Note that, for types on which implementing the logical equality in Ada is impossible, GNATprove might not be able to prove that two Ada values are logically equal even if there is no way to tell the difference in SPARK. For example, it might not be able to prove that two arrays are logically equal even if they have the same bounds and the same value. It is because it is not necessarily true in the underlying model, where values outside of the array bounds are represented. Therefore, using an assumption to state that two objects which are equal-in-Ada are logically equal might introduce an unsoundness, in particular in the presence of slices. It is demonstrated in the example below where GNATprove can prove that two strings are not logically equal even though they have the same bounds and the same elements. However, logical equality can be used safely as long as everything is proved correct (no assumption is used).
procedure Test is
S1 : constant String := "foo1";
S2 : constant String := "foo2";
begin
pragma Assert (S1 (1 .. 3) = S2 (1 .. 3));
pragma Assert (not Real_Eq (S1 (1 .. 3), S2 (1 .. 3)));
end Test;
Annotation for the Predefined Equality of Private Types
In Ada, an equality operator is predefined for almost all types (except limited types). This predefined equality depends on the shape of the type. It is also possible to override the equality operator for a given type. This overriding is called the primitive equality of the type. Depending on the context, the predefined or the primitive equality of a type might be used. In particular, implicit equality operations on types which are not record types - in membership tests or predefined equality of composite types typically - uses the predefined equality, even if a primitive equality is supplied for the type.
In general, predefined equality operators are handled precisely by GNATprove
following the semantics of Ada. However, when the full view of a private type
is not visible in SPARK, it might not be possible to do so. In this case,
GNATprove approximates the behavior of the predefined equality by peeking
beyond SPARK_Mode boundaries into the full view of the type. If it can
determine that it is safe to do so, it will handle the predefined equality of
a private type as the logical equality (see
Annotation for Accessing the Logical Equality for a Type). Otherwise,
the predefined equality of the private type will be left unspecified and nothing
will be provable about it.
It is possible for a user to short-circuit this mechanism and instead specify
directly on a private type whose full view is not in SPARK how the predefined
equality should be handled using the Predefined_Equality annotation. If this
annotation is provided on a type, it will be trusted and GNATprove will not
peek into the full view. For now, the following profiles are supported:
No_Equality: GNATprove will make sure that the predefined equality of the private type is never used. It can be a good way to ensure that users of a library use the primitive equality instead. This is the default handling of GNATprove for visible composite types containing a component of an access-to-object type.Only_Null: GNATprove will make sure that the predefined equality of the private type is only used when one of the operands is a specific constant annotated as theNull_Value. This is the default handling of GNATprove for visible access-to-object types.
As an example consider the following package. An appropriate equality for the
Unbounded_String type is provided as a primitive equality in
Unbounded_Strings. The Predefined_Equality annotation is used to make
sure that its predefined equality will never be called by programs using this
library. It is necessary in particular so that the To_Unbounded_String
function can be used safely even though it will produce different pointers each
time it is called.
package Unbounded_Strings is
type Unbounded_String is private with
Default_Initial_Condition => False,
Annotate => (GNATprove, Predefined_Equality, "No_Equality");
function "=" (X, Y : Unbounded_String) return Boolean;
function To_Unbounded_String (S : String) return Unbounded_String;
function To_String (S : Unbounded_String) return String;
private
pragma SPARK_Mode (Off);
type Unbounded_String is not null access constant String;
function "=" (X, Y : Unbounded_String) return Boolean is (X.all = Y.all);
function To_Unbounded_String (S : String) return Unbounded_String is
(new String'(S));
function To_String (S : Unbounded_String) return String is
(S.all);
end Unbounded_Strings;
It would be possible instead to provide a specific
Null_String value on which the predefined equality is allowed:
package Unbounded_Strings is
type Unbounded_String is private with
Default_Initial_Condition => Unbounded_String = Null_String,
Annotate => (GNATprove, Predefined_Equality, "Only_Null");
Null_String : constant Unbounded_String with
Annotate => (GNATprove, Predefined_Equality, "Null_Value");
function To_Unbounded_String (S : String) return Unbounded_String;
function To_String (S : Unbounded_String) return String with
Pre => S /= Null_String;
private
pragma SPARK_Mode (Off);
type Unbounded_String is access constant String;
Null_String : constant Unbounded_String := null;
function To_Unbounded_String (S : String) return Unbounded_String is
(new String'(S));
function To_String (S : Unbounded_String) return String is
(S.all);
end Unbounded_Strings;
Annotation for Enforcing Ownership Checking on a Private Type
Private types whose full view is not in SPARK can be annotated with a
pragma Annotate (GNATprove, Ownership, ...). Such a type is handled by
GNATprove in accordance to the Memory Ownership Policy of SPARK.
For example, the type T declared in the procedure Simple_Ownership
below has an ownership annotation. As a result, GNATprove will reject the
second call to Read in the body of Simple_Ownership, because the value
designated by X has been moved by the assignment to Y.
1procedure Simple_Ownership with SPARK_Mode is
2 package Nested is
3 type T is private with
4 Default_Initial_Condition,
5 Annotate => (GNATprove, Ownership);
6
7 function Read (X : T) return Boolean;
8 private
9 pragma SPARK_Mode (Off);
10 type T is null record;
11 function Read (X : T) return Boolean is (True);
12 end Nested;
13 use Nested;
14
15 X : T;
16 Y : T;
17
18begin
19 pragma Assert (Read (X)); -- OK
20
21 Y := X;
22
23 pragma Assert (Read (X)); -- Error, X has been moved
24end Simple_Ownership;
In addition, it is possible to state that a type needs reclamation with a
pragma Annotate (GNATprove, Onwership, "Needs_Reclamation", ...). In
this case, GNATprove emits checks to ensure that the resource is not leaked.
For these checks to be handled precisely, the user should provide a way for
the tool to check that an object has been reclaimed. This can be done by
annotating a function which takes a value of this type as a parameter and
returns a boolean with a
pragma Annotate (GNATprove, Onwership, "Needs_Reclamation", ...) or
pragma Annotate (GNATprove, Onwership, "Is_Reclaimed", ...). This
function is used to check that the resource cannot be leaked. A function
annotated with "Needs_Reclamation" shall return True when its input holds
some resource while a function annotated with "Is_Reclaimed" shall return
True when its input has already been reclaimed. Another possibility is to
annotate a constant of the type with a
pragma Annotate (GNATprove, Onwership, "Reclaimed_Value", ...). Objects are
considered to be reclaimed if they are equal to the provided constant. Note
that constants annotated with "Reclaimed_Value" are not considered to hold
resources themselves, so they can be duplicated. Only one such function or
constant shall be provided for a given type. Three examples of use are given
below.
1package Hidden_Pointers with
2 SPARK_Mode,
3 Always_Terminates
4is
5 type Pool_Specific_Access is private with
6 Default_Initial_Condition => Is_Null (Pool_Specific_Access),
7 Annotate => (GNATprove, Ownership, "Needs_Reclamation");
8
9 function Is_Null (A : Pool_Specific_Access) return Boolean with
10 Global => null,
11 Annotate => (GNATprove, Ownership, "Is_Reclaimed");
12 function Deref (A : Pool_Specific_Access) return Integer with
13 Global => null,
14 Pre => not Is_Null (A);
15
16 function Allocate (X : Integer) return Pool_Specific_Access with
17 Global => null,
18 Post => not Is_Null (Allocate'Result) and then Deref (Allocate'Result) = X;
19 procedure Deallocate (A : in out Pool_Specific_Access) with
20 Global => null,
21 Post => Is_Null (A);
22
23private
24 pragma SPARK_Mode (Off);
25 type Pool_Specific_Access is access Integer;
26end Hidden_Pointers;
The package Hidden_Pointers defines a type Pool_Specific_Access which
is really a pool specific access type. The ownership annotation on
Pool_Specific_Access instructs GNATprove that objects of this type
should abide by the Memory Ownership Policy of SPARK. It also states
that the type needs reclamation when a value is finalized. Because of the
annotation on the Is_Null function, GNATprove will attempt to prove that
Is_Null returns True when an object of type Pool_Specific_Access is
finalized unless it was moved.
The mechanism can also be used for resources which are not linked to memory
management. For example, the package Text_IO defines a limited type
File_Descriptor and uses ownership annotations to force GNATprove to
verify that all file descriptors are closed before being finalized.
1package Text_IO with
2 SPARK_Mode,
3 Always_Terminates
4is
5 type File_Descriptor is limited private with
6 Default_Initial_Condition => not Is_Open (File_Descriptor),
7 Annotate => (GNATprove, Ownership, "Needs_Reclamation");
8
9 function Is_Open (F : File_Descriptor) return Boolean with
10 Global => null,
11 Annotate => (GNATprove, Ownership, "Needs_Reclamation");
12 function Read_Line (F : File_Descriptor) return String with
13 Global => null,
14 Pre => Is_Open (F);
15
16 function Open (N : String) return File_Descriptor with
17 Global => null,
18 Post => Is_Open (Open'Result);
19 procedure Close (F : in out File_Descriptor) with
20 Global => null,
21 Post => not Is_Open (F);
22
23private
24 pragma SPARK_Mode (Off);
25 type Text;
26 type File_Descriptor is access all Text;
27end Text_IO;
In our last example, the ownership annotation is used to enforce the
Memory Ownership Policy of SPARK on pointers used to represent
strings compatible with C. Note that the New_String function has to be
volatile as the predefined equality can be used on Chars_Ptr (it is not
visibly a pointer), so New_String will return visibly different values
each time it is called.
1package C_Strings with
2 SPARK_Mode,
3 Always_Terminates
4is
5 type Chars_Ptr is private with
6 Annotate => (GNATprove, Ownership, "Needs_Reclamation");
7
8 Null_Ptr : constant Chars_Ptr with
9 Annotate => (GNATprove, Ownership, "Reclaimed_Value");
10
11 function New_String (Str : String) return Chars_Ptr with
12 Global => null,
13 Volatile_Function,
14 Post => New_String'Result /= Null_Ptr;
15
16 procedure Free (Item : in out Chars_Ptr) with
17 Global => null,
18 Post => Item = Null_Ptr;
19private
20 pragma SPARK_Mode (Off);
21 type Chars_Ptr is access all Character;
22
23 Null_Ptr : constant Chars_Ptr := null;
24end C_Strings;
Note
The equality used to check whether an object is equal to a reclaimed value is the same as the equality used by membership tests and equality of composite types: it uses the predefined equality even if it has been redefined by the user, unless the type of the operands is ultimately a record type in which case it uses the primitive equality.
Annotation for Instantiating Lemma Procedures Automatically
As featured in Manual Proof Using User Lemmas, it is possible to write
lemmas in SPARK as ghost procedures. However, actual calls to the procedure
need to be manually inserted in the program whenever an instance of the
lemma is necessary.
It is possible to use a pragma Annotate to instruct GNATprove that an
axiom should be introduced for a lemma procedure so manual
instantiations are no longer necessary. This annotation is called
Automatic_Instantiation. As an example, the Equivalent function below
is an equivalence relation. This is expressed using three lemma procedures
which should be instantiated automatically:
function Equivalent (X, Y : Integer) return Boolean with
Global => null;
procedure Lemma_Reflexive (X : Integer) with
Ghost,
Global => null,
Annotate => (GNATprove, Automatic_Instantiation),
Post => Equivalent (X, X);
procedure Lemma_Symmetric (X, Y : Integer) with
Ghost,
Global => null,
Annotate => (GNATprove, Automatic_Instantiation),
Pre => Equivalent (X, Y),
Post => Equivalent (Y, X);
procedure Lemma_Transitive (X, Y, Z : Integer) with
Ghost,
Global => null,
Annotate => (GNATprove, Automatic_Instantiation),
Pre => Equivalent (X, Y) and Equivalent (Y, Z),
Post => Equivalent (X, Z);
Such lemmas should be declared directly after a function declaration, here the
Equivalent function. The axiom will only be available when the associated
function is used in the proof context.
Annotation for Managing the Proof Context
By default, when verifying a part of a program, GNATprove chooses which
information is available for proof based on a liberal notion of visibility:
everything is visible except if it is declared in the body of another
(possibly nested) unit. It assumes values of
global constants, postconditions of called subprograms, bodies of expression
functions… This behavior can be tuned either globally or, in some cases,
specificaly for the analysis of a given unit, using the dual annotations
Hide_Info and Unhide_Info.
Overriding the Default Handling of Visibility
The private part of withed units is visible by GNATprove by default if it is in SPARK. This is useful in particular for units which declare private types as it makes it optional for users to introduce a proper abstraction for these types. As an example, consider the following package:
1package Geometry with SPARK_Mode is
2 type Rectangle is private;
3
4 function Perimeter (X : Rectangle) return Positive;
5
6 function Area (X : Rectangle) return Positive;
7
8 function Is_Square (X : Rectangle) return Boolean;
9private
10 subtype Small_Positive is Positive range 1 .. 100;
11
12 type Rectangle is record
13 Height : Small_Positive;
14 Width : Small_Positive;
15 end record with Predicate => Width <= Height;
16
17 function Perimeter (X : Rectangle) return Positive is
18 (2 * (X.Height + X.Width));
19
20 function Area (X : Rectangle) return Positive is
21 (X.Height * X.Width);
22
23 function Is_Square (X : Rectangle) return Boolean is
24 (X.Height = X.Width);
25end Geometry;
The package Geometry is not annotated with any contract. However, as its
private part is visible, it is still possible to prove programs using this
library:
1with Geometry; use Geometry;
2
3procedure Use_Geometry (X, Y : Rectangle) with
4 SPARK_Mode,
5 Global => null
6is
7begin
8 pragma Assert ((Area (X) >= 3) = (Perimeter (X) >= 8));
9 pragma Assert
10 (if Area (X) = Area (Y) and then Is_Square (X) and then Is_Square (Y)
11 then X = Y);
12end Use_Geometry;
1use_geometry.adb:5:03: info: data dependencies proved
2use_geometry.adb:8:19: info: assertion proved
3use_geometry.adb:10:07: info: assertion proved
This behavior is useful in general. However, when designing complex libraries,
it might be interesting to enforce abstraction in order to reduce the
proof context in user code. It can be done by using a Hide_Info annotation
at the top of the private part of a package:
1package Geometry with SPARK_Mode is
2 type Rectangle is private;
3
4 function Perimeter (X : Rectangle) return Positive;
5
6 function Area (X : Rectangle) return Positive;
7
8 function Is_Square (X : Rectangle) return Boolean;
9private
10 pragma Annotate (GNATprove, Hide_Info, "Private_Part", Geometry);
11
12 subtype Small_Positive is Positive range 1 .. 100;
13
14 type Rectangle is record
15 Height : Small_Positive;
16 Width : Small_Positive;
17 end record with Predicate => Width <= Height;
18
19 function Perimeter (X : Rectangle) return Positive is
20 (2 * (X.Height + X.Width));
21
22 function Area (X : Rectangle) return Positive is
23 (X.Height * X.Width);
24
25 function Is_Square (X : Rectangle) return Boolean is
26 (X.Height = X.Width);
27end Geometry;
Such an annotation is only allowed on library-level packages that are visible
from outside the library unit. This excludes in particular nested packages in
a package body or in a private child package. They cause the private
parts of annotated packages to no longer be visible when verifying
user code. However, they remain visible when analysing enclosing units and
child packages. Note that using this annotation generally requires users to
write additional contracts for user code to remain provable. In particular,
this might include getter or model functions as well as a user-defined
primitive equality with a contract. As an example, with this annotation and
no other changes, Use_Geometry becomes impossible to prove:
1
2use_geometry.adb:8:19: medium: assertion might fail
3 8 | pragma Assert ((Area (X) >= 3) = (Perimeter (X) >= 8));
4 | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
5 possible fix: subprogram at line 3 should mention X in a precondition
6 3 |procedure Use_Geometry (X, Y : Rectangle) with
7 |^ here
8
9use_geometry.adb:11:12: medium: assertion might fail, cannot prove X = Y
10 11 | then X = Y);
11 | ^~~~~
12 possible fix: subprogram at line 3 should mention X and Y in a precondition
13 3 |procedure Use_Geometry (X, Y : Rectangle) with
14 |^ here
Retaining provability can be done for example by introducing ghost functions returning the width and the heigth of a rectangle and using them in the contracts of other functions. The obvious duplication here is the reason why abstraction is not enforced on private parts by default:
1package Geometry with SPARK_Mode is
2 type Rectangle is private;
3
4 function Get_Height (X : Rectangle) return Positive with
5 Ghost,
6 Post => Get_Height'Result <= 100;
7
8 function Get_Width (X : Rectangle) return Positive with
9 Ghost,
10 Post => Get_Width'Result <= Get_Height (X);
11
12 function Perimeter (X : Rectangle) return Positive with
13 Post => Perimeter'Result = 2 * (Get_Height (X) + Get_Width (X));
14
15 function Area (X : Rectangle) return Positive with
16 Post => Area'Result = Get_Height (X) * Get_Width (X);
17
18 function Is_Square (X : Rectangle) return Boolean with
19 Post => Is_Square'Result = (Get_Height (X) = Get_Width (X));
20
21 function "=" (X, Y : Rectangle) return Boolean with
22 Post => "="'Result =
23 (Get_Height (X) = Get_Height (Y) and Get_Width (X) = Get_Width (Y));
24private
25 pragma Annotate (GNATprove, Hide_Info, "Private_Part", Geometry);
26
27 subtype Small_Positive is Positive range 1 .. 100;
28
29 type Rectangle_Base is record
30 Height : Small_Positive;
31 Width : Small_Positive;
32 end record with Predicate => Width <= Height;
33
34 function My_Eq (X, Y : Rectangle_Base) return Boolean renames "=";
35 -- Introduce another name to refer to the predefined equality
36
37 type Rectangle is new Rectangle_Base;
38
39 function Get_Height (X : Rectangle) return Positive is (X.Height);
40
41 function Get_Width (X : Rectangle) return Positive is (X.Width);
42
43 function Perimeter (X : Rectangle) return Positive is
44 (2 * (X.Height + X.Width));
45
46 function Area (X : Rectangle) return Positive is
47 (X.Height * X.Width);
48
49 function Is_Square (X : Rectangle) return Boolean is
50 (X.Height = X.Width);
51
52 function "=" (X, Y : Rectangle) return Boolean renames My_Eq;
53 -- "=" really is the predefined equality on rectangle
54end Geometry;
1use_geometry.adb:5:03: info: data dependencies proved
2use_geometry.adb:8:19: info: assertion proved
3use_geometry.adb:10:07: info: assertion proved
Note
Private types declared in packages with hidden private parts should be
annotated with Ownership and Predefined_Equality annotations if
their full view is subject to ownership or if its predefined equality is
restricted (in particular if they have access parts). Otherwise, GNATprove
rejects the code with an error. See
Annotation for Enforcing Ownership Checking on a Private Type
and Annotation for the Predefined Equality of Private Types for more
information.
By default, refined postconditions and bodies of expression functions declared in the body of a package are not visible from outside of this package. This enforces abstraction and prevents the proof context from growing too much, in particular with generic instantiations. However, it can be the case that the information hidden in the body of a nested package is in fact necessary to prove its enclosing unit. In particular, it happens when all entities introduced for the specification of a library are grouped together in a ghost nested package:
package My_Lib is
type T is private;
package Formal_Model with Ghost is
type Model_T is ...;
function Model (X : T) return Model_T;
end Formal_Model;
...
end My_Lib;
It is possible to disclose the content of the body of a nested package using
an Unhide_Info annotation. In this case, the body of expression functions
and potential refined postconditions specified in this body are visible as if
they were declared directly in the enclosing unit.
package body My_Lib is
package body Formal_Model with
Annotate => (GNATprove, Unhide_Info, "Package_Body")
is
function Model (X : T) return Model_T is (...);
end Formal_Model;
...
end My_Lib;
Pruning the Proof Context on a Case by Case Basis
While, in general, having information about all used entities is desirable, it might result in untractable proof contexts on large programs. It is possible to use an annotation to manually add or remove information from the proof context. For the time being, only bodies of expression functions can be handled in this way.
Information hiding is decided at the level of an entity for which checks are
generated, namely, a subprogram or entry, or the elaboration of a package. It
cannot be refined in a smaller scope. To state that the body of an expression
function should be hidden when verifying an entity E, a pragma with the
Hide_Info annotation should be used either at the begining of the body of
E or just after its specification or body. In the following example, the
body of the expression function F is hidden when verifying its callers,
making it impossible to prove their postconditions:
function F (X, Y : Boolean) return Boolean is (X and Y);
function Call_F (X, Y : Boolean) return Boolean is
(F (X, Y))
with Post => Call_F'Result = (X and Y); -- Unprovable, F is hidden
pragma Annotate (GNATprove, Hide_Info, "Expression_Function_Body", F);
function Call_F_2 (X, Y : Boolean) return Boolean with
Post => Call_F_2'Result = (X and Y); -- Unprovable, F is hidden
function Call_F_2 (X, Y : Boolean) return Boolean is
begin
return F (X, Y);
end Call_F_2;
pragma Annotate (GNATprove, Hide_Info, "Expression_Function_Body", F);
function Call_F_3 (X, Y : Boolean) return Boolean with
Post => Call_F_3'Result = (X and Y); -- Unprovable, F is hidden
function Call_F_3 (X, Y : Boolean) return Boolean is
pragma Annotate (GNATprove, Hide_Info, "Expression_Function_Body", F);
begin
return F (X, Y);
end Call_F_3;
It is also possible to hide information by default and then use an annotation to
disclose it when needed. A Hide_Info annotation located on the entity which
is hidden is considered to provide a default. For example, the body of the
expression function G is hidden by default. The postcondition of its caller
Call_G cannot be proved.
function G (X, Y : Boolean) return Boolean is (X and Y) with
Annotate => (GNATprove, Hide_Info, "Expression_Function_Body");
-- G is hidden by default
function Call_G (X, Y : Boolean) return Boolean is
(G (X, Y))
with Post => Call_G'Result = (X and Y); -- Unprovable, G is hidden
When information is hidden by default, it is possible to disclose it while
verifying an entity using the Unhide_Info annotation. This allows proving
the Call_G_2 function below:
function Call_G_2 (X, Y : Boolean) return Boolean is
(G (X, Y))
with Post => Call_G_2'Result = (X and Y); -- Provable, G is no longer hidden
pragma Annotate (GNATprove, Unhide_Info, "Expression_Function_Body", G);
Remark that, when information is hidden by default, it is even hidden during
the verification of the entity whose information we are hiding. For example,
when verifying a recursive expression function whose body is hidden by default,
the body of recursive calls is not available. If necessary, it can be disclosed
using an Unhide_Info annotation:
-- Rec_F is hidden for its recursive calls
function Rec_F (X, Y : Boolean) return Boolean is
(if not X then False elsif X = Y then True else Rec_F (Y, X))
with
Subprogram_Variant => (Decreases => X),
Post => (if X then Rec_F'Result = Y), -- Unprovable, Rec_F is hidden
Annotate => (GNATprove, Hide_Info, "Expression_Function_Body");
-- The second annotation overrides the default for recursive calls
function Rec_F_2 (X, Y : Boolean) return Boolean is
(if not X then False elsif X = Y then True else Rec_F_2 (Y, X))
with
Subprogram_Variant => (Decreases => X),
Post => (if X then Rec_F_2'Result = Y), -- Provable, Rec_F_2 is visible
Annotate => (GNATprove, Hide_Info, "Expression_Function_Body");
pragma Annotate (GNATprove, Unhide_Info, "Expression_Function_Body", Rec_F_2);
Annotation for Handling Specially Higher Order Functions
Functions for higher order programming can be expressed using parameters of an
anonymous access-to-function type. As an example, here is a function Map
returning a new array whose elements are the result of the application a
function F to the elements of its input array parameter:
function Map
(A : Nat_Array;
F : not null access function (N : Natural) return Natural)
return Nat_Array
with
Post => Map'Result'First = A'First and Map'Result'Last = A'Last
and (for all I in A'Range => Map'Result (I) = F (A (I)));
In a functional programming style, these functions are often called with an
access to a local function as a parameter. Unfortunately, as GNATprove
generally handles access-to-subprograms using refinement semantics, it is not
possible to use a function accessing global data as an actual for an anonymous
access-to-function parameter (see Subprogram Pointers). To workaround
this limitation, it is possible to annotate the function Map with
a pragma or aspect Annotate => (GNATprove, Higher_Order_Specialization).
When such a function is called on a reference to the Access attribute
of a function, it will benefit from a partial exemption from the checks
usually performed on the creation of such an access. Namely, the function will
be allowed to access data, and it might even have a precondition if it can
be proved to always hold at the point of call. We say that such a call is
specialized for a particular value of its access-to-function parameter.
As an example, consider the function Divide_All defined below. As the
function Map is annotated with Higher_Order_Specialization, it can be
called on the function Divide, even though it accesses some global data
(the parameter N) and has a precondition.
function Map
(A : Nat_Array;
F : not null access function (N : Natural) return Natural)
return Nat_Array
with
Annotate => (GNATprove, Higher_Order_Specialization),
Post => Map'Result'First = A'First and Map'Result'Last = A'Last
and (for all I in A'Range => Map'Result (I) = F (A (I)));
function Divide_All (A : Nat_Array; N : Natural) return Nat_Array with
Pre => N /= 0,
Post => (for all I in A'Range => Divide_All'Result (I) = A (I) / N);
function Divide_All (A : Nat_Array; N : Natural) return Nat_Array is
function Divide (E : Natural) return Natural is
(E / N)
with Pre => N /= 0;
begin
return Map (A, Divide'Access);
end Divide_All;
Note
It might not be possible to annotate a function with
Higher_Order_Specialization if the access value of its parameter
is used in the contract of the function, as opposed to only its dereference.
This happens in particular if the parameter is used in a call to a function
which does not have the Higher_Order_Specialization annotation.
Because the analysis done by GNATprove stays modular, the
precondition of the referenced function has to be provable on all possible
parameters (but the specialized access-to-function parameters)
and not only on the ones on which it is actually called. For
example, even if we know that the precondition of Add holds for all the
elements of the input array A, there will still be a failed check on the
call to Map in Add_All defined below. Indeed, GNATprove does not
peek into the body of Map and therefore has no way to know that its
parameter F is only called on elements of A.
function Add_All (A : Nat_Array; N : Natural) return Nat_Array with
Pre => (for all E of A => E <= Natural'Last - N),
Post => (for all I in A'Range => Add_All'Result (I) = A (I) + N);
function Add_All (A : Nat_Array; N : Natural) return Nat_Array is
function Add (E : Natural) return Natural is
(E + N)
with Pre => E <= Natural'Last - N;
begin
return Map (A, Add'Access);
end Add_All;
To avoid this kind of issue, it is possible to write a function with no
preconditions and a fallback value as done below. Remark that this does not
prevent the tool from proving the postcondition of Add_All.
function Add_All (A : Nat_Array; N : Natural) return Nat_Array is
function Add (E : Natural) return Natural is
(if E <= Natural'Last - N then E + N else 0);
begin
return Map (A, Add'Access);
end Add_All;
Note
Only the regular contract of functions is available on specialized calls. Bodies of expression functions and refined postconditions will be ignored.
The Higher_Order_Specialization annotation can also be supplied on a lemma
procedure (see Manual Proof Using User Lemmas). If this procedure
has an Automatic_Instantiation annotation
(see Annotation for Instantiating Lemma Procedures Automatically) and its associated
function also has an Higher_Order_Specialization annotation, the lemma
will generally be instantiated automatically on specialized calls to the
function. As an example, the function Count defined below returns the number
of elements with a property in an array. The function Count is specified in
a recursive way in its postcondition. The two lemmas Lemma_Count_All and
Lemma_Count_None give the value of Count when all the elements of A
or no elements of A fulfill the property. They will be automatically
instantiated on all specializations of Count.
function Count
(A : Nat_Array;
F : not null access function (N : Natural) return Boolean)
return Natural
with
Annotate => (GNATprove, Higher_Order_Specialization),
Subprogram_Variant => (Decreases => A'Length),
Post =>
(if A'Length = 0 then Count'Result = 0
else Count'Result =
(if F (A (A'Last)) then 1 else 0) +
Count (A (A'First .. A'Last - 1), F))
and Count'Result <= A'Length;
procedure Lemma_Count_All
(A : Nat_Array;
F : not null access function (N : Natural) return Boolean)
with
Ghost,
Annotate => (GNATprove, Automatic_Instantiation),
Annotate => (GNATprove, Higher_Order_Specialization),
Pre => (for all E of A => F (E)),
Post => Count (A, F) = A'Length;
procedure Lemma_Count_None
(A : Nat_Array;
F : not null access function (N : Natural) return Boolean)
with
Ghost,
Annotate => (GNATprove, Automatic_Instantiation),
Annotate => (GNATprove, Higher_Order_Specialization),
Pre => (for all E of A => not F (E)),
Post => Count (A, F) = 0;
Note
It can happen that some lemmas cannot be specialized with their associated function. It is the case in particular if the lemma contains several calls to the function with different access-to-function parameters. In this case, a warning will be emitted on the lemma declaration.
Annotation for Handlers
Some programs define handlers, subprograms which might be called
asynchronously to perform specific treatments, for example when an interrupt
occurs. These handlers are often registered using access-to-subprogram
types. In general, access-to-subprograms are not allowed to access or modify
global data in SPARK. However, this is too constraining for handlers which
tend to work by side-effects. To alleviate this limitation, it is
possible to annotate an access-to-subprogram type with a pragma or aspect
Annotate => (GNATprove, Handler). This instructs GNATprove that these
access-to-subprograms will be called asynchronously. It is possible to
create a value of such a type using a reference to the Access attribute
on a subprogram accessing or modifying global data, but only when this global
data is synchronized (see SPARK RM 9.1). However, GNATprove will make sure
that the subprograms designated by objects of these types are never called from
SPARK code, as it could result in a missing data dependency.
For example, consider the following procedure which resets to zero a global
variable Counter:
Counter : Natural := 0 with Atomic;
procedure Reset is
begin
Counter := 0;
end Reset;
It is not possible to store an access to Reset in a regular
access-to-procedure type, as it has a global effect. However, it can be stored
in a type annotated with an aspect Annotate => (GNATprove, Handler) like
below:
type No_Param_Proc is access procedure with
Annotate => (GNATprove, Handler);
P : No_Param_Proc := Reset'Access;
However, it is not possible to call P from SPARK code as the effect to
the Counter variable would be missed.
Note
As handlers are called asynchronously, GNATprove does not allow providing pre and postconditions for the access-to-subprogram type. As a result, a check will be emitted to ensure that the precondition of each specific subprogram designated by these handlers is provable in the empty context.
Annotation for Container Aggregates
The Container_Aggregates annotation allows specifying aggregates on types
annotated with the Aspect Aggregate either
directly, using predefined aggregate patterns, or through a model. The second
option is the easiest. It is enough to provide a model function returning a type
which supports compatible aggregates. When an aggregate is encountered,
GNATprove deduces the value of its model using the Container_Aggregates
annotation on the model type. In particular, functional containers from the
SPARK Libraries are annotated with the Aggregate aspect. Other
container libraries can take advantage of this support to specify aggregates on
their own library by providing a model function returning a functional
container. As an example, sequences can be used as a model to provide aggregates
for a linked list of integers:
1with SPARK.Containers.Functional.Infinite_Sequences;
2
3package Through_Model with SPARK_Mode is
4 package My_Seqs is new SPARK.Containers.Functional.Infinite_Sequences (Integer);
5 use My_Seqs;
6
7 type List is private with
8 Aggregate => (Empty => Empty_List, Add_Unnamed => Add),
9 Annotate => (GNATprove, Container_Aggregates, "From_Model");
10
11 function Empty_List return List;
12
13 function Model (L : List) return Sequence with
14 Subprogram_Variant => (Structural => L),
15 Annotate => (GNATprove, Container_Aggregates, "Model");
16
17 procedure Add (L : in out List; E : Integer) with
18 Always_Terminates,
19 Post => Model (L) = Add (Model (L)'Old, E);
20
21private
22
23 type List_Cell;
24 type List is access List_Cell;
25 type List_Cell is record
26 Data : Integer;
27 Next : List;
28 end record;
29
30 function Model (L : List) return Sequence is
31 (if L = null then Empty_Sequence
32 else Add (Model (L.Next), L.Data));
33
34 function Empty_List return List is (null);
35end Through_Model;
The Container_Aggregates annotation on type List indicates that its
aggregates are specified using a model function. The annotation on the Model
function identifies it as the function that should be used to model aggregates
of type List. It is then possible to use aggregates of type List in
SPARK as in the Main procedure below. GNATprove will use the handling of
aggregates on infinite sequences to determine the value of the model of the
aggregate and use it to prove the program.
1with Through_Model; use Through_Model;
2
3procedure Main with SPARK_Mode is
4 L : constant List := [1, 2, 3, 4, 5, 6];
5begin
6 pragma Assert (My_Seqs.Get (Model (L), 4) = 4);
7end Main;
It is also possible to specify directly how aggregates should be handled,
without going through a model. To do this, GNATprove provides three different
predefined patterns: one for vectors and sequences, one for sets,
and one for maps. The chosen pattern is specified inside the
Container_Aggregates annotation on the type. Depending on this pattern,
different functions can be provided to describe it. As an example, aggregates
on our linked list of integers can also be described directly by supplying the
three functions required for predefined sequence aggregates - First,
Last, and Get:
1with SPARK.Big_Integers; use SPARK.Big_Integers;
2with SPARK.Big_Intervals; use SPARK.Big_Intervals;
3
4package Predefined with SPARK_Mode is
5 pragma Unevaluated_Use_Of_Old (Allow);
6 type List is private with
7 Aggregate => (Empty => Empty_List, Add_Unnamed => Add),
8 Annotate => (GNATprove, Container_Aggregates, "Predefined_Sequences");
9
10 function Empty_List return List;
11
12 function First return Big_Positive is (1) with
13 Annotate => (GNATprove, Container_Aggregates, "First");
14
15 function Length (L : List) return Big_Natural with
16 Subprogram_Variant => (Structural => L),
17 Annotate => (GNATprove, Container_Aggregates, "Last");
18
19 function Get (L : List; P : Big_Positive) return Integer with
20 Pre => P <= Length (L),
21 Subprogram_Variant => (Structural => L),
22 Annotate => (GNATprove, Container_Aggregates, "Get");
23
24 function Eq (L1, L2 : List) return Boolean is
25 (Length (L1) = Length (L2)
26 and then
27 (for all I in Interval'(1, Length (L1)) =>
28 Get (L1, I) = Get (L2, I)));
29
30 function Copy (L : List) return List with
31 Subprogram_Variant => (Structural => L),
32 Post => Eq (L, Copy'Result);
33
34 procedure Add (L : in out List; E : Integer) with
35 Always_Terminates,
36 Post => Length (L) = Length (L)'Old + 1
37 and then Get (L, Length (L)) = E
38 and then (for all I in Interval'(1, Length (L) - 1) =>
39 Get (L, I) = Get (Copy (L)'Old, I));
40
41private
42 type List_Cell;
43 type List is access List_Cell;
44 type List_Cell is record
45 Data : Integer;
46 Next : List;
47 end record;
48
49 function Length (L : List) return Big_Natural is
50 (if L = null then 0 else 1 + Length (L.Next));
51
52 function Get (L : List; P : Big_Positive) return Integer is
53 (if P = Length (L) then L.Data else Get (L.Next, P));
54
55 function Empty_List return List is (null);
56end Predefined;
For all types annotated with Container_Aggregates, GNATprove performs
consistency checks to make sure that the description induced by the annotation
is compatible with the subprograms supplied by its Aggregate aspect. For
example, on the List type defined above, GNATprove generates checks to
ensure that Length returns First - 1 on Empty_List. It also checks
that calling Add increases the result of Length by one and that its
parameter E is associated to this last position. These checks succeed on
our example thanks to the postcondition of Add as made explicit by the
info messages on line 8:
predefined.ads:8:06: info: Container_Aggregates annotation proved
when establishing invariant on Length at predefined.ads:15
after a call to Empty_List at predefined.ads:10
predefined.ads:8:06: info: Container_Aggregates annotation proved
when reestablishing invariant on Get at predefined.ads:19
after a call to Add at predefined.ads:34
predefined.ads:8:06: info: Container_Aggregates annotation proved
when reestablishing invariant on Length at predefined.ads:15
after a call to Add at predefined.ads:34
The Container_Aggregates annotation might also induce
restrictions on aggregate usage. For example, if we had chosen a signed
integer type for the return type of Length in Predefined,
GNATprove would have introduced checks on all aggregates of type List to
make sure that the number of elements doesn’t exceed the number of indexes.
When a model is used to specify aggregates, both the restrictions on
aggregate usage and the consistency checks of the model are inherited. For
example, GNATprove attempts to prove the consistency of Empty_List
and Add from Through_Model with the functions supplied for the model.
These checks are proved thanks to the precise postcondition on Add.
In the same way, if we had chosen to use a functional vector indexed by a signed
integer type instead of an infinite sequence as a model in Through_Model,
we would have been limited by the size of the integer type for our aggregates.
All types with a Container_Aggregates annotation can be supplied an
additional Capacity function. In general, this function does not have any
parameters. It provides a constant bound on the number of elements allowed in
the container. If a Capacity function is supplied on a type using models for
its aggregates, it overrides the Capacity function of the model if any.
If present, the Capacity function is used both as an additional restriction
on aggregate usage and as an additional assumption for the consistency checks:
GNATprove assumes that the container holds strictly less than Capacity
elements before a call to Add and it makes sure that the number of elements
in actual aggregates never exceeds the capacity.
To accomodate containers which can have a different capacity depending on the
object, Ada allows providing an Empty function which takes an integer value
for the capacity as a parameter in the Aggregate aspect. If a Capacity
function is specified for such a type, it shall take the container as a
parameter since the capacity is specific to each container. In this case, it is
the upper bound of the parameter type of the Empty function which is used
as a restriction on aggregate usage. Examples of containers with
a capacity function (both with and without parameters) can be found in formal
container packages in the SPARK Libraries.
There are three kinds of predefined aggregates patterns:
Predefined_Sequences like in the Predefined package,
Predefined_Sets, and Predefined_Maps. The selected pattern should be
provided as a string to the Container_Aggregates annotation specified on the
container type. Additional Container_Aggregates annotations are necessary on
each specific function supported by the pattern. They also require a string
encoding its intended use. This usage is examplified in
the Predefined package.
The Predefined_Sequences pattern can be applied to containers with
positional aggregates. It supports three kinds of function annotations:
The function
Firstreturns the index or position that should be used for the first element in a container.The function
Lastreturns the index or position of the last element in a specific container.The function
Getreturns the element associated to a valid index or position in the container.
All three functions are mandatory. The return types of First and Last
should be subtypes of the same signed integer type, or possibly of
Big_Integer.
The consistency checks ensure that:
Emptyreturns a containerCsuch thatLast (C) = First - 1,Addcan be called on a containerCsuch thatLast (C) < Index_Type'Last, andafter a call to
Add, the result ofLast (C)has been incremented by one, the result of callingGeton all previous indexes is unchanged, and callingGeton the last index returns the added element.
The contracts of Empty and Append below ensure conformance to
these consistency checks:
type T is private with
Aggregate => (Empty => Empty,
Add_Unnamed => Append),
Annotate => (GNATprove, Container_Aggregates, "Predefined_Sequences");
function Empty return T with
Post => Last (Empty'Result) = First - 1;
procedure Append (X : in out T; E : Element_Type) with
Always_Terminates,
Pre => Last (X) < Index_Type'Last,
Post => Last (X) = Last (X)'Old + 1 and Get (X, Last (X)) = E
and (for all I in First .. Last (X) - 1 => Get (X, I) = Get (X'Old, I));
function Last (X : T) return Ext_Index with
Annotate => (GNATprove, Container_Aggregates, "Last");
function First return Index_Type with
Annotate => (GNATprove, Container_Aggregates, "First");
function Get (X : T; I : Index_Type) return Element_Type with
Annotate => (GNATprove, Container_Aggregates, "Get"),
Pre => I <= Last (X);
If Last returns a signed integer type, there is a restriction on predefined
sequence aggregates usage: GNATprove will make sure that the number of
elements in an aggregate never exceeds the maximum value of the return type of
Last.
When an aggregate C is encountered, GNATprove automatically infers that:
Last (C) - First + 1is the number of elements in the aggregate andGet (First + N - 1)returns a copy of the N’th element.
The Predefined_Sets pattern can be applied to containers with
positional aggregates. It supports three kinds of function annotations:
The
Containsfunction returns True if and only if its element parameter is in the container.Equivalent_Elementsis an equivalence relation such thatContainsalways returns the same value on two equivalent elements.The
Lengthfunction returns the number of elements in the set.
Contains and Equivalent_Elements are mandatory, Length is optional.
If it is supplied, the Length function should return a signed
integer type or a subtype of Big_Integer.
The consistency checks ensure that:
Containsreturns False for all elements on the result ofEmptyandLength, if specified, returns 0,Addcan be called on a containerCand an elementEsuch thatContains (C, E)returns False,after a call to
Addon a containerCand an elementE,Containsreturns True onEand on all elements which were inCbefore the call, plus potential additional elements equivalent toE,after a call to
Add, the result of theLengthfunction if any is incremented by one.
The contracts of Empty and Insert below ensure conformance to
these consistency checks:
type T is private with
Aggregate => (Empty => Empty,
Add_Unnamed => Insert),
Annotate => (GNATprove, Container_Aggregates, "Predefined_Sets");
function Empty return T with
Post => Length (Empty'Result) = 0
and then (for all E in Element_Type => not Contains (Empty'Result, E));
procedure Insert (X : in out T; E : Element_Type) with
Always_Terminates,
Pre => not Contains (X, E),
Post => Length (X) = Length (X'Old) + 1 and Contains (X, E)
and (for all F in Element_Type =>
(if Contains (X'Old, F) then Contains (X, F)))
and (for all F in Element_Type =>
(if Contains (X, F) then Contains (X'Old, F) or Eq_Elem (F, E)));
function Eq_Elem (X, Y : Element_Type) return Boolean with
Annotate => (GNATprove, Container_Aggregates, "Equivalent_Elements");
function Contains (X : T; E : Element_Type) return Boolean with
Annotate => (GNATprove, Container_Aggregates, "Contains");
function Length (X : T) return Natural with
Annotate => (GNATprove, Container_Aggregates, "Length");
Aggregates of types annotated with Predefined_Sets cannot contain
duplicates, that is, two elements on which Equivalent_Elements returns
True. This restriction on aggregate usage is enforced by GNATprove. It
allows the tool to properly assess the cardinality of the resulting set. If
a Length function is supplied and returns a signed integer type, and no
Capacity function applies to the type, GNATprove also makes sure that the
number of elements in the aggregate does not exceed the upper bound of the
return type of Length. This last check is replaced by a check on the
capacity if there is one.
When an aggregate C is encountered, GNATprove automatically infers that:
Contains (C, E)returns True for every elementEof the aggregate,Contains (C, E)returns False for every elementEwhich is not equivalent to any element in the aggregate, andLength (C), if supplied, is the number of elements in the aggregate.
The Predefined_Maps pattern can be applied to containers with
named aggregates. It supports five kinds of function annotations:
The
Default_Itemfunction returns the element associated by default to keys of total maps.The
Has_Keyfunction returns True if and only if its key parameter has an association in a partial map.The
Getfunction returns the element associated to a key in the container.Equivalent_Keysis an equivalence relation such thatHas_KeyandGetreturn the same value on two equivalent keys.The
Lengthfunction returns the number of associations in a partial map.
Get and Equivalent_Keys are mandatory, exactly one of Default_Item
and Has_Key should be supplied (depending on whether the map is total - it
associates a value to all keys - or partial) , and Length is optional and
can only be supplied for partial maps. If it is supplied, the Length
function should return a signed integer type or a subtype of Big_Integer.
The consistency checks ensure that:
if
Default_Itemis supplied,GetreturnsDefault_Itemfor all keys on the result ofEmpty,if
Has_Keyis supplied, it returns False for all keys on the result ofEmpty, andLength, if specified, returns 0,Addcan be called on a containerCand a keyKsuch thatHas_Key (C, K)returns False (for patial maps) orGet (C, K) = Default_Item(for total maps),after a call to
Addon a containerC, a keyK, and an elementE,Has_Key, if any, returns True onKand on all keys which were inCbefore the call, plus potential additional keys equivalent toK,after a call to
Addon a containerC, a keyK, and an elementE,Getreturns a copy ofEonKand its association inCbefore the call on keys which are not equivalent toK, andafter a call to
Add, the result of theLengthfunction if any is incremented by one.
The contracts of Empty and Insert below ensure conformance to
these consistency checks for total maps:
type T is private with
Aggregate => (Empty => Empty,
Add_Named => Insert),
Annotate => (GNATprove, Container_Aggregates, "Predefined_Maps");
function Empty return T with
Post => (for all K in Key_Type => Get (Empty'Result, K) = Default_Value);
procedure Insert (X : in out T; K : Key_Type; E : Element_Type) with
Always_Terminates,
Pre => Get (X, K) = Default_Value,
Post => Get (X, K) = E
and (for all F in Key_Type =>
(if not Eq_Key (F, K) then Get (X, F) = Get (X'Old, F)));
function Eq_Key (X, Y : Key_Type) return Boolean with
Annotate => (GNATprove, Container_Aggregates, "Equivalent_Keys");
function Default_Value return Element_Type with
Annotate => (GNATprove, Container_Aggregates, "Default_Item");
function Get (X : T; K : Key_Type) return Element_Type with
Annotate => (GNATprove, Container_Aggregates, "Get";
And here is a version for partial maps:
type T is private with
Aggregate => (Empty => Empty,
Add_Named => Insert),
Annotate => (GNATprove, Container_Aggregates, "Predefined_Maps");
function Empty return T with
Post => Length (Empty'Result) = 0
and (for all K in Key_Type => not Has_Key (Empty'Result, K));
procedure Insert (X : in out T; K : Key_Type; E : Element_Type) with
Always_Terminates,
Pre => not Has_Key (X, K),
Post => Length (X) - 1 = Length (X)'Old
and Has_Key (X, K)
and (for all F in Key_Type =>
(if Has_Key (X'Old, F) then Has_Key (X, F)))
and (for all L in Key_Type =>
(if Has_Key (X, L) then Has_Key (X'Old, L) or Eq_Key (L, K)))
and Get (X, K) = E
and (for all F in Key_Type =>
(if Has_Key (X'Old, F) then Get (X, F) = Get (X'Old, F)));
function Eq_Key (X, Y : Key_Type) return Boolean with
Annotate => (GNATprove, Container_Aggregates, "Equivalent_Keys");
function Has_Key (X : T; K : Key_Type) return Boolean with
Annotate => (GNATprove, Container_Aggregates, "Has_Key");
function Get (X : T; K : Key_Type) return Element_Type with
Pre => Has_Key (X, K),
Annotate => (GNATprove, Container_Aggregates, "Get");
function Length (X : T) return Natural with
Annotate => (GNATprove, Container_Aggregates, "Length");
Aggregates of types annotated with Predefined_Maps cannot contain
duplicates, that is, two keys on which Equivalent_Keys returns
True. This restriction on aggregate usage is enforced by GNATprove. It
allows the tool to determine the associated element uniquely and to assess the
cardinality of the resulting map. If a Length function is supplied and
returns a signed integer type, and no Capacity function applies to the type,
GNATprove also makes sure that the number of elements in the aggregate does
not exceed the upper bound of the return type of Length. This last check is
replaced by a check on the capacity if there is one.
When an aggregate C is encountered, GNATprove automatically infers that:
if
Has_Keyis supplied,Has_Key (C, K)returns True for every associationK => _in the aggregate,Get (C, K)returns a copy ofEfor every associationK => Ein the aggregate,for every key
Kwhich is not equivalent to any key in the aggregate eitherHas_Key (C, K)returns False (for patial maps) orGet (C, K)returnsDefault_Item(for total maps), andLength (C), if supplied, is the number of elements in the aggregate.
Annotation for Mutable IN Parameters
In SPARK, parameters of mode in - and every object they designate,
see Memory Ownership Policy - are considered to be preserved by
subprogram calls unless the parameters are of an access-to-variable type. Ada,
however, does not enforce the same restriction. In particular, if a parameter of
mode in is of a private type which is ultimately an access-to-variable type,
then the subprogram might modify the value it designates. The
Mutable_In_Parameter annotation is designed to make it possible to interact
with existing Ada libraries from SPARK code, even if the libraries are not
abiding by the language restrictions. It allows annotating an entry, procedure,
or function with side effects so that all its parameters of mode in of
a given type are considered to be potentially modified by the subprogram. This
is only supported for parameters of a private type whose ultimate full view is
either not visible from SPARK or an access-to-variable type.
As an example, consider an Ada library for strings with the following signature:
package My_Unbounded_Strings is
type My_String is private;
Null_String : constant My_String;
function Get (S : My_String) return String with
Pre => S /= Null_String;
procedure Update
(S : My_String;
Index : Positive;
Char : Character)
with Pre =>
S /= Null_String and then Index in Get (S)'Range;
private
type My_String is access String;
Null_String : constant My_String := null;
end My_Unbounded_Strings;
To be able to designate strings of any size, the type My_String is in fact
a pointer to an Ada string that can be retrieved through the Get function.
The Update procedure writes a character Char at position Index
in the value designated by S. Since the value of the pointer S is not
modified by Update, Ada allows it to be a parameter of mode in. However,
this procedure is not compatible with SPARK, as it modifies the value
designated by Item which is considered to be part of Item as per the
Memory Ownership Policy. To make it possible to use this procedure from
SPARK code, a pragma Annotate is supplied directly after Update:
pragma Annotate (GNATprove, Mutable_In_Parameters, My_String);
Thanks to this annotation, GNATprove considers that a call to Update can
modify its parameter Item, even if it has mode in.
Note
This pragma Annotate does not designate a parameter by name but the
parameter type (because the scope of the parameter entity is limited to the
declaration of the enclosing subprogram). It can happen that the same type
is used for more than one parameter of mode in in the subprogram. If it
is the case, all such parameters will be considered to be potentially mutated
by the call. If some are in fact preserved, it will need to be stated as a
postcondition of the subprogram.