win and sin : predicate transformers for concurrency
Leslie Lamport · ACM Transactions on Programming Languages and Systems · 1990
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.