We can all agree that more checking of your Java code is better than less checking, and we've examined the use of assertions in testing new and improved programming. But while traditional assertions can increase the amount of checking that can be done, there are many checks we just can't perform with them.

However, there is a way to fill the checking gap that assertions leave. That is with the use of temporal logic. Temporal logic is a formalism used to describe how a program state will change with time. Let's discuss assertions and their properties and how temporal logic fits into checking. Then we'll take a look at a tool for processing temporal logic assertions.

Assertions and their properties

In addition to type checking and unit tests, assertions provide a great way to determine that various properties are maintained in a program.

Let's take a quick look at three categories of common assertion properties (common, but which don't offer us the full coverage we'd like), compare them with the types of program properties that can be expressed in a traditional assertion language, and examine assertion properties that are necessary for a multithreading context but are impossible to express as conventional assertions. We'll also offer some code examples.

Common assertion properties

Traditionally, assertion properties fall into one of these three categories:

• Pre-conditions assert that a property holds before execution of a code block.
• Post-conditions assert that a property hold after execution of a code block.
• Invariants assert that a property holds before and after the execution of a code block.

As helpful as assertions of these typical forms can be, they don't quite have the range for all the properties we'd like to be able to hold in a program. Let's look at typical assertion-expressed program properties.

Program properties expressable as assertions

This is just a short list of the types of program properties that can be expressed in a traditional assertion language -- properties that any programmer would like in code:

• To ensure that any nonce is generated only once
• To assert that documents are never accessed by unauthorized agents
• To assert that each thread is given a chance to run
• To assert that the system will never get itself into deadlock

A nonce (number used once) generator is used by security protocols to ensure freshness of transactions. As a simple concept in security, it is important to ensure that once a particular nonce is generated, it is not generated again. Another important security assertion is that secure documents are never accessed by unauthorized agents.

In multithreaded code, we'd like to assert that each thread is eventually given a chance to run. We'd also like to assure that the system will never get itself into a state where two or more threads are waiting on each other to supply a resource before they can continue processing (also known as deadlock).

Essential, non-conventional assertion properties

Following are two very useful types of properties that we'd like to make (and that we often want to make in the context of multithreaded code) that are simply not possible to express with conventional assertions:

• Safety assertions
• Liveness assertions

Safety assertions state that certain undesirable states of the system will never be reached under any circumstances. Liveness assertions state that certain events are guaranteed to occur eventually -- for instance, that a given thread will eventually wake up instead of sleeping forever.

Temporal logic can help make these assertions.

Back to top

Where the temporal logic comes in

temporal logic

Temporal logic defined

Temporal logic is a type of modal logic that is used for reasoning about changing properties with time.

Keeping time in mind, there are two general kinds of temporal logic:

• One that models the future as a linear sequence of events
• One that models the future as a tree branching out with various possibilities

In this article, we will only consider the temporal logic that models the future as a linear sequence of events. (The "branching tree" logic is quite cool, but it's computationally less tractable.)

A temporal logic is normally built atop a simpler set of atomic (small-unit) propositions, such as traditional program assertions. Various modal operators can then be applied to these atomic assertions to generate more complex assertions. The chain continues since traditional, Boolean, logical operators (such as and or or) can be applied to these assertions to generate even more complex assertions. Newly generated assertions can generate still more complex assertions, ad infinitum.

Temporal logic employs three (or four, depending on the model) common modal operators.

The typical modal operators

Back to top

How can I check up on my temporal logic?

These modal operators are usually available in temporal logic:

• Always
• Sometime
• Until
• Next (special case)

When applied to an assertion, Always ensures that the assertion continues to hold throughout the remainder of the execution of the program.

A much weaker operator, Sometime in a sense is a relative of Always. When applied to an assertion, Sometime stipulates that there must be some point in the future of the execution of the program during which the assertion holds.

Until works over two assertions, stipulating that as soon as the first assertion ceases to hold, the second must hold thereafter.

In contexts where time can be a model that consists of a series of discrete steps (as it can during, say, the execution of a program), you will sometimes see the Next operator added to this illustrious list. When Next is applied to an assertion, it stipulates that the assertion holds in the "next" step. Of course, this only makes sense when we are breaking time up into discrete steps.

Listing 1 shows some examples of temporal logic assertions:

Always x != 0
Sometime x == 0
{x == y} implies {Next {x == y + 1}}
{x == y} Until {y == 0}
{x == 0} implies {Next {Always {x != 0}}} // x is zero only once
Sometime {! this.isInterrupted()} // this thread is not interrupted forever

Here's an example assertion for two threads that asserts they never deadlock. (Note that the Boolean method isWaitingOn is used to check if one thread is holding on a task performed by the other.)

Always {x.isWaitingOn(y) implies {! y.isWaitingOn(x)}}

And temporal logic can be extended.

Extending the language

We can also extend the language of temporal logic to include quantifiers over collections of values in databases. For example, we could check that the assertion always held for all values in a table or for at least one value in the table.

With this level of expressiveness, we can form extremely powerful safety and security assertions. For example, consider a context where explicit agent objects can request access to various documents. We can form assertions about the clearance of the agents that can view various documents.

The following assertion guarantees that no agent views a document until he has clearance to do so:

ForAll agents in AgentPool
  {ForAll document in TopSecretDocumentPool
    {{! agent.canView(document)} Until {agent.hasClearanceFor(document)}}}

Now, at this point you might protest: "Well, it's great that I can say all of these things, but I don't have any way to check what I say is true, so what's the point?!"

To that I say: there are tools for checking just these types of assertions. In the case of digital circuits, assertions like these are statically verified before the chip is built.

In the case of software, our ability to statically check such assertions is paltry, but quality tools exist for checking that these assertions hold during particular runs of the program (such as, say, the runs of your unit tests). Assertions like these can help you to leverage unit testing to a much greater degree; each temporal logic assertion can correspond to countless traditional assertions (and that's just in cases where traditional assertions could be used to express the assertion at all).

Temporal Rover, from Time Rover Inc., is a tool for processing temporal logic assertions in Java programs and generating valid Java code from the assertions. (See Resources.) The company also offers a tool, DBRover, that works over database tables.

Temporal Rover includes all of the temporal operators as well as others designed for discussing events that occurred in the past. DBRover can quantify assertions over values in a database. Unfortunately, these tools are not free, but they do offer a 30-day free trial version.

Like assertions in JUnit, Temporal Rover/DBRover assertions give the programmer the option to print diagnostic messages when assertions fail. In fact, the syntax of Temporal Rover assertions is the same syntax I've used in the examples above, where assertions taken by the modal operators are surrounded with braces. These assertions are then passed to a TRAssert function (Temporal Rover Assert) with the following syntax:

/* TRAssert{<assertion> => <output string>}

The <output string> is displayed when the assertion fails to hold. In this way, TRAssert statements can be embedded into valid Java programs and these programs can still be compiled without Temporal Rover (of course, compiling without Temporal Rover will prevent the assertions from having any affect).

Back to top

A timely last word

Temporal logic assertions like these can help you to leverage unit testing to a greater degree because each temporal logic assertion can correspond to many traditional assertions. This means that these assertions are so powerful that they can help in a big way to stamp out many of the classic bug patterns discussed in this column.

In the next article, I will re-examine several bug patterns in the context of temporal logic assertions and demonstrate how to use these assertions to eliminate occurrences of the pattern.

Resources

• 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.
  
  
• The assertion facility is one eagerly awaited new feature of the Java 1.4 release. Learn more about it in "Magic with Merlin: Working with assertions" (developerWorks, February 2002).
  
  
• In a previous Diagnosing Java code installment, "The Fictitious Implementation bug pattern" (developerWorks, August 2001), Eric Allen shows you how to use assertions and unit tests as executable documentation.
  
  
• Granville Miller discusses the Unified Modeling Language and sequence diagramming, examining the role of conditional logic in sequence diagramming, in "Java Modeling: A UML workbook" (developerWorks, June 2001).
  
  
• "Testing, fun? Really?" (developerWorks, March 2001) helps you integrate testing into your daily development activities.
  
  
• Follow along in "Automating the build and test process" (developerWorks, August 2001) as Erik Hatcher shows you how he has modified the popular Ant 1.3 and the JUnit test framework for complete, customized automation of the build and test process.
  
  
• "Dynamic Type Checking in Jalapeno" presents a variety of techniques for performing dynamic type checking, reducing the run-time overhead of such tests.
  
  
• 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.
  
  
• You can check out the Temporal Rover trial at the Time-Rover Web site.
  
  
• Read all of Eric Allen's Diagnosing Java code articles.
  
  
  
• Find more Java resources on the developerWorks Java technology zone.
  
  

About the author

Rate this article

Comments

Back to top

Table of contents

• Assertions and properties
• Temporal logic connection
• How to check temporal logic
• A timely last word
• Resources
• About the author
• Comments