win and sin : predicate transformers for concurrency
Author:
Open Access
- 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
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 10 references indexed in Scilit:
- The ``Hoare Logic'' of CSP, and All ThatACM Transactions on Programming Languages and Systems, 1984
- Reasoning about nonatomic operations1983
- A Distributed Algorithm for Minimum-Weight Spanning TreesACM Transactions on Programming Languages and Systems, 1983
- Ten Years of Hoare's Logic: A Survey—Part IACM Transactions on Programming Languages and Systems, 1981
- On folk theoremsCommunications of the ACM, 1980
- A New Approach to Proving the Correctness of Multiprocess ProgramsACM Transactions on Programming Languages and Systems, 1979
- Proving the Correctness of Multiprocess ProgramsIEEE Transactions on Software Engineering, 1977
- Proving assertions about parallel programsJournal of Computer and System Sciences, 1975
- A new solution of Dijkstra's concurrent programming problemCommunications of the ACM, 1974
- An axiomatic basis for computer programmingCommunications of the ACM, 1969