Formalising general correctness

Jeremy E. Dawson*

*Corresponding author for this work

    Research output: Contribution to journalConference articlepeer-review

    3 Citations (Scopus)

    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 languageEnglish
    Pages (from-to)21-42
    Number of pages22
    JournalElectronic Notes in Theoretical Computer Science
    Volume91
    DOIs
    Publication statusPublished - 16 Feb 2004
    EventProceedings of Computing: The Australasian Theory Symposium (CATS) - Dunedin, New Zealand
    Duration: 19 Jan 200420 Jan 2004

    Fingerprint

    Dive into the research topics of 'Formalising general correctness'. Together they form a unique fingerprint.

    Cite this