| | | CoFI Origins |
Algebraic specification is one of the most extensively-developed approaches in the formal methods area. The most fundamental assumption underlying algebraic specification is that programs are modelled as many-sorted algebras consisting of a collection of sets of data values together with functions over those sets. This level of abstraction is commensurate with the view that the correctness of the input/output behaviour of a program takes precedence over all its other properties. Another common element is that specifications of programs consist mainly of logical axioms, usually in a logical system in which equality has a prominent role, describing the properties that the functions are required to satisfy--often just by their interrelationship.
This property-oriented approach is in contrast to so-called model-oriented specifications in frameworks like VDM [25] which consist of a simple realization of the required behaviour. However, the theoretical basis of algebraic specification is largely in terms of constructions on algebraic models, so it is at the same time much more model-oriented than approaches such as those based on type theory (see e.g. [45]), where the emphasis is almost entirely on syntax and formal systems of rules, and semantic models are absent or regarded as of secondary importance.
The past 25 years has seen a great deal of research on the theory and practice of algebraic specification. Overviews of this material include [1][6][10][30][50][51][54]. Developments on the foundational side have been balanced by work on applications, but despite a number of success stories, industrial adoption has so far been limited.
The current proliferation of algebraic specification languages is seen as a significant obstacle to the dissemination and use of these techniques. Despite extensive past collaboration between the main research groups involved and a high degree of agreement concerning the basic concepts, the field has given the appearance of being extremely fragmented, with no de facto standard specification language, let alone an international standard. Moreover, although many tools supporting the use of algebraic techniques have been developed in the academic community, none of them has gained wide acceptance, at least partly because each tool uses a different specification language.
The dozens of algebraic specification languages that have been developed all support the basic idea of using axioms to specify algebras, but differ in design choices concerning syntax (concrete and abstract) and semantics.
Why not agree on a common framework?
This was the provocative question asked at a WADT/Compass meeting in Santa Margherita, 1994. At least the main concepts to be incorporated were thought to be clear--although it was realized that it might not be so easy to agree on a common language to express these concepts.
| | | CoFI Origins |