Nuka, Gift and Woodcock, Jim (2004) Mechanising the alphabetised relational calculus. In: Electronic Notes in Theoretical Computer Science. Electronic Notes in Theoretical Computer Science, 95. Elsevier , Campina Grande, Brazil pp. 209-225.
| The full text of this publication is not available from this repository. (Contact us about this Publication) | |
| Official URL http://dx.doi.org/10.1016/j.entcs.2004.04.013 |
Abstract
In Hoare and He's unifying theories of programming, the alphabetised relational calculus is used to describe and relate different programming paradigms, including functional, imperative, logic, and parallel programming. In this paper, we give a formal semantics of the alphabetised relational calculus, and use our definition to create a deep embedding of the calculus in Z. This allows us to use one of the standard theorem provers for Z, in order to provide mechanised support for reasoning about programs in the unifying theory
| Item Type: | Conference or workshop item (Paper) |
|---|---|
| Additional information: | To be published in Electronic Notes in Theoretical Computer Science 2004 |
| Uncontrolled keywords: | Relational Calculus; Verification; UTP |
| Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
| Divisions: | Faculties > Science Technology and Medical Studies > School of Computing > Systems Architecture Group |
| Depositing User: | Mark Wheadon |
| Date Deposited: | 24 Nov 2008 18:01 |
| Last Modified: | 11 Jul 2009 02:31 |
| Resource URI: | http://kar.kent.ac.uk/id/eprint/14035 (The current URI for this page, for reference purposes) |
- Depositors only (login required):
