The axiomatic semantics of programs based on Hoare's logic (Q800712)

From MaRDI portal
Revision as of 19:43, 5 July 2023 by Importer (talk | contribs) (‎Created a new Item)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
scientific article
Language Label Description Also known as
English
The axiomatic semantics of programs based on Hoare's logic
scientific article

    Statements

    The axiomatic semantics of programs based on Hoare's logic (English)
    0 references
    0 references
    0 references
    1984
    0 references
    This paper is about the Floyd-Hoare principle which says that the semantics of a programming language can be formally specified by axioms and rules of inference for proving the correctness of programs written in the language. We study the simple language WP of while-programs and Hoare's system for partial correctness and we calculate the relational semantics of WP as this is determined by Hoare's logic. This calculation is possible by using relational semantics to build a completeness theorem for the logic. The resulting semantics AX we call the axiomatic relational semantics for WP. This AX is not the conventional semantics for WP: it need not be effectively computable or deterministic, for example. A large number of elegant properties of AX are proved and the Floyd-Hoare principle is reconsidered.
    0 references
    Floyd-Hoare principle
    0 references
    semantics
    0 references
    programming language
    0 references
    correctness of programs
    0 references
    while-programs
    0 references
    axiomatic relational semantics
    0 references

    Identifiers