zbMATH — the first resource for mathematics

A generalization of Owicki-Gries’s Hoare logic for a concurrent while language. (English) Zbl 0653.03017
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.
Reviewer: J.Zlatuska

03B70 Logic in computer science
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] Abrahamson, K., Modal logic of concurrent programs, (), 21-33
[2] Apt, K., Recursive assertions and parallel programs, Acta inform., 15, 219-232, (1981) · Zbl 0436.68009
[3] Barringer, H.; Kuiper, R.; Pnueli, A., Now you may compose temporal logic specifications, Proc. 16th STOC, 51-63, (1984)
[4] Brookes, S., An axiomatic treatment of a parallel programming language, (), 41-60
[5] Hennessy, M.; Plotkin, G., Full abstraction for a simple parallel programming language, (), 108-120 · Zbl 0457.68006
[6] Jones, C., Specification and design of (parallel) programs, Proc. IFIP, 321-332, (1983)
[7] Lamport, L., The Hoare logic of concurrent programs, Acta inform., 14, 21-37, (1980) · Zbl 0416.68032
[8] Owicki, S., Axiomatic proof techniques for parallel programs, () · Zbl 0395.68015
[9] Owicki, S.; Gries, D., An axiomatic proof technique for parallel programs I, Acta inform., 6, 319-340, (1976) · Zbl 0312.68011
[10] de Roever, W., The quest for compositionality—a survey of assertion-based proof systems for concurrent programs. part 1: concurrency based on shared variables, () · Zbl 0594.68019
[11] Soundararajan, N., A proof technique for parallel programs, Theoeret. comput. sci., 31, 13-29, (1984) · Zbl 0543.68010
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.