Automatic Generation of Frame Conditions for Record Components
by Claire Dross –
As explained in a previous post, formal verification tools like GNATprove rely on the user to provide loop invariants to describe the actions performed inside loops.
Though the preservation of variables which are not modified in the loop need not be mentioned in the invariant, it is in general necessary to state explicitly the preservation of unmodified object parts, such as record fields or array elements. These preservation properties form the loop’s frame condition. As it may seem obvious to the user, the frame condition is unfortunately often forgotten when writing a loop invariant, leading to unprovable checks.
To alleviate this problem, the GNATprove tool now generates automatically frame conditions for unmodified fields of record variables. It also handles unmodified fields of array components as long as they are preserved at every index in the array.
Let us look what it means on an example. We consider a structure which is an array containing for each element its value, the maximum of the values of the previous elements in the array and the maximum of the values of the next elements in the array:
type Cell is record
Value : Natural;
Max_Left : Natural;
Max_Right : Natural;
end record;
type Cell_Array is array (Positive range <>) of Cell;We create a function which updates the fields Max_Left and Max_Right of each element of an array A with the appropriate values. The postcondition of the procedure states that the Max_Left (resp. Max_Right) component of each cell is bigger than the elements located before (resp. after) the cell.
procedure Update_Max (A : in out Cell_Array) with
Post => (for all I in A'Range =>
A (I).Value = A'Old (I).Value
and (for all J in I .. A'Last =>
A (I).Value <= A (J).Max_Left
and A (J).Value <= A (I).Max_Right));We implement Update_Max using two loops. The first one goes from left to right and only updates the Max_Left field of each array cell while the second one goes from right to left and only updates the Max_Right field.
procedure Update_Max (A : in out Cell_Array)is
K : Positive;
Max : Natural;
begin
-- If A is empty, there is nothing to do.
if A'Length = 0 then
return;
end if;
-- Loop from A'First to A'Last. Max is the maximum of the
-- elements encountered so far. At each step, update the
-- Max_Left field of the current index with the current value
-- of Max.
K := A'First;
Max := 0;
loop
if A (K).Value > Max then
Max := A (K).Value;
end if;
A (K).Max_Left := Max;
exit when K = A'Last;
K := K + 1;
end loop;
-- Loop from A'Last to A'First. Max is the maximum of the
-- elements encountered so far. At each step, update the
-- Max_Right field of the current index with the current
-- value of Max.
K := A'Last;
Max := 0;
loop
if A (K).Value > Max then
Max := A (K).Value;
end if;
A (K).Max_Right := Max;
exit when K = A'First;
K := K - 1;
end loop;
end Update_Max;For the postcondition of Update_Max to be proved, we need to add a loop invariant to both loops stating how the loop has modified A, K, and Max during the previous iterations (see the user guide to know what should be written in loop invariants). In each loop invariant, we need only to speak about the components the array cells which we are updating:
loop
if A (K).Value > Max then
Max := A (K).Value;
end if;
A (K).Max_Left := Max;
-- K stays in A'Range
pragma Loop_Invariant (K in A'Range);
-- Max is bigger than all the elements encountered so far
pragma Loop_Invariant
(for all I in A'First .. K => A (I).Value <= Max);
-- For every indexes I <= J updated so far, Max_Left of J is bigger than the Value of I
pragma Loop_Invariant
(for all I in A'First .. K =>
(for all J in I .. K =>
A (I).Value <= A (J).Max_Left));
exit when K = A'Last;
K := K + 1;
end loop;For this loop, GNATprove infers that components Value and Max_Right of each element of A are preserved and automatically generates the corresponding frame condition:
pragma Loop_Invariant
(for all I in A'Range => A (I).Value = A'Loop_Entry (I).Value
and A (I).Max_Right = A'Loop_Entry (I).Max_Right);So that the above subprogram is completely proved by GNATprove with level=1.
Note that, as SPARK treats subprograms' inputs as a whole, the frame condition could not be generated if the modifications in the loops were done to A through a subprogram call, and the frame condition would need to be stated explicitly in the invariant:
procedure Set_Max_Left (Index : Positive; Value : Natural)
with Post => A = A'Old'Update
(Index => A'Old (Index)'Update (Max_Left => Value));
loop
if A (K).Value > Max then
Max := A (K).Value;
end if;
-- Set_Max_Left only modifies A (K).Max_Left, but frame condition generation
-- does not know it.
Set_Max_Left (K, Max);
-- Frame condition
pragma Loop_Invariant
(for all I in A'Range => A (I).Value = A'Loop_Entry (I).Value
and A (I).Max_Right = A'Loop_Entry (I).Max_Right);
[...]
exit when K = A'Last;
K := K + 1;
end loop;Also note that no frame condition is currently generated for unmodified components of an array. For example, we cannot prove at the beginning of the loop that the Max_Left component of the current array cell is equal to its value before the loop without explicitly stating its preservation as a loop invariant:
A_Init := A;
loop
-- The element stored at index K has not been modified so far,
-- but no frame condition is currently generated for that.
pragma Assert (A (K).Max_Left = A_Init (K).Max_Left);
if A (K).Value > Max then
Max := A (K).Value;
end if;
A (K).Max_Left := Max;
-- Frame condition
pragma Loop_Invariant
(for all I in A'Range =>
(if I > K then A (I).Max_Left = A'Loop_Entry (I).Max_Left));
[...]
exit when K = A'Last;
K := K + 1;
end loop;See the corresponding section in the user guide for more information.
About Claire Dross
Claire Dross has a PhD in deductive verification of programs using a satisfiability modulo theory solver with the Universite Paris-Sud. She also has an engineering degree from the Ecole Polytechnique and an engineering degree from the Ecole Nationale Superieure des Telecommunications. At AdaCore, she works full-time on the formal verification SPARK 2014 toolset.