Compensable Programs - Formal Methods and Hybrid Real-Time Systems - page 352

Theorem 2.4
If P and Q are domain-disjoint, then
(1) P ⊕ Q = P Q

(2) ( P

⊕ Q ); R =( P ; R ) ⊕

( Q ; R )

Proof
(1) RHS

{ refinement calculus }

= b ∨ c ) (( b ⇒ S ) ∧ ( c ⇒ T )) { ordering of designs }

= b ∨ c ( b ∨ c ) ∧ ( ¬ c ∧ S ∨¬ b ∧ T ) { b ∧ c = false }

= LHS
(2) LHS

{ def of ⊕}

= b ∨ c ) ( b ∧ S ∨ c ∧ T ); R { refinement calculus }

= b ∨ c ) ∧¬ (( b ∧ S ∨ c ∧ T ); ¬ d ) ( b ∧ S ∨ c ∧ T ); U { b ∧ c = false }

= b ∧ ( ¬ ( b ∧ S ); ¬ d ) ∨ c ∧¬ (( c ∧ T ); ¬ d )

( b ∧ S ∨ c ∧ T ); U { def of ⊕}

= b

∧¬

(( b

∧ S ); ¬ d )

( b

∧ S ); U ⊕

c ∧¬ ( c ∧ T ); ¬ d )) ( c ∧ T ); U { refinement calculus }

= RHS
Theorem 2.5
If R = true U ,then( P ⊕ Q ); R =( P ; R ) ⊕ ( Q ; R ).

3D gnM ix

In this section we work towards a precise characterisation of the class of designs
[14] that are most useful in exception handling and compensation.
A subclass of designs may be defined in a variety of ways. Sometimes it is
done by a syntactic property. Sometimes the definition requires satisfaction of
a particular collection of algebraic laws. In general, the most useful definitions
are these that are given in many different forms, together with a proof that all
of them are equivalent.
To handling exception requires a more explicit analysis of the phenomena of
program execution. We therefore introduce into the alphabet of our designs a
pair of Boolean variables to denote the relevant observations.

Definition 3.1 ( eflag and eflag )
eflag records the observation that the program is asked to start when the exe-
cution of its predcessor halts due to an exception.
eflag records the observation that an exception occurs during the execution
of the program.