Skip navigation
Skip navigation

Formalising general correctness

Dawson, Jeremy

Description

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.

CollectionsANU Research Publications
Date published: 2004
Type: Journal article
URI: http://hdl.handle.net/1885/81138
Source: Electronic Notes in Theoretical Computer Science
DOI: 10.1016/j.entcs.2003.12.004

Download

There are no files associated with this item.


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  20 July 2017/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator