A logic covering undefinedness in program proofs

H. Barringer, J. H. Cheng, C. B. Jones

    Research output: Contribution to journalArticlepeer-review


    Recursive definition often results in partial functions; iteration gives rise to programs which may fail to terminate for some imputs. Proofs about such functions or programs should be conducted in logical systems which reflect the possibility of "undefined values". This paper provides an axiomatization of such a logic together with examples of its use. © 1984 Springer-Verlag.
    Original languageEnglish
    Pages (from-to)251-269
    Number of pages18
    JournalActa Informatica
    Issue number3
    Publication statusPublished - Oct 1984


    Dive into the research topics of 'A logic covering undefinedness in program proofs'. Together they form a unique fingerprint.

    Cite this