Go up to B.5 Verification Go forward to Invariants

Correctness Theorem

The following definitions capture the measures we are interested in:

Definition. [Network Value] The network value value_net is the sum of all node deposits plus the sum of the values of all messages being processed in some node plus all channel values:

value_net := Sum_i (deposit_i + mvalue(message_i)) + Sum_c cvalue(c).

Definition. [Channel Value] The channel value cvalue(c) of a channel c is the sum of all message values in c:

cvalue(c) := Sum_k mvalue(c[k])

Definition. [Message Value] The message value mvalue(m) of a message m is the value carried by m, if m is a value message, and 0, otherwise:

mvalue(m) :=

m.getValue()	if m instanceOf ValueMessage
0	else

The correctness theorem for our program can be then expressed as follows:

Theorem. [Correctness] When a node terminates, its totalValue equals the network value:

mode_i = TERMINATED => totalValue_i = value_net