Skip to content

Latest commit

 

History

History
436 lines (351 loc) · 14.1 KB

Push_Heap.org

File metadata and controls

436 lines (351 loc) · 14.1 KB
Raw

The Push_Heap algorithm

When adding (pushing) a new value V into a heap represented by a complete binary tree, the idea is to put V at the first available place in the tree and to make V “go up” on the path to the root of the tree to find its place. The same principle will be applied on our array representation of the heap.

The Push_Heap algorithm takes a Heap with the value to be added placed at the first available index of the array and makes the value go up into the heap to match the property Is_Heap. Its signature is the following:

procedure Push_Heap (H : in out Heap)

Specification of Push_Heap

In order to specify Push_Heap, we must be able to express that the elements contained in the array up to index Size are the same up to a permutation. As the array encapsulated in the Heap record type can be viewed as a multiset of T values and such properties can be expressed on multisets, we use the predicates already defined when proving the Remove_Copy algorithm, particularly the Multiset_Unchanged predicate

The specification of Push_Heap is rather simple to express:

procedure Push_Heap (H : in out Heap) with
   Pre => H.Size in 1 .. MAX_SIZE
   and then Is_Heap_Def ((A => H.A, Size => H.Size - 1)),
   Post => Is_Heap_Def (H) and then Multiset_Unchanged (H'Old.A, H.A)
   and then
   (if H.Size < MAX_SIZE then
      H'Old.A (H.Size + 1 .. MAX_SIZE) = H.A (H.Size + 1 .. MAX_SIZE))
   and then H.Size = H'Old.Size;

The preconditions express the following assertions:

  • the heap is not full
  • the heap without its last value verifies the properties of a heap. Notice that our array representation is rather simple as we only have to consider the array up to index Size - 1 to have the heap without the last value

The postconditions express the following assertions:

  • the array up to index Size verifies the properties of a heap
  • the array in the heap after the call is just a permutation of the array in the heap before the call, i.e. the elements in the array after the call are exactly the same than the ones before the call.
  • the size of the heap has not been modified

New predicates on multisets

In order to easily express properties on heaps, particularly properties on permutations, three new multiset predicates will be defined.

The Multiset_Add and Multiset_Minus predicates

The Multiset_Add and Multiset_Minus predicates are used to check whether the number of occurrences of a given value Val has increased or decreased.

function Multiset_Add
  (A   : T_Arr;
   B   : T_Arr;
   Val : T)
   return Boolean is (Occ (B, Val) = Occ (A, Val) + 1) with
   Pre => A'Length < Positive'Last;
function Multiset_Minus
  (A   : T_Arr;
   B   : T_Arr;
   Val : T)
   return Boolean is (Occ (B, Val) = Occ (A, Val) - 1);

The precondition on Multiset_Add is used to prevent possible overflows.

Another Multiset_Retain_Rest_Double predicate

We have already defined predicates on multisets for the Remove_Copy algorithm, particularly a predicate Multiset_Retain_Rest to check whether two arrays are equal up to a permutation except for a particular value. As we will see later, we will need another form of Multiset_Retain_Rest, but this time with two excluded values. The definition of Multiset_Retain_Rest_Double is not that different from Multiset_Retain_Rest:

function Multiset_Retain_Rest_Double
  (A    : T_Arr;
   B    : T_Arr;
   Val1 : T;
   Val2 : T)
   return Boolean is
  (for all X in T =>
     (if X /= Val1 and then X /= Val2 then Occ (A, X) = Occ (B, X)));

Implementation of Push_Heap

The implementation of Push_Heap in ACSL By Example is split in three parts: the prologue, the main act and the epilogue. We follow the same architecture in our implementation in SPARK, presenting the implementation and the lemmas helping the prover to prove the parts. The main idea of the algorithm is to make the value at index Size in the array “go up” through the heap until it finds a correct place.

Prologue

Implementation of Prologue

The prologue part of the implementation is the following:

procedure Push_Heap (H : in out Heap) is
   V    : T                 := H.A (H.Size);
   Size : constant Positive := H.Size with
      Ghost;
   Hole   : Natural;
   Parent : Natural;
   A_Old  : constant T_Arr := H.A with
      Ghost;
   A_Save : T_Arr := H.A with
      Ghost;
   V_Old : T with
      Ghost;

begin

   if 1 < H.Size then

      Hole := Heap_Parent (H.Size);

      if H.A (Hole) < V then

	 -- beginning of Prologue

	 H.A (H.Size) := H.A (Hole);
	 Make_Prove_Prologue (H.A, A_Old, V, H.Size);

	 -- end of Prologue

The only variables used here are V, Hole and A_Old. V is the value at the index Size in the array, i.e. the value to be added. Hole represent the index in the heap being currently checked for heap consistency. A_Old is a ghost variable containing the state of the heap array before the call.

Let us briefly explain what happens in the prologue:

  • if the size of the heap is 1, there’s no need to do anything, so we jump directly to the en of the procedure
  • otherwise we assign Hole with the index of the parent of index Size in the array and if the value of the parent node is less than V, we store this value at index Size.

    Notice that at this point, the slice H.A (1 .. H.Size) respects the properties of a heap and that the value of the parent node of node at index Size is duplicated.

The Make_Prove_Prologue procedure

We want to prove the previous property at the end of the prologue: H.A (1 .. H.Size) is a heap, H.A (Hole) is duplicated and V has lost one occurrence in A. The Make_Prove_Prologue represents this property:

procedure Make_Prove_Prologue
  (A, A_Old : T_Arr;
   V        : T;
   Hole     : Positive) with
   Pre => A'First = A_Old'First and then A'Last = A_Old'Last
   and then Hole in A'Range and then A'Last < Positive'Last
   and then Is_Set (A_Old, Hole, A (Hole), A) and then A_Old (Hole) = V
   and then A (Hole) /= V,
   Post => Multiset_Add (A_Old, A, A (Hole))
   and then Multiset_Minus (A_Old, A, V)
   and then Multiset_Retain_Rest_Double (A_Old, A, V, A (Hole));

The postcondition of Make_Prove_Prologue correctly represents what is expected at the end of the prologue. Notice that the preconditions are valid at this state of the procedure.

As usual, we have to give an implementation of the lemma to guide the provers:

procedure Make_Prove_Prologue
  (A, A_Old : T_Arr;
   V        : T;
   Hole     : Positive)
is
begin
   for E in T loop
      Occ_Set (A_Old, A, Hole, A (Hole), E);
      pragma Loop_Invariant
	(for all F in T'First .. E =>
	   (if F = V then Occ (A, F) = Occ (A_Old, F) - 1
	    elsif F = A (Hole) then Occ (A, F) = Occ (A_Old, F) + 1
	    else Occ (A, F) = Occ (A_Old, F)));
   end loop;
end Make_Prove_Prologue;

The implementation is quite basic for this kind of lemma (we loop on T values), except for the loop invariant which is a bit different from the previous ones, because of the new predicates: we want to show that V has lost an occurrence and A (Hole) has one extra occurrence.

With this implementation and specification, GNATprove proves the lemma and the assertions at the end of the prologue, i.e.:

  • the array is now a heap (because A (1 .. Size - 1) was a heap
  • the multiset predicates are verified

Main act

Implementation of Main Act

In the main act we go up in the tree representating the heap to find the index where we can put the value V. Of course we will switch values accordingly. The implementation of the Main Act is the following:

-- beginning of Main Act

if 1 < Hole then

   Parent := Heap_Parent (Hole);

   while 1 < Hole and then H.A (Parent) < V loop

      A_Save := H.A;
      V_Old  := H.A (Hole);

      if H.A (Hole) < H.A (Parent) then
	 H.A (Hole) := H.A (Parent);

      end if;

      Make_Prove_Loop (H.A, A_Save, A_Old, V_Old, V, Hole);

      Hole := Parent;

      if (1 < Hole) then
	 Parent := Heap_Parent (Hole);
      end if;

      pragma Loop_Invariant
	(if Size < MAX_SIZE then
	   A_Old (Size + 1 .. MAX_SIZE) =
	   H.A (Size + 1 .. MAX_SIZE));
      pragma Loop_Invariant (Hole in 1 .. H.Size);
      pragma Loop_Invariant (Is_Heap_Def (H));
      pragma Loop_Invariant
	(if 1 < Hole then Parent = Heap_Parent (Hole));
      pragma Loop_Invariant (H.A (Hole) < V);
      pragma Loop_Invariant
	(Multiset_Add (A_Old, H.A, H.A (Hole)));
      pragma Loop_Invariant (Multiset_Minus (A_Old, H.A, V));
      pragma Loop_Invariant
	(Multiset_Retain_Rest_Double (A_Old, H.A, H.A (Hole), V));
   end loop;
end if;

-- end of Main Act

The actual code is not that long: we modify in the llop the position of the Hole index (we go up in the heap) to find the final index where we will insert V in the Epilogue phase of the algorithm. When going up, we exchange the value of the current node (represented by the Hole index) with the value of its parent.

In order to prove the loop, we use a A_Save array which is a copy of A at the beginning of each iteration (notice that A_Save is a ghost variable, hence does not impact the performance of the algorithm). Since we just modify one value in A at each iteration, we can use the Is_Set predicate previously defined to compare A with A_Save.

As for the Prologue, we will define a Make_Prove_Loop lemma which calculates the Multiset properties that hold between A and A_Old, considering the predicates between A and A_Save and between A_Save and A_Old. The next subsections detail Make_Prove_Loop.

The loop invariants specify the fact that:

  • Hole is in the right range.
  • H is a heap.
  • Parent is the parent of Hole if Hole > 1.
  • the multiset predicates are verified: the number of occurrences of H.A (Hole) has been incremented by one (remember that Hole is the index of the parent node!), V has lost an occurrence compared to A_Old and the occurrences of the other values have not changed

The Make_Prove_Loop lemma

The Make_Prove_Loop lemma helps proving the multiset predicates between A and A_Old considering the predicates holding between A_Old and A_Save and between A and A_Save. Its specification is:

procedure Make_Prove_Loop
  (A, A_Save, A_Old : T_Arr;
   V_Old, V         : T;
   Hole             : Positive) with
   Pre => A'Last < Positive'Last and then A'First = A_Save'First
   and then A'First = A_Old'First and then A'Last = A_Save'Last
   and then A'Last = A_Old'Last and then Hole in A'Range
   and then A_Save (Hole) = V_Old and then A (Hole) /= V
   and then Multiset_Add (A_Old, A_Save, V_Old)
   and then Multiset_Minus (A_Old, A_Save, V)
   and then Multiset_Retain_Rest_Double (A_Old, A_Save, V_Old, V)
   and then Is_Set (A_Save, Hole, A (Hole), A),
   Post => Multiset_Add (A_Old, A, A (Hole))
   and then Multiset_Minus (A_Old, A, V)
   and then Multiset_Retain_Rest_Double (A_Old, A, A (Hole), V);

Its implementation is:

procedure Make_Prove_Prologue
  (A, A_Old : T_Arr;
   V        : T;
   Hole     : Positive)
is
begin
   for E in T loop
      Occ_Set (A_Old, A, Hole, A (Hole), E);
      pragma Loop_Invariant
	(for all F in T'First .. E =>
	   (if F = V then Occ (A, F) = Occ (A_Old, F) - 1
	    elsif F = A (Hole) then Occ (A, F) = Occ (A_Old, F) + 1
	    else Occ (A, F) = Occ (A_Old, F)));
   end loop;
end Make_Prove_Prologue;

The only thing to do during the loop is to calculate the number of occurrences of the values in A, considering the number of occurrences in A_Save (only one value differs between A and A_Save at this point of the algorithm).

Using Make_Prove_Loop, GNATprove proves the main act.

Epilogue

Implementation of Epilogue

Now that the final index where V can be has been found, we just have to insert V in the array. The implementation of the Epilogue is:

	 -- beginning of Epilogue

	 A_Save     := H.A;
	 V_Old      := H.A (Hole);
	 H.A (Hole) := V;

	 Make_Prove_Epilogue (H.A, A_Save, A_Old, V, Hole);

	 -- end of Epilogue

      end if;
   end if;
end Push_Heap;

We need to make a final backup A_Save of the array to prove the Multiset_Unchanged predicates between A and A_Old.

The Make_Prove_Epilogue lemma

The lemma is very similar to the two others and is just here to finalize the proof after the Epilogue. Its specification is:

procedure Make_Prove_Epilogue
  (A, A_Save, A_Old : T_Arr;
   V                : T;
   Hole             : Positive) with
   Pre => A'Last < Positive'Last and then A'First = A_Save'First
   and then A'First = A_Old'First and then A'Last = A_Save'Last
   and then A'Last = A_Old'Last and then Hole in A'Range
   and then A (Hole) = V
   and then Multiset_Add (A_Old, A_Save, A_Save (Hole))
   and then Multiset_Minus (A_Old, A_Save, V)
   and then Multiset_Retain_Rest_Double (A_Old, A_Save, A_Save (Hole), V)
   and then Is_Set (A_Save, Hole, V, A),
   Post => Multiset_Unchanged (A, A_Old);

Its implementation is:

procedure Make_Prove_Epilogue
  (A, A_Save, A_Old : T_Arr;
   V                : T;
   Hole             : Positive)
is
begin
   for E in T loop

      Occ_Set (A_Save, A, Hole, V, E);

      pragma Loop_Invariant
	(for all F in T'First .. E => Occ (A, F) = Occ (A_Old, F));
   end loop;
end Make_Prove_Epilogue;

Using GNATprove, the implementations and the specifications, everything is now proved.