The final goal of formal methods in computer science is to prove that a program behaves as it should. The work of Zeyda and Cavalcanti, as reported in this paper, is another step toward this ultimate goal. The authors show that a current state-of-the-art proof environment can, using pragmatics and clever engineering, be used to build an environment for formal reasoning about specifications and programs.

The paper starts with an overview of the basic idea, namely to encode Hoare and He’s unifying theory of programming (UTP) within ProofPower-Z, a theorem-proving environment using higher-order logic and Z notation. The following sections briefly explain UTP and how it is encoded within Z notation.

The next section shows encoding in action, first introducing the Circus programming language and then explaining how to add an encoding of CSP and then the Circus programming language to the theory constructed thus far. The complete encoding now forms a hierarchy of layered theories, each building upon another.

The next sections explore how to reason within the hierarchy of theories, as well as how to deal with multiple instances of theories, which is needed to manage the encoding of a particular program added as another layer to the hierarchy.

The complete tower of theories constructed by the different encodings is conceptually very clear, but is very difficult in theorem proving, since proving a theorem at the upper level generates a plethora of subtheorems to be proved at the lower levels. Hence, section 7 deals with strategies and proof automation used for discharging most of the rather technical subtheorems.

The paper concludes with references to related and future work and an appendix showing several important but rather technical definitions of the encoding.

The paper is well written and understandable for anyone who enjoys a cursory acquaintance with Z notation (the notation itself is not completely explained). The work builds upon previous work in encoding UTP within Z notation, but extends this work in several aspects. Most notably, the clear layered architecture together with the proof tactics and automation mechanisms give a glimpse of what might someday be possible in the realm of formal methods.