Motivating Key Ideas using Examples

In interface declarations, the intention usually is not to expose the state. This can make it difficult to write specifications using pre- and post-conditions (see the bank account example below). However, one can get a fair idea about the state of the object looking at the return values of observers. The main idea is to partition the messages of an interface into update and observer¹ operations, and specify how an update message sent will change the behavior of other update and observer operations without explicitly using the state. This includes specifying if subsequent messages will behave normally or abnormally and what the return values, if any, would be.

Below by a series of examples, we will illustrate our methodology for writing interfaces and their behavior specifications. We also introduce (most of) the new constructs of the language one by one. The language IBDL is introduced fully in the next section with informal semantics.

We first introduce the enables and disables constructs along with simple interface declarations.

Consider the following example of a simple read-write object interface :

interface ReadWrite {
   void Write(int x);
   int Read();
   ReadWrite(); 
};

Here Write is the update message and Read is the only observer. ReadWrite is the constructor that creates objects of this type. If the state was exposed as a part of the interface, then it is easy to write the post-conditions for these two methods. Without access to state, however, a post-condition cannot be given.

Our approach to specification in these situations is to define sequences of messages, classify terminations of messages and specify the return values of the observers based on these sequences.

For the above example, this can be done as follows : The Read message should not be invoked until something is written using the Write operation, assuming initially the value stored is undefined. Similarly once a message Write(k) is sent for some integer k, subsequently a Read() message will succeed and its return value will be k until another Write message is sent. Here there is no explicit use of state in the specification, even though it can be observed using the observer operation Read.

This can be written formally in IBDL as follows. The complete syntax for IBDL is in the appendix.

specification ReadWrite {
   interface ReadWrite semantics {
      ReadWrite() { normal enables Write(x); }
      void Write(int i) {
         normal enables Read();
                interpretations   Read() = i;
      }
   }
}

Sometimes it is not possible to give complete specifications just by relating an update operation and its parameter values to subsequent messages. It is required to look at the behavior of the messages before the call to the update is made. We will introduce the ``@'' and the enabled operators here that can be used for this purpose. The ``@''operator is used to access the state prior to the message and the enabled operator is used to check the enabledness of a particular message without actually sending it.

Consider the following bank account interface :

interface Account {
   void    Deposit(int x);
   boolean ClearCheck(int x)
         raises InvalidAmount, NotEnoughFunds;
   Account(int acNum, int initialBalance);
};

The objective here is not to allow clients sending the ClearCheck message to access the balance. In practice also, it is typical for clearing houses not to have access to the balance when they try to clear a check. At the same time, we want to be able to specify that if there is not enough balance in the account, the ClearCheck operation is going to fail. The methodology is particularly geared towards these situations.

An IBDL specification for this interface is :

specification Account {
   interface Account semantics {
      Account(int acNum, int initBalance) {
         normal enables
            Deposit(x) if (x >= 0);
            ClearCheck(x) if (x >= 0 and
                               x <= initBalance);
      }

      void Deposit(int amount) {
         normal enables
            ClearCheck(amount + y)
                      if @enabled(ClearCheck(y));
      }

      boolean ClearCheck(int amount) {
         normal disables ClearCheck(z)
                    if @(not enabled(
                        ClearCheck(z + amount)));
         abnormal defined by 
                     raised(InvalidAmount) or
                          raised(NotEnoughFunds)
                     (amount < 0)
                         if raised(InvalidAmount)
      }
   }
}

The informal semantics of this interface can be given by the following rules :

1.

After creating a new object using the message Account(a, ib), a message Deposit(k) for any integer or ClearCheck(l) for any integer l such that and can be sent to that object.

2.

A message Deposit(k) with will always succeed because it is enabled immediately after the constructor and does not appear in a disables clause of any message.

3.

After a Deposit(k) message to an Account object returns normally, a message ClearCheck(l + k) would succeed by returning true if a ClearCheck(l) would have succeeded prior to the Deposit(k) message. Also, any message that would terminate normally prior to the Deposit(k), would remain so.

4.

If a message ClearCheck(k) terminates normally, a subsequent ClearCheck(l) would fail if ClearCheck(l + k) would have failed prior to it and all other messages would succeed only if they would do so prior to the ClearCheck(k) message. Otherwise, it should raise one of the two listed exceptions and if the InvalidAmount exception is raised, then the value of amount  should be less than 0.

In rules 2 and 3, the specification of the behavior of ClearCheck depends on its behavior prior to a Deposit or a ClearCheck respectively using the ``@'' operator to denote the state before the message.

A state-based specification for this interface would require the use of balance explicitly to specify the post-condition. One such specification in ADL/C++ using the state variable long balance of a C++ implementation of this interface is given in[17]. The reader will notice the dependence of the post-condition specification on the state variable balance, whereas our methodology uses only the messages of the interface and their parameters; it does not require the state information for writing specifications.

The above specification defines all possible sequences by specifying all the extensions of a given prefix that will guarantee normal behavior, assuming initially only the constructor is enabled. In that sense this is a constructive definition of all the normal traces (sequences of messages) for an object. As motioned earlier in the related work section, this is not the case with other trace specification methodologies such as in [8]. In these, one can only check for the validity of a given sequence of messages and value(s) returned, but cannot generate (in a straightforward manner) legal sequences.

Even the ability to look at the behavior of observers prior to an update message is not enough to describe the behavior fully in some cases. It may also be necessary to look at a message that was sent much earlier and its parameter values. For this, two new operators on sequences - param - to access the parameters of a particular message sent earlier and ``#'' - to count the number of times a particular kind of message sent, are introduced.

For example, consider an IBDL specification of an unbounded queue of integers :

specification Queue {
   interface Queue semantics {
      Queue() {
         normal enables Enqueue(x);
      }

      void Enqueue(int elem) {
         normal
           enables Dequeue();
           interpretations
             Dequeue() = param(#(Dequeue)+1,
                                  Enqueue, elem);
      }

      int Dequeue() {
         normal
           disables
             Dequeue() if (#(Dequeue) =
                           #(Enqueue));
           interpretations
             Dequeue() = param(#(Dequeue) + 1,
                                Enqueue, elem);
      }
   }
}

All the operations have their usual meanings and Queue is the constructor for queue objects. Following is the intuitive meaning of the above specification :

1.

When a queue is created using the Queue() message, only a message Enqueue(k), for any integer k, can be sent to the created Queue object.

2.

After a message Enqueue(k), a message Dequeue() will terminate normally. Its return value (the next element in the Queue) is the parameter to the i th occurrence of the Enqueue message if there are i - 1 occurrences of normal-terminating calls to Dequeue() so far (before this Enqueue message).

3.

Similarly, after the message Dequeue() is sent, a subsequent message to Dequeue() will succeed only if there are more Enqueue messages than Dequeue messages prior to that. Once again, the return value of an enabled Dequeue message is going to be determined same way as in the previous step.

The ``#'' operator counts the number of times a particular message is sent and terminated normally since the time of creation of the object (including this message). The param operator returns the value of a certain parameter to a message given a message name and the number of occurrence in the sequence of messages prior to this one. This all abnormal messages are ignored for counting purposes.

As the above example shows, sometimes it is also necessary to know how many times a particular message is sent and its corresponding parameters for giving a complete specification.

This particular example can be much simplified if we allow trace simplification rules, i.e., equations to specify that a dequeue message will cancel the first Enqueue message, immediately following the constructor, in the current sequence giving a new trace without either being present. This will be similar to incorporating some algebraic axioms as simplification rules into the language. We are currently investigating such an extension to the language.