This version was quite a bit more work , and probably can be improved upon, but it attempts to prove more functional properties one might want to apply to this problem. For example, it ensures that adding an element to the list only modifies one storage element, without modifying others, and that the number of elements in the list matches the number of used slots in the array. This version also provides a main program which is written in SPARK that uses the package.
I did have an intermediate version which I arrived at fairly easily that proved
the extra functional requirements, but when I tried to use it with a client
program written in SPARK, it led me to add to and revise what I had.
package Array_Item_Lists with SPARK_Mode is
Max_Item : constant := 3; -- Set to whatever limit is desired
subtype Element_Count is Natural range 0 .. Max_Item;
subtype Element_Index is Natural range 1 .. Max_Item;
type Integer_List is private;
function Create return Integer_List
with Post => Length (Create'Result) = 0
and then Used_Count (Create'Result) = 0
and then not Is_Full (Create'Result)
and then Not_Full (Create'Result)
and then (for all I in 1 .. Max_Item =>
not Has_Element (Create'Result, I));
function Length (List : Integer_List) return Element_Count;
function Used_Count (List : Integer_List) return Element_Count;
-- Is_Full is based on Length being = Max_Item
function Is_Full (List : Integer_List) return Boolean;
-- Not_Full is based on there being empty slots in the list available
-- Since the length is kept in sync with number of used slots, the
-- negation of one result should be equivalent to the result of the other
function Not_Full (List : Integer_List) return Boolean;
function Next_Index (List : Integer_List) return Element_Index
with Pre => Used_Count (List) = Length (List)
and then Length (List) < Max_Item and then Not_Full (List),
Post => not Has_Element (List, Next_Index'Result);
function Element (List : Integer_List;
Index : Element_Index) return Integer;
function Has_Element (List : Integer_List;
Index : Element_Index) return Boolean;
procedure Append_Item (List : in out Integer_List;
Value : Integer;
Success : out Boolean)
with
Pre => Used_Count (List) = Length (List)
and then (if Length (List) < Max_Item
then Not_Full (List) and then
not Has_Element (List, Next_Index (List))
else Is_Full (List)),
Post =>
(if not Is_Full (List) then Not_Full (List)) and then
(if Length (List'Old) < Max_Item
then Success
and then Length (List) = Length (List'Old) + 1
and then Element (List, Next_Index (List'Old)) = Value
and then Has_Element (List, Next_Index (List'Old))
and then (for all I in 1 .. Max_Item =>
(if I /= Next_Index (List'Old) then
Element (List'Old, I) = Element (List, I)
and then
Has_Element (List'Old, I) = Has_Element (List, I)))
and then Used_Count (List) = Used_Count (List'Old) + 1
else not Success and then
Length (List) = Max_Item and then List'Old = List
and then Used_Count (List) = Max_Item);
private
type t_item is record
Used : Boolean := False;
Value : Integer := 0;
end record;
type t_item_list is
array (Element_Count range 1 .. Element_Count'Last) of t_item;
type Integer_List is
record
Items : t_item_list := (others => (Used => False, Value => 0));
Used_Items : Element_Count := 0;
end record;
function Element (List : Integer_List;
Index : Element_Index) return Integer is
(List.Items (Index).Value);
function Has_Element (List : Integer_List;
Index : Element_Index) return Boolean is
(List.Items (Index).Used);
function Length (List : Integer_List) return Element_Count is
(List.Used_Items);
function Is_Full (List : Integer_List) return Boolean is
(for all Item of List.Items => Item.Used
and then Length (List) = Max_Item);
function Not_Full (List : Integer_List) return Boolean is
(for some Item of List.Items => not Item.Used
-- Used_Count (List) < Max_Item
);
end Array_Item_Lists;
I'm not quite happy about having both an Is_Full function and a Not_Full function,
and that may be something that can be simplified. But I did manage to get this to prove, once I added some reasonable assumptions in the body below.
pragma Ada_2012;
package body Array_Item_Lists with SPARK_Mode is
procedure Append_Item (List : in out Integer_List;
Value : Integer;
Success : out Boolean)
is
Old_Used_Count : constant Element_Count := Used_Count (List);
begin
if List.Used_Items = Max_Item then
Success := False;
return;
end if;
declare
Update_Index : constant Element_Index := Next_Index (List);
begin
pragma Assert (List.Items (Update_Index).Used = False);
List.Items (Update_Index) := (Value => Value, Used => True);
List.Used_Items := List.Used_Items + 1;
Success := True;
pragma Assert (List.Items (Update_Index).Used = True);
-- We have proven that one the one element of the array
-- has been modified, and that it was previous not used,
-- and that not it is used. From this, we can now assume that
-- the use count was incremented by one
pragma Assume (Used_Count (List) = Old_Used_Count + 1);
-- If the length isn't full (Is_Full) we can assume the
-- number of used items has room also. We incremented both
-- of these above, and the two numbers are always in sync.
pragma Assume (if not Is_Full (List) then Not_Full (List));
end;
end Append_Item;
-----------------------------------------------------------------
function Create return Integer_List is
Result : Integer_List := (Items => <>,
Used_Items => 0);
begin
for I in Result.Items'Range loop
Result.Items (I) := (Used => False, Value => 0);
pragma Loop_Invariant
(for all J in 1 .. I => Result.Items (J).Used = False);
end loop;
pragma Assert (for all Item of Result.Items => Item.Used = False);
-- Since we have just proven that all items are not used, we know
-- the Used_Count has to be zero, and hence we are not full
-- so we can make the following assumptions
pragma Assume (Used_Count (Result) = 0);
pragma Assume (Not_Full (Result));
return Result;
end Create;
-----------------------------------------------------------------
function Next_Index (List : Integer_List) return Element_Index
is
Result : Element_Index := 1;
begin
Search_Loop :
for I in List.Items'Range loop
pragma Loop_Invariant
(for some J in I .. Max_Item => not List.Items (J).Used);
if not List.Items (I).Used then
Result := I;
exit Search_Loop;
end if;
end loop Search_Loop;
return Result;
end Next_Index;
function Used_Count (List : Integer_List) return Element_Count is
Count : Element_Count := 0;
begin
for Item of List.Items loop
if Item.Used then
Count := Count + 1;
end if;
end loop;
return Count;
end Used_Count;
end Array_Item_Lists;
And finally, here is a SPARK main program that makes calls to the above package
with Ada.Text_IO; use Ada.Text_IO;
with Array_Item_Lists;
procedure Main with SPARK_Mode
is
List : Array_Item_Lists.Integer_List := Array_Item_Lists.Create;
Success : Boolean;
begin
Array_Item_Lists.Append_Item (List => List,
Value => 3,
Success => Success);
pragma Assert (Success);
Array_Item_Lists.Append_Item (List => List,
Value => 4,
Success => Success);
pragma Assert (Success);
Array_Item_Lists.Append_Item (List => List,
Value => 5,
Success => Success);
pragma Assert (Success);
Array_Item_Lists.Append_Item (List => List,
Value => 6,
Success => Success);
pragma Assert (not Success);
Put_Line ("List " &
(if Array_Item_Lists.Is_Full (List)
then "is Full!" else "has room!"));
end Main;
