Chapter 14: Logical Properties

Overview

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 us to do this is linear temporal logic. A proposition in this logic describes a set of infinite sequences for which the proposition is true. A program execution is essentially a sequence of states and so a program satisfies a linear temporal logic proposition if all its executions belong to the set described by the formula.

How can we refer to states when our LTS models are essentially based on actions or events? This chapter introduces fluents as a means of describing abstract states of our models. We show how logical properties for both safety and liveness can be specified in terms of fluents and analyzed using LTSA.