Contents: Dangling Composite Saboteur Data Split Cleaner Orphaned Thread Fictitious Implementation Conclusion Resources About the author Rate this article Related content: Magic with Merlin: Working with assertions Diagnosing Java code columns Subscriptions: dW newsletters dW Subscription (CDs and downloads)

Eric E. Allen (mailto:eallen@cs.rice.edu?cc=&subject=Using temporal logic with bug patterns)
Ph.D. candidate, Java programming languages team, Rice University
1 August 2002

Temporal logic is a formalism used to describe how a program state will change over time. In this article, his second on temporal logic and assertions, Eric Allen discusses how several of the most common bug patterns can be prevented by the use of temporal logic assertions. Share your thoughts on this article with the author and other readers in the discussion forum by clicking Discuss at the top or bottom of the article.

Although traditional assertions can increase the amount of checking that can be done over Java code, there are many checks you just can't perform with them. One way to handle these cases is with temporal logic. Recall from last month's article, "Assertions and temporal logic in Java programming," that temporal logic can help to provide much more powerful assertions over methods in programs, helping to enforce invariants that are otherwise hard to express formally.

We don't have to search far to find many useful invariants that can help to keep bugs out of our programs. In fact, we can augment our efforts to eliminate some of the most common patterns of bugs through the use of such temporal logic assertions. In this article, we'll examine some of the bug patterns most positively affected by the use of temporal logic. We'll be using the following bug patterns as examples:

• Dangling Composite. This bug occurs when your software throws a null-pointer exception, a hard-to-diagnose problem, due to the misrepresentation of a recursive datatype.
  
  
• Saboteur Data. This bug occurs when stored data fails to satisfy certain syntactic or semantic constraints; when software crashes due to an error, not in the coding, but in the data the code is manipulating.
  
  
• Split Cleaner. This bug occurs when the acquisition and freeing of a resource are split across method boundaries, allowing for certain flows of control that do not free the resource as they should, either by leaking them or by freeing them too early.
  
  
• Orphaned Thread. This bug occurs when a master thread throws an exception and the remaining threads continue to run, awaiting more input to the queue; this bug can cause a program to freeze.
  
  
• Fictitious Implementation. This bug occurs when you "implement" an interface without actually meeting its intended semantics.

The Dangling Composite bug pattern
The Dangling Composite bug pattern involves the misrepresentation of a recursive datatype, representing some base cases of the type as null values rather than separate classes. Doing so can cause hard-to-diagnose NullPointerExceptions.

For example, suppose you have formed the following hideous datatype to represent binary trees:

public class Tree {
  public int value;
  public Tree left;
  public Tree right;

  // Leaves are represented as Trees
  // with null branches.
  public Tree(int _value) {
    this.value = _value;
    this.left = null;
    this.right = null;
  }

  public Tree(int _value, Tree _left, Tree _right) {
    this.value = _value;
    this.left = _left;
    this.right = _right;
  }
}

Please, do us all a favor and don't use this code for any purpose other than as a bad example!

This code forms a Dangling Composite. Leaves are represented as Trees with null values for the left and right branches. If we try to recursively descend such a tree, we might easily cause the signaling of a NullPointerException.

The best way to prevent this bug pattern is to refactor the representation of the datatype as a Composite class hierarchy (see the article on this subject in the Resources section). Suppose you've completed just such a refactoring, as follows:

abstract class Tree {
  public int value;

  public Tree(int _value) {
    this.value = _value;
  }
}

class Leaf extends Tree {

  private Leaf(int _value) {
    super(_value);
  }
}

class Branch extends Tree {
  public Tree left;
  public Tree right;

  public Branch(int _value, Tree _left, Tree _right) {
    super(_value);
    this.left = _left;
    this.right = _right;
  }
}

You want to make sure that none of the remaining code (or any outside client code) is still constructing any of the old Dangling Composites: How can you do this?

Easy: do a clean compile. You'll get a compiler error if you try to construct an instance of class Tree. And because Tree is abstract, when you try to compile the new program, errors from the type checker will notify you about every construction site you should refactor. Additionally, the fact that the left and right fields were moved into class Branches means that every statement that sets the values of these fields in class Tree will cause a type-checking error too.

As this example demonstrates, type checkers can be extremely powerful refactoring tools. But consider this Doomsday scenario: new client programmers may very well remember the old practice of constructing leaves and attempt to construct new leaves by constructing new instances of class Branch, passing in null values for the left and right branches. Well, with temporal logic, you can put "Always" assertions on the fields that assert the field never takes a null value:

Always{left != null}
Always{right != null}

Granted, we could refactor the code in such a way that we could put a similar, ordinary, assertion on the field. But the process is much more involved. Specifically, we'd have to make the field private, add a setter, and refactor all places in the code where the field was set into calls on the setter (we could leverage the type-checker when performing this operation just like we could in the one above). Then we could put an ordinary assertion on the setter that the value set to is not null.

So, in this case, you can get away without using temporal logic assertions, but the task is much more difficult. Let's look at some other bug patterns where temporal logic gives us a bigger advantage.

The Saboteur Data bug pattern
The Saboteur Data bug pattern occurs when stored data fails to satisfy certain syntactic or semantic constraints. Such data can lie dormant for a long period of time and then explode when accessed.

The best way to prevent this pattern of bug is to perform sufficient checks over the data before putting it into long-term storage. But suppose you're maintaining a database with multiple clients, some of whom you don't control, all of whom have write access. How do you prevent the inappropriate insertion of data?

The first level of defense is to provide a single point of control (in the form of a Mediator) for all database access. However, you still might not be able to prevent malicious (or just clueless) clients from breaking your abstraction and entering data through an alternative path.

One way to help diagnose such problems quickly is to place temporal assertions over the database. These temporal assertions can state the syntactic and semantic invariants that are expected to hold, as "Always" assertions:

 ForAll x in Employees . Always{Age >= 0}
 ForAll x,y in Employees . Always{isMarried(x,y) implies isMarried{y,x}}
 etc.

The Split Cleaner bug pattern
The Split Cleaner bug pattern occurs when the acquisition and freeing of a resource are split across method boundaries, allowing for certain flows of control that do not free the resource as they should.

The best way to handle this pattern of bug is to refactor. But if the code base is large and sufficiently ugly, it can be difficult to ensure that every possible execution path has been traced through.

In that case, one form of Split Cleaner bug pattern will be transformed into another: instead of not freeing the resource at all down a path, we will attempt to free it more than once.

One thing we can do to help root out such tragic refactoring attempts is to place a temporal assertion in the method that originally acquires the resource to the affect that, if the resource is freed, it is not freed again until it is acquired.

For example, consider the following horrendously broken code for opening and closing files:

import java.io.*;

class ReaderMaker {
 
  String name;

  public ReaderMaker(String _name) {
    this.name = _name;
  }

 FileReader getReader() {
   return new FileReader(this.name);
 }
 ...
}

class Client1 {
 ...
 void doSomeWork(ReaderMaker maker) {
   FileReader reader = maker.getReader();
   ...
   reader.close();
 }
}

Who is responsible for closing FileReaders once we're done with them? Apparently the client is. This is a classic case of a split cleaner. It's just too easy to retrieve a resource and never free it when distinct methods are responsible for the two activities.

Temporal logic assertions are also useful for diagnosing such errors in the first place. For example, if we suspect a split cleaner, we can place an assertion over the method obtaining the resource that says that if a resource is acquired, then it is eventually freed. Then, if a program execution terminates without satisfying the assertion, we'll be notified with an error message. Ideally, all resource acquisitions would include such assertions in the first place, so that we're notified of split cleaners as soon as possible.

The Orphaned Thread bug pattern
The Orphaned Thread bug pattern occurs in a multithreaded program when some of the threads wait upon one thread that terminated.

Temporal logic assertions can help to diagnose such bugs. At every instance where a "wait" is placed for a reply from another thread, we can insert an assertion that the wait is eventually satisfied. If it never is, we'll get an error message saying so, when the program is terminated:

Always{wait() implies {Sometime{notify()}}}

The Fictitious Implementation bug pattern
One of the most straightforward applications of temporal logic assertions is for adding executable documentation on interfaces, thereby catching fictitious implementations of the interface as soon as these assertions are violated.

For example, consider my favorite example of an interface: a Stack. We could add very powerful assertions to this interface, to say things like the following:

// Once push(x) occurs, top() will return x until a push or a pop occurs.
Always{push(x) implies {{top() == x} until {push(y) || pop()}}  

// If the stack is empty, there should be no pops until a push occurs.
Always{isEmpty() implies {{! pop()} until {push(x)}}}

// (if we have a length operation) If the length is n, and a push occurs, 
// then next step, the length will be n+1.
Always{{length == n && push(x)} implies {Next{length == n + 1}}}

You get the idea.

Not only are the temporal logic assertions in the interface much more precise than prose would be, but they are actually enforced at run time (if we are running code instrumented to include checks on the assertions).

Tying up loose threads
As we have seen in this and the previous column, temporal logic assertions are powerful because they can help you make unit testing that much more powerful, because each temporal logic assertion can correspond to many traditional assertions.

In this article, we've shown how to use temporal logic assertions to combat the following bug patterns:

• Dangling Composite. Using a simpler "Always" assertion on the fields to assert that the field never takes a null value.
  
  
• Saboteur Data. Using "Always" assertions over a database to state the syntactic and semantic invariants that are expected to hold in that database.
  
  
• Split Cleaner. Using a temporal assertion in the method that originally acquires the resource to assert that if the resource is freed, it is not freed again until it is acquired. Temporal assertions are also useful here as error-producing diagnostic tools.
  
  
• Orphaned Thread. Using temporal assertions to assert that a "wait" is eventually satisfied wherever there is a wait placed for a reply from another thread. Again, this technique is useful as an error-producing tool.
  
  
• Fictitious Implementation. Using temporal assertions as added executable documentation on interfaces to catch fictitious implementations of the interface as soon as the assertions are violated.

Next time, we'll talk about yet more ways to help improve the robustness of your code. In particular, we'll look at some exciting new tools that can automatically detect intended assertions over your code, by examining your JUnit test suite.

Resources

• Participate in the discussion forum on this article. (You can also click Discuss at the top or bottom of the article to access the forum.)
  
  
• You can check out the Temporal Rover trial version (a tool for checking temporal logic assertions at run time) at the Time-Rover Web site. Note: Although the price of Temporal Rover and other products from Time Rover, Inc. is not made public, you may want to contact this company before testing the trial versions of their products; you might find the cost of the commercial versions to be prohibitive.
  
  
• The Stanford Encyclopedia of Philosophy carries a broad discussion of the philosophical and mathematical foundations of temporal logic.
  
  
• The Spin project at Bell Labs -- a widely distributed software package that supports the formal verification of distributed systems -- is an example of temporal logic model checking for hardware verification.
  
  
• Read all about assertions in Java 1.4 in John Zukowski's "Magic with Merlin: Working with assertions" (developerWorks, February 2002).
  
  
• Check out this XP site for a summary of the ideas behind extreme programming.
  
  
• The JUnit Web site provides links to many interesting articles from a multitude of sources that discuss program testing methods.
  
  
• Read all of Eric Allen's Diagnosing Java Code columns.
  
  
• Get hundreds of Java technology-related resources at the developerWorks Java technology zone.
  
  

What do you think of this document? Killer! (5) Good stuff (4) So-so; not bad (3) Needs work (2) Lame! (1) Send us your comments or click Discuss to share your comments with others.

developerWorks > Java technology