EXAMPLE OF BACKWARD SUBSTITUTION

Prove the following:

{x>0 and y>0}
z := x * y
{z > -1}

By backward substitution

{x * y > -1}

This is implied by {x>0 and y>0}

The general Hoare's proof rule:

F0 implies F1,{F1}S1{F2},{F2}S2{F3},F3 implies F4
________________________________________________
{F0}S1;S2{F4}