
Design by Proof Rules 157
derive a precondition of a part of the program segment in question arises, that is, task 1. Task 3 does not arise
in an engineering design process, because it is a goal-directed process and is expressed in the post-condition,
which must, therefore, be specifi ed before meaningful design or verifi cation work can start.
Some of the rules, useful in a design process are:
1. Strengthening a pre-condition and weakening a post-condition if
{}{}
{} {}
11 1 1VV VSP P P
VSP
⇒⇒∧∧
Strengthening a condition means making it stricter, while weakening it means making it more permissive.
When working backward (upward, that is, towards its ...