(extended version)
Ana Cavalcanti and Jim Woodcock
May 1997, 28pp.
Revised January 1998.
The lack of a method for developing programs from Z specifications is a difficulty widely recognised. In response to this problem, different approaches to the integration of Z with a refinement calculus have been proposed. These programming techniques are promising, but, as far as we know, have not been formalised. Since they are based on a refinement calculus formalised in terms of weakest preconditions, the definition of a weakest precondition semantics for Z is a significant contribution to the solution of this problem. In this paper, we actually construct a weakest precondition semantics from a relational semantics proposed by the Z standards panel. The construction provides reassurance as to the adequacy of the resulting semantics definition and, additionally , establishes an isomorphism between weakest preconditions and relations. Compositional formulations for the weakest precondition of some schema expressions are provided.