A language independent proof of the soundness and completeness of generalized Hoare logic (Q1122978)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 4108141
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | A language independent proof of the soundness and completeness of generalized Hoare logic |
scientific article; zbMATH DE number 4108141 |
Statements
A language independent proof of the soundness and completeness of generalized Hoare logic (English)
0 references
1989
0 references
For generalized Hoare logic (GHL), a formal system for proving invariance properties of programs was introduced in papers of \textit{L. Lamport} [Acta Inf. 14, 21-37 (1980; Zbl 0416.68032)] and \textit{L. Lamport}, \textit{F. B. Schneider} [ACM Trans. Program. Lang. Syst. 6, 281-296 (1984; Zbl 0536.68017)]. The authors first give a rigorous definition essentially independent of any programming language. Then they describe a corresponding semantic, introduce a suitable consequence relation, and prove for the provability relation of GHL its soundness as well as its (relative) completeness with respect to that consequence relation.
0 references
program verificiation
0 references
reasoning about programs
0 references
Hoare logic
0 references
0.8371567726135254
0 references
0.8218356370925903
0 references
0.8081793189048767
0 references
0.787790060043335
0 references
