Calculating with procedure calls (Q685524)

Various proof rules for procedure calls in weakest precondition semantics have been proposed. The author gives a proof rule that is very easy to use, but does not yield the best possible answer for every specification -- only for a large class of specifications called normal specifications. In the Appendix, he shows how every specification can be transformed into an equivalent normal one.