A Weakest Precondition Semantics For Z

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 refinement calculi 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 calculus expressions are provided. 1 Introduction Z [1, 2] is a well-established fo..