Control Predicates are Better than Dummy Variables for Reasoning about Program Control

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.