3 Comparison

A simple form of interface checking is already routine in most systems design projects using some form of high level programming language for describing components. It is common practice to do type-checking across separately compiled components (the C header file mechanism is an example which makes it possible to do a simple check of interface consistency). However, the idea of type checking common interfaces can be taken much further [DET84,GwSGJ⁺93]. The LCLint tool [DET84] is a nice example of how extended checking can be useful for revealing bugs before going to full scale testing.

Most modern high-level languages have a sophisticated module concept for handling a hierarchical library, the package concept in VHDL [VHD88] and the interface/class constructs in Java [AG96] are good examples. Although these module concepts are useful they only represent a small step towards what is feasible in terms of checking interface consistency. By documenting essential properties of an interface in formal notation, such as the interface predicates defined above, it becomes possible to exhaustively check interface consistency as described in the position section (and the references mentioned in that section).

In my view there are a number of interesting issues that need further work including:

1.

Experimentation with the expressive power of the notation used for documenting interfaces. It is not clear that notations which are very expressive from a theoretical viewpoint are also the most useful in practice. An example is LCLint [DET84] which is a tool that practioners find very useful even if it is used in a very limited way.

2.

Timing is a key issue in many interfaces, and it would of course be very useful to check timing properties of interfaces. There is work on formalizing timing diagrams e.g. in [PG97,CHR91], but I do not think that the final words on this issue have been said.

3.

Tool support is important for any approach that wants to gain practical acceptance. Tremendous progress has been made over the past few years in model-checking tools, see e.g., [K.L93]. However, it is not clear that such finite state models are adequate for the more open ended formalism needed to document interfaces. Personally, I have experimented with tools based on general purpose theorem proves which makes it possible to check interfaces including infinite domains like integers (without bounds) and arrays without fixed index ranges [SM95].