UP

Belorussian translation

Formal Specification Languages

Model Oriented

Algebraic

Process Model

Logical

Constructive

Broad Spectrum

Model Oriented

"model oriented" specification languages are so called because they are support the specification of systems by construction of a mathematical model of the system. In a sense any formal specification can be thought of as providing a mathematical model of a system so it may be helpful to expand on this.

It is characteristic of model oriented languages that the model of the system is given by describing the state of the system, together with a number of operations over that state. An operation is a function which maps a value of the state together with values of parameters to the operation onto a new state value.

A model oriented language is typically used by describing in detail specific mathematical objects (e.g. data structures or functions) which are structurally similar to the required computer software. It is then permitted to transform these mathematical objects, during the design and implementation of the system, in ways which preserve the essential features of the requirements as initially specified.

Probably the most widely known model oriented specification languages are VDM-SL, the specification language associated with VDM, the Vienna Development Method, and the Z specification language.

Algebraic

Algebraic specification languages are used to specify information systems using methods derived from abstract algebra or category theory.

Abstract algebra is the mathematical study of certain kinds or aspects of structure abstracted away from other features of the objects under study. Algebraic methods are beneficial in permitting key features of information systems to be described without prejudicing questions which are intended to be settled later in the development process (implementation detail).

The best known algebraic specification language is probably OBJ, which is related to clear. Clear is itself a system for specification "in the large" by combining together specifications in ways which are independent of the "institution" in which the specifications are expressed. i.e., clear is an abstract system for modular specification generic over a wide range of specification notations.

Process Model

Specification languages for describing concurrent systems are sometimes implicitly based on a specific (though perhaps implicit) model for concurrency. In these languages expressions denote processes, and are built up from elementary expressions which describe particularly simple processes by operations which combine processes to yield new potentially more complex processes.

Possibly the best know process modelling languages are CSP and CCS.

Logical

This class of specification languages consists of those languages which are closest to (or identical with) logical languages not originally intended for specifying informations systems. The use of these languages reflects the belief sometimes held that formal specification is special only in its use of formal notations, not in the kinds of logic or mathematics which it employs.

A distinction may be drawn between two traditions within this group. In some cases it is advocated that a formal logic be used for specification in a fairly unrestrained axiomatic manner. In other cases it is advocated that specifications be undertaken using only conservative extensions over some sufficiently rich formal mathematical baseline. In the second tradition the kind of logical system adopted as baseline will need to amount to a logical foundation for mathematics, in the former case the weaker constraints on the means of specification means that a logical system which falls short of providing a foundation for mathematics may be acceptable.

Of the former kind, first order logic is the classic example. Of the latter, first order set theory has sometimes been adopted, but more frequently some kind of logical type theory (e.g. HOL) or typed set theory. Many different type theories have been used (see PTS for a systematic account of many logical type theories), often constructive (e.g. NUPRL) rather than classical.

The the Z specification language is at bottom a typed set theory which could therefore have been positioned as a foundational specification language were it not that its use has predominantly been advocated in a free-wheeling axiomatic manner and no rules are enunciated to permit specification by conservative extension. The support for Z provided by the Lemma 1 proof tool ProofPower includes the necessary features to support its use for specification and proof using only conservative extension. A seemingly free-wheeling axiomatic style implemented in a strictly conservative way is also supported by HOL.

Constructive

Theoretical work on constructive logical systems, usually type theories (see PTS), has become widespread since Martin Löf claimed special relevance to computing for his Intuitionistic Type Theories.

Constructive mathematics is particularly concerned with realisability (in an informal as well as a technical sense). Whereas in classical mathematics the notion of a function is very broad, and includes many functions which could never be evaluated by a computer, constructive mathematics concerns itself only with functions which are effectively computable.

In constructive logics the ways of demonstrating the existence of functions satisfying some property (which may be thought of as the specification of a program) are restricted. The result of this restriction is that from any proof of the consistency of a specification, a value satisfying the specification can be extracted. In principle therefore the specify/implement/verify post hoc verification paradigm may be modified when using a constructive logic to specify/verify-consistency/extract-implementation, where the last stage is completely automatic. This principle has been demonstrated by proof tools for constructive logics, for example the NUPRL system.

Broad Spectrum

The label broad spectrum is used to describe specification languages which are suitable for use at all stages in the development of an information system from conception through specification, design, implementation and verification.

It is used here to cover not only that kind of language, but also languages which are hybrid relative to the above classification for any reason at all. Two examples of such hybrid notations are RSL the specification language associated with the RAISE development methods, and LOTOS, a specification notation intended originally for the specification of communication protocols. RAISE synthesises the model oriented, process model and algebraic paradigms, while LOTOS combines process model and algebraic methods.


UP HOME © RBJ created 1995-05-24 modified 2011-08-06