Go backward to Invariants Go up to B.5 Verification Go forward to Termination

Program Properties

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

snap_i :<=>
    mode_i = SNAPPING,
    snapValue_i = deposit_i,
    totalValue_i = 0,
    forall h ~snapped_i[h],
    missingSnaps_i = in_i().getSize(),
    forall j ~done_i[j],
    missingValues_i = n.

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

S_i ^LOOP :<=> state_i = LOOP =>
    message_i = null.

S_i ^TRIGGER :<=> state_i = TRIGGER =>
    i = 0, message_i = null, snap_i.

S_i ^SELECT :<=> state_i = SELECT =>
    mode_i /= TERMINATED.

S_i ^DEPOSIT :<=> state_i = DEPOSIT =>
    mode_i /= TERMINATED, 0 <= index_i < out_i().getSize(),
    message_i instanceOf ValueMessage.

S_i ^RECEIVE :<=> state_i = RECEIVE =>
    mode_i /= TERMINATED, 0 <= index_i < in_i().getSize(),
    inpos_{in_i(index_i)} < outpos_{in_i(index_i)}.

S_i ^SNAP :<=> state_i = SNAP =>
    mode_i /= TERMINATED, 0 <= index_i < in_i().getSize(),
    message_i instanceOf SnapMessage,
    message_i = In_i(index_i)[inpos_{in_i[index_i]}-1],
    snap_i.

S_i ^SNAP2 :<=> state_i = SNAP2 =>
    mode_i in {SNAPPING, BROADCASTING},
    0 <= index_i < in_i().getSize(),
    message_i instanceOf snapMessage,
    message_i = In_i(index_i)[inpos_{in_i[index_i]}-1].

S_i ^SNAP3 :<=> state_i = SNAP3 =>
    mode_i = BROADCASTING,
    missingSnaps = 0.

S_i ^RESULT :<=> state_i = RESULT =>
    mode_i /= TERMINATED, 0 <= index_i < in_i().getSize(),
    message_i instanceOf ResultMessage,
    message_i = In_i(index_i)[inpos_{in_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 state_i as illustrated in Subsection A. These proofs are rather straight-forward from the code and from I; we omit the details.