Download Communicating Sequential Processes

5.5
Assignment
175
therefore
(q := q + 1 ; r := r − y ; X ) sat (y ≤ r ⇒ (r < (n + 1) × y ⇒ DIVLOOP 0 ))
where
DIVLOOP 0 =
(tr = hi ∨ (tr = h✓i ∧ (r − y) = (q ✓ − (q + 1)) × y + r ✓ ∧
r ✓ < y ∧ x ✓ = x ∧ y ✓ = y))
By elementary algebra of natural numbers
y ≤ r ⇒ (DIVLOOP 0 ≡ DIVLOOP )
therefore
(q := q + 1 ; r := r − y ; X ) sat (y ≤ r ⇒ (T (n + 1) ⇒ DIVLOOP ))
This result will be used in X10.
For general sequential composition, a much more complicated law is required, in which the traces of the components are sequentially composed, and
the initial state of the second component is identical to the final state of the
first component. However, the values of the variables in this intermediate state
are not observable; only the existence of such values is assured
L3
If P sat S (x, tr , x ✓ )
and Q sat T (x, tr , x ✓ )
and P does not diverge
then (P ; Q ) sat (∃ y, s, t • tr = (s ; t ) ∧ S (x, s, y) ∧ T (y, t , x ✓ ))
In this law, x is a list of all variables in the alphabet of P and Q , x ✓ is a list of
their subscripted variants, and y a list of the same number of fresh variables.
The specification of a conditional is the same as that of the first component
if the condition is true, and the same as that of the second component if false.
L4
If P sat S and Q sat T
then (P <| b >
| Q ) sat ((b ∧ S ) ∨ (¬ b ∧ T ))
An alternative form of this law is sometimes more convenient
L4A
If P sat (b ⇒ S ) and Q sat (¬ b ⇒ S )
then (P <| b >
| Q ) sat S