Download SPARK for Concurrent Programming - Infosun

63
6.3 Protected Type Priority List
entry Remove (Element Index : out Buffer Index);
−−# global in out State;
−−# derives Element Index from State & State from State;
private
List : Priority Queue;
end Priority List ;
As for the protected type Buffer Guard, we name the state variable simply State.
The invariant of the declaration part of the protected type Priority List has the same
semantics as in the protected type body.
priority list(17): priority list invariant(S) may be replaced by
sorted(fld list(S))
and fld pri(element(fld list(S), [buf ext])) = buf system priority last.
The declaration part also contains the declarations of the proof functions L, Sorted,
Min and Loop Condition, in addition to the set proof functions of Section 4.5.
As for the protected type Buffer Guard, we limit the pre- and post-conditions to
the bare necessities. Therefore only procedure Enter requires a pre-condition due to
refinement. It has the same semantics as the pre-condition of procedure Enter in the
body:
priority list(18): can be removed(S,E) may be replaced by E not in l(fld list(S)).
6.3.3 Proof Sessions for Procedure Initialize
Proof Session from Start to Finish:
No hypotheses are required for this verification condition; The conclusions are always
true.
CHECK|: list.
C1: sorted(update(list, [0], upf pri(upf suc(element(list, [0]), 0),
9223372036854775807)))
C2: l(update(list, [0], upf pri(upf suc(element(list, [0]), 0), 9223372036
The Simplifier replaced every occurrence of the list extension buf ext by its value 0.
The proof rule which enables this is automatically generated by the Examiner:
initialize rules(3): buf ext may be replaced by 0.
Our proof rules reference buf ext. We need to replace every 0 in the verification
condition by buf ext first because otherwise we could not apply a single one of our
proof rules.