Z and Hoare logics

When I wrote "Z and Hoare logics" Z was gaining ground in the software development community as a specification language, but there was then no standard way of relating a Z specification to program code. Hoare logics had been around for about 20 years at that time. They were well understood and widely taught as a method of proving that a program meets its specification. In "Z and Hoare logics" I put forward a proposal about how combining both techniques and notations could provide a path from a high-level Z specification to program code. Rules and conventions for combining the two notations were given and their use was illustrated by two case studies.

References

Antoni Diller, "Z and Hoare Logics", in J. E. Nicholls (editor), Z User Workshop: York 1991, [London, Springer-Verlag, 1992], pp. 59–76; a PDF version of this paper is available on this website.
This paper is mentioned and an idea from it used in Shengchao Qin and Guanhua He's paper Linking Object-Z with Spec# in the 12th IEEE International Conference on Engineering of Complex Computer Systems, 11–14 July 2007, Auckland, New Zealand; proceedings. Los Alamitos, CA: IEEE, pp. 185–196.