%0 Journal Article %1 oliveira_08_unifying %A Oliveira, Marcel %A Cavalcanti, Ana %A Woodcock, Jim %D 2009 %J Formal Aspects of Computing %K 2009 utp z _to_appear circus %R http://dx.doi.org/10.1007/s00165-007-0044-5 %T Unifying theories in ProofPower-Z %U http://dx.doi.org/10.1007/s00165-007-0044-5 %X Abstract The increasing interest in the combination of different computational paradigms is well represented by Hoare and He in the Unifying Theories of Programming (UTP). 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. Furthermore, the mechanisation of Circus, a language that combines Z, CSP, specification statements and Dijkstra^a€™s guarded command language, is also presented here. We also present an account of how this mechanisation is achieved, and more interestingly, of what issues were raised, and of our decisions. We aim at providing tool support not only for CSP and Circus, but also for further explorations of Hoare and He^a€™s unification, and for the mechanisation of languages whose semantics is based on the UTP.

@article{oliveira_08_unifying, abstract = {Abstract The increasing interest in the combination of different computational paradigms is well represented by Hoare and He in the Unifying Theories of Programming (UTP). 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. Furthermore, the mechanisation of Circus, a language that combines Z, CSP, specification statements and Dijkstra^{a}€™s guarded command language, is also presented here. We also present an account of how this mechanisation is achieved, and more interestingly, of what issues were raised, and of our decisions. We aim at providing tool support not only for CSP and Circus, but also for further explorations of Hoare and He^{a}€™s unification, and for the mechanisation of languages whose semantics is based on the UTP.}, added-at = {2009-02-11T20:10:30.000+0100}, author = {Oliveira, Marcel and Cavalcanti, Ana and Woodcock, Jim}, biburl = {https://www.bibsonomy.org/bibtex/295ee77583c201539add8ccc16fc0d735/leonardo}, citeulike-article-id = {1924099}, doi = {http://dx.doi.org/10.1007/s00165-007-0044-5}, interhash = {d73c2e9fb1916f4120660a73dd2eb4c8}, intrahash = {95ee77583c201539add8ccc16fc0d735}, journal = {Formal Aspects of Computing}, keywords = {2009 utp z _to_appear circus}, posted-at = {2007-11-15 22:03:45}, priority = {3}, timestamp = {2009-02-11T20:10:31.000+0100}, title = {Unifying theories in ProofPower-Z}, url = {http://dx.doi.org/10.1007/s00165-007-0044-5}, year = 2009 }