x = 1; // P
y = x + 1; // Q
x = y + 2; // R
For every possible execution (e) of this program, P must precede
Q and Q must precede R.
forall e: P ® Q ® R
The “®” operator means precedes or happens before. P ®Q means that
P must begin before Q begins and further P must finish before Q finishes
ie. there is no overlap in the execution of the instructions making up P & Q.
If each component P & Q is made up of several instructions then:
forall e: p1 ® p2 ... ® pm ® q1 ® q2 ... ® qn
There is a total ordering of the instructions making up P & Q.