Formal and Abstract Software Module Specifications -
A Survey

Mr. Yabo Wang

Software Engineering Research Group
CRL, McMaster University,
Hamilton, Ontario, Canada L8S 4K1


Some modern software systems have grown to such a big size and complex structure that no one person (or even a team) can finish the development of a system in a few weeks, or months. To attack such a big and complex software development problem, nearly every software design methodology is based ont he decomposition of large, complex systems into smaller, simpler modules. In design, development, and maintenance of such large and complex software systems, formal and abstract module specification plays an increasingly important role.

Among various formal and abstract module specification techniques, the abstract model based techniques specify software modules by first constructing abstract models, usually some commonly used and well understood data structures, and then by specifying modules properties in terms of models; algebraic techniques view abstract data values and operations implemented by a module as forming absstract algebra and specify the module by presenting such algebra; the trace based techniques treat software modules as finite state machines and describe the modules' behaviour in terms of their external observable properties - the effects of module access programs; and process based techniques model a system as a set of interconnected processes and specify such a system by describing the behaviour of each process and the communication channels among the set of processes.

This report surveys the above four classes of module specification techniques and provides a comparison on the advantages and disadvantages of each specification technique.