We have described a specification methodology for interface behaviors based on a message-based paradigm. An important feature of the methodology is that specifications can be designed without needing access to state information. A behavior specification for a message is a post-condition that distinguishes between normal and abnormal termination as well as its effect on subsequent messages vis-a-vis their pre-condition being satisfied or not. This supports the explicit (extensional) specification of the normal traces of an interface. A simple specification language, IBDL, is defined embodying the main ideas of the methodology. Specifications at the client level using normal/abnormal as well as at the server level using the enables/disables constructs can be given. The use of this methodology for validating sequence testing of implementations is also developed.
Even though the specification method is quite powerful and expressive, specifying certain behaviors can be tedious. We are investigating the use of message sequence axioms to simplify message sequences. Consider an example of a Stack interface. With the proposed methodology, one has to write a complex formula on the prefix of a sequence just to specify that a Pop message is enabled only if the number of Push messages is greater than the number of Pop operations in the prefix. A simpler specification would be to specify that a Pop message will cancel the latest Push message in the prefix, thus simplifying a message sequence. Such a rule, combined with a specification for Push that it enables a Pop, can completely define the behavior of the Stack interface. We are developing conditions on such rules on message sequences for specifications so as to keep the specification simple.
The proposed methodology as well as IBDL do not support explicit specifications of inheritance, an important concept in object-oriented languages as well as in interface languages. Inheritance is also supported in many interface languages including [3]. We would like to ensure that some form of behavioral subtyping [9,1] is achieved using the specifications as opposed to the syntactic subtyping that interfaces have. The expression language used in IBDL is restrictive in that it only allows specification of fully deterministic systems. But for top-down design, non-deterministic specifications and constructs may have to be supported. This may be useful for behavioral subtyping where the subtype has more specific (deterministic) behavior than the supertype. We have some preliminary ideas on this and are working on incorporating those into IBDL in such a way that it remains testable. We have worked out the formal denotational semantics of IBDL, which will be presented in a separate paper.