The axiomatic semantics of programs based on Hoare's logic
type: Item
instance of: scholarly article
title: The axiomatic semantics of programs based on Hoare's logic
zbMATH Open document ID: 0551.68016
DOI: 10.1007/BF00264252
author: John V. Tucker
author: J. A. Bergstra
published in: Acta Informatica
publication date: 1984-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 3878334
zbMATH Keywords: Floyd-Hoare principle
zbMATH Keywords: semantics
zbMATH Keywords: programming language
zbMATH Keywords: correctness of programs
zbMATH Keywords: while-programs
zbMATH Keywords: axiomatic relational semantics
describes a project that uses: ALGOL 68
MaRDI profile type: Publication
cites work: Ten Years of Hoare's Logic: A Survey—Part I
cites work: Q4193440
cites work: A complete logic for reasoning about programs via nonstandard model theory. I
cites work: Q3939224
cites work: Q3899466
cites work: Floyd's principle, correctness theories and program equivalence
cites work: Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs
cites work: Q3917477
cites work: Expressiveness and the completeness of Hoare's logic
cites work: Two theorems about the completeness of Hoare's logic
cites work: Hoare's logic and Peano's arithmetic
cites work: Hoare's logic for programming languages with two data types
cites work: Soundness and Completeness of an Axiom System for Program Verification
cites work: Q3911362
cites work: A PROPERTY OF 2‐SORTED PEANO MODELS AND PROGRAM VERIFICATION
cites work: Guarded commands, nondeterminacy and formal derivation of programs
cites work: Q4144755
cites work: Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer
cites work: An axiomatic basis for computer programming
cites work: Consistent and complementary formal theories of the semantics of programming languages
cites work: An axiomatic definition of the programming language Pascal
cites work: Infinite proof rules for loops
cites work: Proof rules for the programming language Euclid
cites work: Q4772698
cites work: CONSTRUCTIVE ALGEBRAS I
cites work: Q3881886
cites work: Axiomatic Definitions of Programming Languages
cites work: Q3928212
cites work: Computable Algebra, General Theory and Theory of Computable Fields
cites work: Q4039815
description: scientific article; zbMATH DE number 3878334