Concurrency: State Models and Java Programs

Chapter 14. Logical Properties

In Chapter 7, we saw that a property is an attribute of a program that is true for every possible execution of that program. We used property processes to specify safety properties and progress properties to express a limited but very common form of liveness property. Here we introduce logical descriptions of properties that capture both safety and liveness.

What do we mean by a logical description? We mean an expression composed out of propositions by logical operators such as and, or, not. A proposition is a statement that is either true or false. It can of course be formed from more primitive propositions by the logical operators and so the overall logical description is itself a proposition. Java already uses this form of expression in the assert construct. For example, using this construct we can assert that after executing some statements it should be true that variable i has the value 0 and variable j has the value 1: (assert i==0 && j==1).

The Java assert construct lets us specify a proposition concerning the state of selected variables that should be true at a particular point in the execution of a program. Of course, if this point is in a loop, it will be visited repeatedly. In our models, we wish to specify propositions that are true for every possible execution of a program without explicit reference to a particular point in the execution of that program. Furthermore, we wish to specify properties independently from models. A logic that permits ...