Download SPARK for Concurrent Programming - Infosun

6.3 Protected Type Priority List
72
Proof Session for Refinement Integrity
There are two verification conditions to prove. In analogy to the refinement integrity
proof of procedure Initialize, only the constants buf system priority last and buf ext
must be replaced. We do not show this here.
6.3.5 Proof Sessions for Procedure Enter
Proof Session from Start to Loop Invariant
As in the proof of procedure Remove we must replace 0 by buf ext before we can
apply any of our proof rules.
CHECK|: infer 0 = buf ext using enter rules(3).
CHECK|: replace all: 0 by buf ext using eq(1).
CHECK|: list.
C1: buf ext in l(list)
C2: loop condition(list, fld suc(element(list, [buf ext])))
C1 and C2 can be inferred directly; no hypotheses are required. Both are the base
cases of an induction.
CHECK|: infer c#1 using priority list(1).
∗∗∗ PROVED C1: buf ext in l(list)
CHECK|: infer c#2 using priority list(14).
∗∗∗ PROVED C2: loop condition(list, fld suc(element(list, [buf ext])))
∗∗∗ VC PROVED −− Well done!
Proof Session for Loop Invariant
This verification condition is the inductive step of the loop.
CHECK|: infer 0 = buf ext using enter rules(3).
CHECK|: replace all: 0 by buf ext using eq(1).
CHECK|: list.
H1: i in l(list OLD)
H2: loop condition(list OLD, fld suc(element(list OLD, [i])))
H16: fld pri(element(list OLD, [fld suc(element(list OLD, [i]))])) <
priority
−−>
C1: fld suc(element(list OLD, [i])) in l(list OLD)
C2: loop condition(list OLD, fld suc(element(list OLD, [fld suc(element(
list OLD, [i]))])))