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.

© Antoni Diller (20 April 2014)