Unifying Theories in ProofPower-Z

摘要

The increasing interest in the combination of different computational paradigms is very well represented by Hoare & He in the Unifying Theories of Programming. In this paper, we present a mechanisation of part of that work in a theorem prover, ProofPower-Z; the theories of alphabetised relations, designs, reactive and CSP processes are in the scope of this paper. An account of how this mechanisation is done, and more interestingly, of what issues were raised and of our decisions, is presented here. We aim at providing tool support for further explorations of Hoare & He's unification, and for the mechanisation of languages based on this unification. More specifically, Circus, a specification language that combines Z, CSP, specification statements, and Dijkstra's guarded command language is our final target.