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.

dc.contributor.authorDawson, Jeremy
dc.date.accessioned2015-12-13T22:51:33Z
dc.date.available2015-12-13T22:51:33Z
dc.identifier.issn1571-0661
dc.identifier.urihttp://hdl.handle.net/1885/81138
dc.description.abstractWe 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.
dc.publisherElsevier
dc.sourceElectronic Notes in Theoretical Computer Science
dc.subjectKeywords: Abstracting; Computer program listings; Formal logic; Mathematical operators; Semantics; Theorem proving; Websites; Abstract commands; General correctness; Operational interpretation; Program logic; Computer programming languages Abstract commands; General correctness
dc.titleFormalising general correctness
dc.typeJournal article
local.description.notesImported from ARIES
local.description.refereedYes
local.identifier.citationvolume91
dc.date.issued2004
local.identifier.absfor080299 - Computation Theory and Mathematics not elsewhere classified
local.identifier.ariespublicationMigratedxPub9486
local.type.statusPublished Version
local.contributor.affiliationDawson, Jeremy, College of Engineering and Computer Science, ANU
local.bibliographicCitation.startpage21
local.bibliographicCitation.lastpage42
local.identifier.doi10.1016/j.entcs.2003.12.004
dc.date.updated2015-12-11T10:45:50Z
local.identifier.scopusID2-s2.0-18944381350
CollectionsANU Research Publications

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:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator