BACKWARD SUBSTITUTION

An assignment statement
x := exp

Take the post condition, and substitute
any occurrence of x by exp

EXAMPLE:

x := x+1
{x = 6}

Substitute x by x+1 and obtain

{x + 1 = 6}

So the pre condition is:

{x = 5}