SRC Research Report 17

win and sin: Predicate Transformers for Concurrency.

Leslie Lamport.

Dijkstra's 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.

Back to the SRC Research Reports main page.

• PostScript compressed with UNIX compress -- 160 Kbytes
  
• PostScript compressed with GNU compress (gzip) -- 128 Kbytes
  
• PostScript compressed with ZIP -- 128 Kbytes
  
• PostScript -- 344 Kbytes
  
• Portable Document Format (PDF) -- 344 Kbytes