Program Semantics and Classical Logic

Example 2 As an example of an (informal) derivation in this calculus, we
show that

Γ, {Fι}X{F2} 'h {F₁}P{F2}
Γ 'h {F1}μX(P){F2}

is a derived rule:

(μ)

1. 'h {F₁}fail{F1 ∧ false}

2. 'h {F1}fail{F2}

3. Γ 'H {F1}fail{F2}

4. Γ, {F1}X{F2} 'H {F1}P{F2}

5. Γ 'h {F1}hX ^ Pi(X){F2}

(Test)

(Consequence, 1)

(Weakening, 2)

(premise)

(Recursion, 3,4)

Example 3 A second example uses the rule we have just derived to show

that

Γ '{F ∧ B}P{F}

Γ '{F}while B do P od {F ∧-B}

(while)

is another derived rule.

1.

Γ 'H {F ∧ B}P{F}

(premise)

2.

'H {F}B?{F ∧ B}

(Test)

3.

Γ 'H {F}B?; P{F}

(Composition, 1,2)

4.

{F}X{F ∧ -B} 'H {F}X{F ∧ -B}

(Id)

5.

Γ, {F}X{F ∧ -B} 'H {F}B?; P; X{F ∧ -B}

(Composition, 3,4)

6.

'h {F}-B?{F ∧-B}

(Test)

7.

8.

Γ 'h {F}μX((B?; P; X) ∪ -B?){F ∧ -B}

(μ, 7)