Prove, don't test!
( Dr. Attila Ulbert / Alvicom Testcenter )


Alvicom Testcenter

We spend considerable time on designing an application, precisely document/specify the behaviour of its modules, classes, methods, etc., and yet we also need to implement tests that can be considered as the formal versions of the (informal) specifications. What if we specified everything formally in Java Modeling Language (JML), and proved the correctness of the implementation?

The Java Modeling Language

The Java Modeling Language [1] can be used to specify the behaviour of Java modules by adding annotations to Java source files. It is easy to learn and easy for Java programmers to use. Moreover, it is supported by several tools for static analysis and verification.

Maybe one of the most promising tools is the Extended Static Checker for Java version 2 (ESC/Java2) by David Cok and Joe Kiniry [2]. The original ESC/Java tool was delevoped at Compaq Research, Cok and Kiniry continued the work on version 2 of ESC/Java (it is still in alpha version) after Compaq stopped with its development. ESC/Java2 attempts to check the correctness of JML-annotated Java programs by static analysis of the program code and its formal annotations.

So, in theory, we can specify the behaviour of our application, and verify the correctness of the implementation. And that's all! We can stop after the specification, and do not have to implement tests. Great, isn't it!? Well, in theory.

Let's see the state-ot-the-art practice!

Writing JML specifications

We have jumped into deep water and started to make certain TCK tests of the SAMS API obsolete [3]. The SAMS API is a messaging API for SMS and MMS, which enables composing, sending and receiving short messages and multimedia messages [4]. The SAMS Reference Implementation and TCK can be downloaded from Forum Nokia [5][6].

After the RI and TCK are installed, we can start specifing the bahaviour of some of the modules of the API. We have chosen to start with interface javax.sams.messaging.sms.TextMessage and its implementation:

public interface TextMessage extends SmsMessage {
  public static final int VOICEMAIL_WAITING = 0;
  public static final int FAX_WAITING = 1;
  public static final int EMAIL_WAITING = 2;
  public static final int OTHER_WAITING = 3;
  public String getText();
  public void setText(String text) 
    throws InvalidArgumentException, MessageSizeExceededException;

  public void setMessageWaitingIndicator(
    int type, int count, boolean store)
    throws InvalidArgumentException, MessageSizeExceededException;

  public int getMessageWaitingCount(int type) 
    throws InvalidArgumentException;

  public boolean getMessageWaitingStore(int type) 
    throws InvalidArgumentException;

  public int[] getMessageWaitingTypes();

As we can see, interface TextMessage specifies a fairly simple container for text SMS messages. The API specification of method getText() states:

Returns the content of the text message as a String. Returns null if the content has not been set.

  the content of the message or null

Well, it is an easy job to specify this in JML:

  @ public normal_behavior
  @   _text_set ==> \result == _message_text; 
  @ // Returns the content of the text message as a String.
  @   !_text_set ==> \result == null; 
  @ // Returns null if the content has not been set.
public String getText();

We also needed a model field for the message text and a specification variable (ghost field):

//@ ghost boolean _text_set = false;
//@ instance model String _message_text;

The _text_set variable will indicate whether the message text has already been set. The _message_text model field contains the SMS message text. The JML model fields must have an actual representation in the implementing class, in our case this will be in class

Okay, we we are finished with getText(), now we should specify method setText(String) as well. Its API specification is as follows:

Sets the content of the text message.

The length of the content depends on the character set encoding and whether there are optional headers. 
If the content does not fit into one message, it will be automatically split into multiple message segments.

The maximum number of segments in the message can be set by setMaxSegmentCount method. 
If the message size will exceed the maximum count, an MessageSizeExceededException will be thrown.

The text may be set to null, which indicates an empty content.

  text - the content text of the message

    - if the text is invalid 
    (e.g. it includes unsupported characters)
    - if content makes the message too long

See Also:

The TCK assertion documentation (JSR212_TCK_J2EE\doc\SAMS_TCK_Assertions_v11.doc) provides a precise, informal description of the expected behaviour of method setText(String):


  Sets the content of the text message.

  If the message became oversized, 
  a MessageSizeExceededException 
  will be thrown when the message is tried-to-be-sent.

  InvalidArgumentException is thrown if the text is invalid 
  (e.g. it includes unsupported characters).

Equivalence class partitioning

text Expected result
valid Sets the content of the text message.
invalid (oversized) MessageSizeExceededException
Boundary value analysis
text Expected result
null, "" Sets the content of the text message.
Text with length of MaxSegmentCount * SegmentSize Sets the content of the text message.
Text with length of MaxSegmentCount * SegmentSize + 1 MessageSizeExceededException

Our JML description reflects these assertions.

/*@ public normal_behavior
  @   ensures (_message_text == text || _message_text == null) 
  @       && _text_set; // Assertion1
  @ also
  @ public exceptional_behavior
  @   signals (Exception e) (e instanceof InvalidArgumentException
  @      || e instanceof MessageSizeExceededException) &&
  @     _text_set == \old(_text_set) 
  @     && _message_text == \old(_message_text); 
  @     // Assertion2 and Assertion3
public void setText(String text) 
  throws InvalidArgumentException, MessageSizeExceededException; 

The description is somewhat (very) liberal in the case of formulation Assertion2 and Assertion3, but it can be made more strict later. Apart from this the description expresses what the API spec says...


So we have one setter and the corresponding getter method specified. Before checking the correctness of the implementation, we need to give a representation of the _message_text model field in class TextMessageImpl. This is a piece of cake as class TextMessageImpl stores the message in a String field. We use a representation function to bind them together:

public class TextMessageImpl extends SmsMessageImpl implements TextMessage {
  //@ represents _message_text <- messageText;
  private String messageText = null;

We also need to deal with _text_set specification field. It is initialized to value false, and it's value must be changed to true, if the message text is successfully set. So let's extend the implementation of method setText(String) with a simple annotation:

public void setText(String text) 
  throws InvalidArgumentException, MessageSizeExceededException {
    //@ set _text_set = true;

The moment of truth!

What have we achieved so far? Based on the API specification we have provided a formal description of methods getText() and setText(String), and we have also given a representation of the model and specification fields. Let's see whether or not the SAMS reference implementation (RI) is correct and complies with the specification. (We could do this by running the TCK, but this article is about formal methods, isn't it? So, some other time...)

To check the correctness of the RI, we run ESC/Java2 in directory JSR212_RI:

$ escj -cp src/

  getText() ...
    [0.061 s 12850496 bytes]  passed 
  setText(java.lang.String) ...
  Caution: Not checking body of anonymous 
class (subclass of Rollback)
        new Rollback() {
    [0.504 s 13376272 bytes]  passed


Ugh, bad news. We have to do something with the anonymous classes. Quick and dirty solution: just for now, create a new method containing the problematic code-fragment.

public void setText(String text) 
  throws InvalidArgumentException, MessageSizeExceededException {
    String oldValue = messageText;

    messageText = text;

    if (!check((messageText != null)
     && ((oldValue == null) || ((oldValue != null) 
     && (oldValue.length() < messageText.length()))), oldValue)) {
      messageText = oldValue;

  //@ set _text_set = true;

private boolean check(boolean b, String oldValue)  throws 
InvalidArgumentException, MessageSizeExceededException {
  try {
    checkSegmentCount(b, oldValue,
      new Rollback() {
        public void rollback(Object data) {} });
    return true;
  } catch (Exception e) {
    return false;

Run ESC/Java2 again:

  getText() ...
    [0.061 s 12822536 bytes]  passed 
  setText(java.lang.String) ...
    [0.506 s 12873120 bytes]  passed 
  check(boolean, java.lang.String) ...
  Caution: Not checking body of anonymous 
class (subclass of Rollback)
                  new Rollback() {
    [0.103 s 12967928 bytes]  passed


The moment of TCK!

Success! ESC/Java2 has proved that the SAMS Reference Implementation is correct! Who needs the TCK anymore?

Do not forget that the tool is only in alpha version! In order to see that the reference implementation is really correct, change the implementation a bit:

public String getText() {
  return "foo";

The verdict of ESC/Java2: getText() ...
Warning: Postcondition possibly not established 
(Post)   }
Associated declaration is "src/javax/sams/messaging/sms/", 
line 57, col 6:
             ensures  _text_set ==> \result == _message_text;
Execution trace information:
    Executed return in "src/com/nokia/sams/messaging/sms/", 
  line 46, col 4.


Fine! The inserted bug has been caught!

But if the implementation is changed in the following way:

public String getText() {
  return messageText + "foo";

ESC/Java2 gives a false positive answer: getText() ...
    [0.381 s 13123600 bytes]  passed

And this is where we can continue writing module and functional tests...


We have tried to use JML [1] along with ESC/Java2 [2] to specify the behaviour of some extremely simple methods defined by JSR212 (SAMS). Java programmers can become familiar with JML pretty fast, as it operates with well-known concepts (pre- and post-conditions, invariants, representation functions, annotation, etc.) and stay as close as possible to Java syntax and semantics. JML is a great tool for precisely documenting and specifying the behaviour of Java applications.

Potentially, JML is the starting point of static verification of Java programs. Or more precisely, it might be. Although ESC/Java2 is a promising tool, unfortunately it is not industry ready yet, and there are no other tools that can superannuate module and functional testing by proving the correctness of Java programs.

And yes, test, as you cannot prove!

[Jump to top]


[1] JML Home Page:

[2] ESC/Java2:

[3] Java Community Process:

[4] JSR 212: Server API for Mobile Services:

[5] SAMS RI: jsr212 ri j2ee v11 installer

[6] SAMS TCK: jsr212 tck j2ee v11 installer