O'Reilly logo

Concurrency: State Models and Java Programs by Jeff Kramer, Jeff Magee

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required