Control predicates are better than dummy variables for reasoning about program control

1 April 1988

journal article
research article
Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems

Vol. 10 (2) , 267-281
https://doi.org/10.1145/42190.42348

Abstract

When explicit control predicates rather than dummy variables are used, the Owicki-Gries method for proving safety properties of concurrent programs can be strengthened, making it easier to construct the required program annotations.

Keywords

This publication has 8 references indexed in Scilit:

An Axiomatic Semantics of Concurrent Programming Languages
Published by Springer Nature ,1985
The ``Hoare Logic'' of CSP, and All That
ACM Transactions on Programming Languages and Systems, 1984
The ?Hoare logic? of concurrent programs
Acta Informatica, 1980
Proving the Correctness of Multiprocess Programs
IEEE Transactions on Software Engineering, 1977
An axiomatic proof technique for parallel programs I
Acta Informatica, 1976
Proving assertions about parallel programs
Journal of Computer and System Sciences, 1975
An axiomatic basis for computer programming
Communications of the ACM, 1969
Assigning meanings to programs
Published by American Mathematical Society (AMS) ,1967