previous up next
Go backward to Invariants
Go up to B.5 Verification
Go forward to Termination
RISC-Linz logo

Program Properties

For proving the invariance of I, we first define a property that holds after each invocation of snap in node i:

snapi :<=>
    modei = SNAPPING,
    snapValuei = depositi,
    totalValuei = 0,
    forall h ~snappedi[h],
    missingSnapsi = ini().getSize(),
    forall j ~donei[j],
    missingValuesi = n.

Then we are going to define the properties that characterize the various states of node i:

Si LOOP :<=> statei = LOOP =>
    messagei = null.

Si TRIGGER :<=> statei = TRIGGER =>
    i = 0, messagei = null, snapi.

Si SELECT :<=> statei = SELECT =>
    modei /= TERMINATED.

Si DEPOSIT :<=> statei = DEPOSIT =>
    modei /= TERMINATED, 0 <= indexi < outi().getSize(),
    messagei instanceOf ValueMessage.

Si RECEIVE :<=> statei = RECEIVE =>
    modei /= TERMINATED, 0 <= indexi < ini().getSize(),
    inposin_i(index_i) < outposin_i(index_i).

Si SNAP :<=> statei = SNAP =>
    modei /= TERMINATED, 0 <= indexi < ini().getSize(),
    messagei instanceOf SnapMessage,
    messagei = Ini(indexi)[inposin_i[index_i]-1],
    snapi.

Si SNAP2 :<=> statei = SNAP2 =>
    modei in {SNAPPING, BROADCASTING},
    0 <= indexi < ini().getSize(),
    messagei instanceOf snapMessage,
    messagei = Ini(indexi)[inposin_i[index_i]-1].

Si SNAP3 :<=> statei = SNAP3 =>
    modei = BROADCASTING,
    missingSnaps = 0.

Si RESULT :<=> statei = RESULT =>
    modei /= TERMINATED, 0 <= indexi < ini().getSize(),
    messagei instanceOf ResultMessage,
    messagei = Ini(indexi)[inposin_i[index_i]-1].

Proof of Invariance: The invariance of I can be proved by showing that the generalized proposition I' defined as the conjunction of I and of all the properties above remains invariant under each state transition. The proof of this proceeds by case destinction of of statei as illustrated in Subsection A. These proofs are rather straight-forward from the code and from I; we omit the details.


Maintainer: Wolfgang Schreiner
Last Modification: November 14, 1997

previous up next