Go backward to 2.2 Writing the Program Go up to 2 Using the Toolkit Go forward to 2.4 Compiling the Program

2.3 Asserting Conditions

While only the code explained in the previous section is required to make the program executable, we would like to make explicit that the program fulfils certain properties. The central property of above example is that there are exactly two messages contained in the network. We can state this as an assertion by rewriting class Prog as follows:

class Prog extends Program
{
  private int number;
  public int index;
  public Message msg;
  public boolean sent;
 
  public Prog(int i)
  {
    number = i; 
    msg = null;
    sent = false;
  }
 
  public void main()
  {
    if (number == 0)
      {
        out(0).send(new Msg(0));
        out(1).send(new Msg(1));
        sent = true;
      }
    GlobalAssertion assertion = new NumberOfMessages();
    for (int i = 0; i < 5; i++)
      {
        assert(assertion);
        index = in().select();
        msg = in(index).receive();
        out(index).send(msg);
        msg = null;
      }
  }
}

This code differs from the previous one by making index and msg public instance variables of class Prog and by introducing an boolean instance variable sent which is set by the program on node 0 to true when it has initialized the network. Furthermore, we reset the received message msg to null after it has been submitted again into the network.

When assert is called with an assertion a as its argument, it invokes the method a.assert(p) on the array of node programs p. The assertion may examine the published state of each program object (in our example, the contents of the public instance variables index, message, and sent). It may also investigate the contents of the attached channels (in, out) by calling the method getMessages which returns the array of messages contained in a channel (in the order in which they were sent). If the method returns false, execution is aborted with the error message returned by a.getText() (which is displayed in the foot line of the visualization window).

The assertion type NumberOfMessages is defined as a subtype of the DAJ type GlobalAssertion as shown below:

class NumberOfMessages extends GlobalAssertion
{
  int count;

  public String getText()
  {
    return "invalid number of messages: " + 
      String.valueOf(count);
  }

  public boolean assert(Program prog[])
  {
    if (!((Prog)prog[0]).sent) return true;
    count = 0;
    for (int j = 0; j < prog.length; j++)
      {
        Prog program = (Prog)prog[j];
        count += getMessages(program.out(0)).length;
        count += getMessages(program.out(1)).length;
        if (program.msg != null) count++;
      }
    return count == 2;
  }
}

The assertion says that, as soon as node 0 has signalled by its variable sent the initialization of the network, there must be exactly two messages in the network. A message may be either contained in some channel out(j), or, in a program's local variable msg.

When assert is called, it may rely on the fact that each program passed to it as its argument is either in the initial state, has terminated execution, or is blocked on a communication operation before the corresponding message was sent or received². This allows to formulate assertions about the state of the network in a comfortable way.

Appendix A contains a formal proof of this assertion.