Ana Cavalcanti and Jim Woodcock
November 1995, 55pp.
The lack of a method for developing programs from Z specifications is a problem that is now widely recognised. Some solutions have already been proposed. We are particularly interested in those that aim at the construction by calculation of efficient programs and that can be justified mathematically. These consist basically of different approaches for the integration of Z with a refinement calculus and seem to be quite effective, as they join a successful specification language to a successful refinement method. However, as far as we know, the proposed development methods have not yet been formalised. As they rely on a refinement calculus whose formalisation is based on weakest preconditions, the definition of a weakest precondition semantics for Z is a promising step in the direction of solving this problem. We define initially a weakest precondition semantics for LittleZ+, a sublanguage of Z that does not include generics and schema operators. Surprisingly maybe, the weakest precondition semantics of Z is precisely the same as that of LittleZ+. The availability of schema operators, however, makes the calculation of weakest preconditions very tedious and lengthy in some cases. As an answer to this problem, we introduce a number of theorems that help in calculating the weakest precondition of some schema expressions. The problem of correctness, which consists of comparing the weakest precondition and the relational semantics of Z, is addressed in the context of LittleZ+. Afterwords, we demonstrate that the introduction of schema expressions and generic definitions does not require the provision of another proof of correctness, so that we can be confident about the weakest precondition semantics in the context of Z as well. As yet further evidence of the correctness of this semantics definition, we identify and prove some healthiness conditions. We conclude by making some observations about the weakest precondition semantics, considering a related work and presenting the next steps of our research.