Mechanising a unifying theory

In this paper, we present a formalisation of a subset of the unifying theories of programming (UTP). In UTP, the alphabetised relational calculus is used to describe and relate different programming paradigms, including functional, imperative, logic, and parallel programming. We develop a verification framework for UTP; we give a formal semantics to an imperative programming language, and use our definitions to create a deep embedding of the language in Z. We use ProofPowerZ, a theorem prover for Z to provide mechanised support for reasoning about programs in the unifying theory.