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.
展开▼
