A generalization of Owicki-Gries's Hoare logic for a concurrent while language
type: Item
instance of: scholarly article
title: A generalization of Owicki-Gries's Hoare logic for a concurrent while language
zbMATH Open document ID: 0653.03017
DOI: 10.1016/0304-3975(88)90033-3
author: Colin Stirling
published in: Theoretical Computer Science
publication date: 1988-01-01T00:00:00Z
review text: The paper presents a generalization of Owicki-Gries's Hoare logic for a concurrent while language. Two deficiencies are connected with Hoare logics in connection with parallel programs: The assertions tell us little about properties of the intermediate states, and the usual meaning of programs do not include the possible effects of interference. Various approaches to logically coding the additional information are briefly summarized, and a reformulation and generalization of Owicki-Gries's Hoare logic is defined as a system comprising syntax-directed rules. The Hoare triples have the form \(\{\) \(\Gamma\),A\(\}\) \(p\{\) B,\(\Delta\) \(\}\), where \(\Gamma\), \(\Delta\) are sets of invariants. The system is shown to be sound with respect to the semantics and complete with respect to Owicki-Gries's system. The paper concludes with a sample proof illustrating the relevance of the system proposed for program development.
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 4064965
zbMATH Keywords: parallal language semantics
zbMATH Keywords: program verification
zbMATH Keywords: Hoare logic
zbMATH Keywords: concurrent while language
zbMATH Keywords: parallel programs
reviewed by: Jiří Zlatuška
MaRDI profile type: Publication
full work available at URL: 0304-3975(88)90033-3
OpenAlex ID: W2071748540
cites work: Q4187288
cites work: Recursive assertions and parallel programs
cites work: Q3685165
cites work: Q3907039
cites work: The ''Hoare logic'' of concurrent programs
cites work: Q4178461
cites work: An axiomatic proof technique for parallel programs
cites work: Q3725529
cites work: A proof technique for parallel programs
description: scientific article; zbMATH DE number 4064965