Mathematics for Computer Science

Chapter 13 State Machines396

The rest of the logical rules follow the recursive definition ofwhileprograms.
There are axioms for the base case commands:

P.x/fxWDegP.e/

PfDonegP;

and proof rules for the constructor cases:



PfCgQANDQfDgR

PfCIDgR



P ANDTfCgQ

P AND TfifTthenCelseDgQANDT



P AND TfCgP

PfwhileTdoCodgP AND NOT.T/

Example13.2.8. TBA - Formal correctness proof of(13.4)for the Euclidean algorithm.

Problems for Section 13.2

Homework Problems

Problem 13.1.
Prove Theorem 13.2.6:

Theorem.
hC; i!

̋

Done; ^0

̨

iff ŒŒCççD^0

Hint: Prove the left to right direction by induction on the number of stepsC
needs to halt starting in environment. Prove the right to left direction by struc-
tural induction on the definition ofwhileprograms. Both proofs follow almost
mechanically from the definitions.