Download SPARK for Concurrent Programming - Infosun

97
A.2 Proof Rules
buffer guard invariant(S) requires [ S:any ] &
can be released(S,E) requires [ S:any, E:i ] &
A \/ B requires [ A:any, B:any ] &
A \ B requires [ A:any, B:any ] &
A in B requires [ A:any, B:any ] &
element(A,B) requires [ A:any, B:any ] &
A < B requires [ A:ire, B:ire ].
buffer guard(1): f(F,P) \/ (set [E]) may be replaced by f(update(F,[P],E),P+1)
if [ E not in f(F,P) ].
buffer guard(2): f(F,P) \ (set [element(F,[P−1])]) may be replaced by f(F,P−1)
if [ element(F,[P−1]) in f(F,P) ].
buffer guard(3): element(F,[J]) in f(F,P) may be deduced from [ J>=1, J<P ].
buffer guard(4): buffer guard invariant(S) may be replaced by
stacks ptr in range(fld stack(S))
and stacks max ptr(fld stack(S)) = conf buffer size.
buffer guard(5): can be released(S,E) may be replaced by
E not in f(fld free list(S),stacks ptr(fld stack(S)))
and not stacks full(fld stack(S)).
rule family priority list:
l(L) requires [ L:any ] &
sorted(L) requires [ L:any ] &
loop condition(L,I) requires [ L:any, I:any ] &
min(X) requires [ X:any ] &
priority list invariant(S) requires [ S:any ] &
can be removed(S,E) requires [ S:any, E:i ] &
A \/ B requires [ A:any, B:any ] &
A \ B requires [ A:any, B:any ] &
A in B requires [ A:any, B:any ] &
set A requires [ A:any ] &
element(A,B) requires [ A:any, B:any ] &
update(A,B,C) requires [ A:any, B:any, C:any ] &
A < B requires [ A:ire, B:ire ] &
for all(A,B) requires [ A:any, B:any ].
list(1): buf ext in l(L) may be deduced.
list(2): fld suc(element(L,[I])) in l(L) may be deduced from [ I in l(L) ].
list(3): for all(x : integer, x in l(L) −> I <> x) may be deduced from [ I not in l(L) ].
list(4): l(L) \/ (set [E]) & l(update(L,[I],upf suc(element(L,[I]),E)))
are interchangeable
if [ I in l(L), E not in l(L), fld suc(element(L,[E])) = fld suc(element(L,[I])) ].
priority list(5): l(L) \ (set [E]) & l(update(L,[I],upf suc(element(L,[I]),fld suc(element(L,[E])))))
are interchangeable
if [ I in l(L), E in l(L), fld suc(element(L,[I])) = E ].
priority list(6): l(update( , [buf ext], upf suc( , buf ext))) & (set [buf ext])
are interchangeable.
priority
priority
priority
priority