The condition {true} is called the PRECONDITION
The condition {output = input1 + input2} is called the POST CONDITION
TECHNIQUE: If postcondition is true, can we deduce that the precondition is also true?
