A generalization of Owicki-Gries's Hoare logic for a concurrent while language (Q1107518): Difference between revisions

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.