The axiomatic semantics of programs based on Hoare's logic (Q800712)
From MaRDI portal
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
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