win and sin : predicate transformers for concurrency

1 July 1990

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

Vol. 12 (3) , 396-428
https://doi.org/10.1145/78969.78970

Abstract

The weakest liberal precondition and strongest postcondition predicate transformers are generalized to the weakest invariant and strongest invariant . These new predicate transformers are useful for reasoning about concurrent programs containing operations in which the grain of atomicity is unspecified. They can also be used to replace behavioral arguments with more rigorous assertional ones.

Keywords

This publication has 9 references indexed in Scilit:

The ``Hoare Logic'' of CSP, and All That
ACM Transactions on Programming Languages and Systems, 1984
A Distributed Algorithm for Minimum-Weight Spanning Trees
ACM Transactions on Programming Languages and Systems, 1983
Ten Years of Hoare's Logic: A Survey—Part I
ACM Transactions on Programming Languages and Systems, 1981
On folk theorems
Communications of the ACM, 1980
A New Approach to Proving the Correctness of Multiprocess Programs
ACM Transactions on Programming Languages and Systems, 1979
Proving the Correctness of Multiprocess Programs
IEEE Transactions on Software Engineering, 1977
Proving assertions about parallel programs
Journal of Computer and System Sciences, 1975
A new solution of Dijkstra's concurrent programming problem
Communications of the ACM, 1974
An axiomatic basis for computer programming
Communications of the ACM, 1969