Download SPARK for Concurrent Programming - Infosun

61
6.3 Protected Type Priority List
entry Remove (Element Index : out Buffer Index) when List (Ext).Suc /= Ext
−−# post L (List) = Set Delete (L (List ˜), Element Index)
−−#
and List ( Element Index).Pri = Min (List ˜) and Min (List) >= Min (List˜);
is
begin
Element Index := List ( Ext). Suc;
List ( Ext). Suc := List ( List ( Ext). Suc).Suc;
end Remove;
The initialization procedure initializes the list extension element. The set consists
only of this single element.
Procedure Enter inserts an element into the list. The element must not be in the
list already. This pre-condition has been erroneously omitted in the original proof
of Coco. It is an essential condition because the linked list could contain inner
loops otherwise. Without this pre-condition, we were not able to finish the proof
successfully with the Checker.
Entry Remove removes an element from the list. There is no pre annotation because
the entry barrier condition will be satisfied when the entry body is executed. The
barrier states that the list must contain other elements than just Ext. The returned
element Element Index is no longer a member of the list and had the lowest priority
of the list. Consequently the minimum priority value of the new list is higher than
the minimum priority value of the unmodified list.
The loop invariant of procedure Enter specifies that element I is always a member of
the list and that the list is not modified during the loop step. Otherwise the Examiner
misses this piece of information. We declare the proof function Loop Condition as
follows:
−−# function Loop Condition (List : in Priority Queue; Index : in List Index) return Boolean;
Its semantics is defined by the loop condition List (List (I).Suc).Pri < Priority. The
loop traverses the list elements until it finds one with a higher priority value. This
leads us to an inductive definition. For the base case List (Ext).Suc, the function
Loop Condition returns true.
priority list(14): loop condition(L,fld suc(element(L,[buf ext]))) may be deduced.
The inductive step is valid if the priority value of the current element is smaller than
variable Priority and the induction hypothesis is satisfied.
priority list(15): loop condition(L,fld suc(element(L,[I]))) may be deduced from
[ loop condition(L,I), fld pri(element(L,[I])) < priority, I <> buf ext ].
We require another proof rule which gives us the information that the priority value
of an element is smaller than variable Priority in the loop condition.