Download ADA USER JOURNAL - Ada

62
function First_To_Previous (Container : List;
Current : Cursor) return List;
The function Current_To_Last takes a container Cont and
a cursor Cu in argument and returns a container that is
Cont where every cursor preceding Cu in Cont have been
removed:
function Current_To_Last (Container : List;
Current : Cursor) return List;
Finally, the function Strict_Equal takes two containers
and returns true if and only if they contain the same
elements in the same order and iteration can be done on
both of them using the same cursors.
function Strict_Equal (Left, Right : List)
return Boolean;
Thanks to these function, we can complete the
specification of Increment_Element:
procedure Increment_Element (L : in out List;
Cu : Cursor) with
Pre => Has_Element (L, Cu) and then
Element (L, Cu) < Element_Type'Last,
Post => Has_Element (L, Cu) and then
Element (L, Cu) = Element (L'Old, Cu) + 1
and then
Strict_Equal (First_To_Previous (L, Cu),
First_To_Previous (L'Old, Cu))
and then
Strict_Equal (Current_To_Last (L, Next(L, Cu)),
Current_To_Last (L'Old, Next(L'Old, Cu)));
The implementation of Increment_Element is as simple as
calling procedure Replace_Element from the formal
containers' API:
procedure Increment_Element (L : in out List;
Cu : Cursor) is
begin
Replace_Element (L, Cu, Element (L, Cu) + 1);
end Increment_Element;
And guess what? GNATprove manages to prove
automatically that the implementation above indeed
implements the contract that we specified for
Increment_Element. And that no run-time errors can be
raised in this code. Not bad for a non-trivial specification!
2 Expressing Properties over Formal
Containers
We saw in the previous post how formal containers can be
used in SPARK code. In this post, I describe how to
express properties over the content of these containers,
using quantified expressions. In their simplest form,
quantified expressions in Ada 2012 can be used to express
a property over a scalar range. For example, that all
integers between 1 and 6 have a square less than 40:
(for all J in 1 .. 6 => J * J < 40)
Vo lu me 3 5 , Nu mb er 1 , March 2014
SPARK 2014 Rationale: Formal Containers
or that every even integer greater than 2 can be expressed
as the sum of two primes (also known as Goldbach's
conjecture):
(for all J in Integer =>
(if J > 2 then
(for some P in 1 .. J / 2 => Is_Prime (P) and then
Is_Prime (J - P))))
The second form of quantified expressions allows to
express a property over a standard container. For
example, that all elements of a list of integers are prime,
which can be expressed by iterating over cursors as
follows:
(for all Cu in My_List => Is_Prime (Element (Cu)))
The general mechanism in Ada 2012 that provides this
functionality relies on the use of tagged types (for the
container type) and various aspects involving access types
so cannot be applied to the SPARK formal containers.
Instead, we have defined in GNAT an aspect Iterable that
provides the same functionality in a simpler way, leading
also to much simpler object code. For example, here is
how it can be used on a type Container_Type:
type Container_Type is ... -- the structure on which we
-- want to quantify
with Iterable => (First => My_First,
Has_Element => My_Has_Element,
Next => My_Next);
where My_First is a function taking a single argument of
type Container_Type and returning a cursor:
function My_First (Cont : Container_Type)
return My_Cursor_Type;
and My_Has_Element is a function taking a container and
a cursor and returning whether this cursor has an
associated element in the container:
function My_Has_Element (Cont : Container_Type;
Pos : My_Cursor_Type) return Boolean;
and My_Next is a function taking a container and a cursor
and returning the next cursor in this container:
function My_Next (Cont : Container_Type; Pos :
My_Cursor_Type) return My_Cursor_Type;
Now, if the type of object Cont is iterable in the sense
given above, it is possible to express a property over all
elements in Cont as follows:
(for all Cu in Cont => Property (Cu))
The compiler will generate code that iterates over Cont
using the functions My_First, My_Has_Element and
My_Next given in the Iterable aspect, so that the above is
equivalent to:
declare
Cu : My_Cursor_Type := My_First (Cont);
Result : Boolean := True;
Ad a User Jo urn al