Example:
Read in 2 integers and output their product divided by their sum. You are guaranteed that there are 2 integer values in the input stream.
Precondition = { Input stream contains two integer values}
Postcondition = { Product / Sum is output}
{Q} p {R} states that a program p. once started in a state satisfying {Q} will lead to a situation characterised by{R}
{Q} may also be written as the weakest precondition of p tp achieve postcondition R i.e. wp(p, R)