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 this page instead for the normal view: A language independent proof of the soundness and completeness of generalized Hoare logic |
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A language independent proof of the soundness and completeness of generalized Hoare logic |
scientific article |
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
