Abstract
We consider the abstract command language of Dunne, and his account of general correctness. We provide an operational interpretation of his abstract commands, and use the automated theorem proving system Isabelle to prove that this operational interpretation leads to Dunne's semantics. We consider the difficulties in precisely formalising some formulae found in the literature.
Original language | English |
---|---|
Pages (from-to) | 21-42 |
Number of pages | 22 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 91 |
DOIs | |
Publication status | Published - 16 Feb 2004 |
Event | Proceedings of Computing: The Australasian Theory Symposium (CATS) - Dunedin, New Zealand Duration: 19 Jan 2004 → 20 Jan 2004 |