Go backward to The UNITY Programming Logic
Go up to Top
Go forward to Quantified Assertions

Assignment Statements

To prove

{p} x := E {q}
it suffices to show
p => qEx
(where qEx is q with E substituted for all occurences of x).

To prove

{p} x := e0 if b0 ~ ...~ en if bn {q}

it suffices to prove

{p and b0} x := e0 {q}
{p and bn} x := en {q}
p and (not b0 and ... and not bn) => {q}

Id: unity2.tex,v 1.1 1996/04/15 14:38:10 schreine Exp schreine

Prev Up Next