Download T2 : Automated Testing Tool for Java User Manual

9.3. SPECIFYING TEMPORAL PROPERTIES
9.3
53
Specifying Temporal Properties
With a bit extra work we can also use T2 to check temporal properties. A temporal property
is a property of an object over time. In many formal frameworks, temporal properties are often
associated with concurrent systems. It is true that many interesting properties of concurrent
systems are temporal. These would be beyond T2’s power, since it can test concurrent threads.
However, we can also express temporal properties of a sequential system. ’Temporal’ simply means
that they are time related.
Linear temporal properties are properties defined in terms of sequences of states that are
observable during the execution of a system. For example we may want to express that if p
holds on some state in a sequence, then q should hold on the next state. Since T2 also generates
sequences, we may wonder if can use it to check linear temporal properties. To some extend we
can.
We will need to fix the concept of ’sequences’ over which we will interpret our temporal properties: our sequences are sequences of field updates and method calls. So, the kind of sequences
generated by T2. More precisely, our temporal properties are interpreted over the sequences of
observable states induced by T2 sequences. The states we consider observable are the states after
each step in a test. In particular, the states of a target object during a method execution (that is,
its states as we are still inside the method) are considered as not observable. Its states just before
and after the call are observable.
Stringly speaking, temporal properties are properties over infinite sequences. In general they
cannot be directly checked, because T2 cannot generate infinite sequences. However we can do
a trick common in LTL (linear time temporal logic) model checking: we can convert it to an
automaton (called Buchi automaton, also known as never claim) which can be checked over finite
sequences.
Not all temporal properties require Buchi encoding though. Some can be translated quite
easily to a class invariant. Here is a simple example. This class Simple maintains a private integer
variable x and a private boolean variable open. The user of this class can call inc or dec on a
Simple object to increase or decrease the value of its x. However, once he calls close the state of
this object will freeze (it won’t change anymore).
private int x = 0;
private boolean open = true;
public void inc() { if (open) x++; }
public void dec() { if (open) x--; }
public void close() { if (open) open=false ; }
}
Suppose we want to express the following temporal property. In LYL notation it would be expressed as follows:
2(¬open ∧ (x = N ) → ◦(¬open ∧ x = N ))
for all N .
It says that once open becomes false, it will remain false, and furthermore the value of x will
not change anymore.
The implicit quantification over N is a bit problem. The straight forward implementation of
this will require us to to test the property for various N . Let’s introduce new variables that will