The proposed specification method is similar in spirit to the trace based specification approach of [8]. However, there are two crucial differences. Firstly, our approach is more structured in that semantics is associated with each message explicitly rather than merely giving rules to describe legality of traces. One of the problems with the approach in [8] is that exceptions cannot be specified. This is a severe restriction in practice as it is common for servers to raise exceptions when a message is received whose pre-condition is not satisfied in the current state, and subsequently, continue with other messages. Clients that send such a message are in a position then to handle such exceptions raised by the server and continue. In the trace-based specification approach in [8], such behavior will not be allowed because a trace with a message whose pre-condition is not satisfied is considered illegal. In contrast, the proposed methodology captures this by characterizing the result of a message to be abnormal in case the pre-condition for a message is not satisfied, and allows both the client as well as the server to continue their respective operations, probably after taking some corrective measure.
ObjLog [2] is a language based on trace model for object-oriented analysis and design. It does not use states explicitly for specification, but requires selector services that return values from the state to give specifications of updates. It uses transition equations to specify properties of updates. It is unclear how updates whose behavior is affected by other updates much before it (as in the queue example below) can be specified in ObjLog. It might be possible to use transition equations for that purpose, but we believe the resulting specifications will be difficult to develop as well as understand. In the proposed methodology, operators on sequences of messages are explicitly introduced for this purpose.
Borneo [12]
is a language designed for low-level specification of message
behaviors of OMG's IDL using the ADL framework [13].
The main problem with Borneo is that if the interface
does not expose any state, the only way to specify the interface
behavior is to use the auxiliary definitions, akin to coming up
with a crude implementation. This blurs any distinction between
a specification and an implementation, thus making the specification
as vulnerable to having bugs as the implementation is.
The proposed methodology does not
suffer from this limitation. Further, the key ideas of our
methodology can be easily adapted into the ADL family of
languages and in fact, we are working on incorporating them
into extending ADL/C++.
Languages based on Algebraic methodology have long been used for specifications. IBDL can be easily translated into any of those languages. But the purpose of IBDL is to give programmers/designers using interface languages, a simpler specification language with straightforward semantics, unlike algebraic specification languages which are usually based on equational theories. Algebraic languages, like Larch/CORBA [11] are quite powerful and general in that almost any computable function can be specified. IBDL on the other hand, is a less powerful language with a few reasonably easy-to-understand new concepts. As demonstrated by the ADL [13] project, despite the simplicity, these methodologies seem to be adequate for specifying many practical problems. Also, this simplicity and the familiar look-and-feel of the specification language seems to encourage practitioners to write specifications at least for some critical portions of their code.
IBDL also provides flexibility to a designer of incrementally specifying behavior at different levels of detail at different stages of interface design. As a start, only normal and abnormal clauses for messages and exception conditions, if any, raised by them can be specified. This can be followed by specifying enable and disable clauses once interaction among messages is analyzed. Subsequently, interpretations can be given once the design and the behavior of messages are finalized.
The other aspect of IBDL that is different from other methodologies
is that states need not be explicitly
modeled, instead observer methods give the ability to get
properties of states.
State however comes up in the form of
history of messages received, but users never need explicitly
specify the state transformation after a message; it
is simply defined as extending the previous history by
the current message.
To see this, consider the LARCH/CORBA specification for a
PrinterQueue interface as given in [11].
interface PrinterQueue {
const int MAX_QUEUE_SIZE 20
uses PrinterQueueTrait(PrinterQueue for PQ);
initially self' = empty;
void enqueue(in int id) raises (QUEUE_FULL) {
requires true;
modifies self;
ensures if len(self^) = MAX_QUEUE_SIZE then
raise(QUEUE_FULL) /\ self' = self^
else self' = append(self^, id);
}
int dequeue() {
requires ~isEmpty(self^)
modifies self;
ensures
self' = tail(self^) /\ result = head(self^);
}
int size() {
ensures result = len(self^);
}
}
There are two main differences between the above specification
and an IBDL specification for a similar interface given in section 2.
Firstly, there is (an abstract) representation of the object in terms
of self (see page 11 of [11]).
The specification for enqueue (and
dequeue) is given as their effect on the
object to say that the new value of self is same as
appending (and removing the head of) the old value of self.
In contrast, in the IBDL specification, this behavior
is done in terms of messages by specifying that a dequeue
operation can be performed after an enqueue; if there
have been equal number of enqueue and dequeue messages,
then a dequeue cannot be performed. This second requirement is captured
above in LARCH/CORBA by the pre-condition (requires clause) using
the state of the queue object.
In algebraic methods, recursion is used extensively which practitioners
often find difficult to understand.
In IBDL, we
support a very restricted form of recursion using the @
operator and to some extent, the # and param operators.
We believe this will make it easier to develop and understand
specifications.
We can certainly extend the language to
include more operations on sequences to enhance its power, but
we purposely chose not to do it to keep the semantics simple.
The other very important difference between IBDL and other languages mentioned is the capability to test implementations against specifications. We have come up with a scheme for this using IBDL and we are actively building a tool to support this scheme. To the best of our knowledge, there are no specification-based sequence testing/validation tools using any of the other languages discussed above.