The KeY Project

[This is being written as an informal introduction to the KeY tool for software developers who don't have background in Logic and Automated Theorem Proving. If you are interested in theoretical aspects, consider reading from the list of research papers from people working on the project.]

The most common way of testing software in the industry is to pass it on to the QA team after development. Depending on the expertise of the QA personnel, they may come up with scenarios where the software doesn't "behave" as per the "expectations." If your company is somewhat sophisticated, writing these "expectations" in the form of functional specifications might be part of the software development life cycle. If you are even more sophisticated (or the correctness of your software is critical), you might even write pre- and post-conditions with each function/ method in your software.

As part of UML, OMG also defined Object Constraint Language (OCL). With OCL, for example, you can write class invariants (statements that always remain true for every instance of a class) and pre- and/ or post conditions for each method. With these things in place, an obvious need arises for checking whether the code satisfies these constraints or not.

The KeY tool (a joint project of the University of Karlsruhe, Chalmers University of Technology and the University of Koblenz) seamlessly integrates with Borland's Together Control Center (now called just Together) - a UML modeling solution. [Work has been done for JML support with Eclipse as well.] One of the features of Together, for example, is that it let's you draw UML diagrams for which it generates skeleton code. OCL expressions are written as comments in the code (somewhat similar in fashion to javadocs). The KeY tool can be used to verify the code against these constraints. It empowers you to find errors within the constraints as well.

As a very simple (and somewhat stupid) example consider a class Account with an attribute balance and two methods deposit () and withdraw (). Let's compare the following two implementations of withdraw() against the class invariant balance >= 0:

public boolean withdraw (int amount) {
   balance -= amount;
   return true;
}

public boolean withdraw (int amount) {
   if (balance < amount)
      return false;

   balance -= amount;
   return true;
}

The implementation on the top is said to break the class invariant, while the one below "preserves" it. An attempt to prove the correctness of the code on the left will fail. While an automated theorem prover might not be needed for complete verification of the applications in the industry, there are specific areas where 100% verification is a need: for example, in safety critical application; or in case of smart card applications where it's almost impossible to recollect all the smart cards from the customers in case a bug is later detected. The latter of the two areas is the main focus of KeY.

Amongst other things, the KeY tool can check your implementation as well as specifications for structural subtyping, behavioural subtyping, satisfaction of post conditions on method invocation and preservation of class invariants. For a not-so-obvious-at-first-sight example, consider the following invariant alongw ith the code that follows:

//Note: these are not 100% accurate OCL expressions
pre-condition: i >= 0 and j >= 0 and
         i<arr->size and j<arr->size
post-condition: arr[i] = arr[j]@pre and arr[j] = arr[i]@pre
void swap (int arr[], int i, int j) {
   arr[i] += arr[j];
   arr[j] = arr[i] - arr[j];
   arr[i] -= arr[j];
}

The code swaps two elements in an array by using integer arithmetic (and avoids use of a temporary variable). However, it violates the specs when you invoke it with i=j. Such non-obvious cases may be missed by the QA people as well. Unfortunately, testing can only show the existence of bugs but not their non-existence. The only guaranteed way of "proving" program correctness is either to use a theorem prover, like KeY, or to exhaustively test every possibility.

---

Philipp Ruemmer has written a paper on this topic. I shall be extending the work (hopefully) for generating counter examples. I'll also get the opportunity to attend the 4th KeY Symposium from 8th to 10th of June.