DEF/specification

Similar terms and concepts requirement specification, requirement, model

Definition

DEF/specification

An expression in some →formal specification language stating some properties of an →artefact.

Explanation

• Formal Methods
• →specification language

Relations with other concepts

An artefact is called an implementation of a →specification if it has the stated →properties.

Pragmatics

In the early years of program correctness, specifications were simple and understandable, but not very realistic.

The output is the square of the input.

1. This specification abstracts from time. How long may such a computation take? Does a program that first waits for several thousand years and then computes the correct result satisfy this specification?
2. It also abstracts from memory limitations. A program that uses INTEGERs can never fulfil this specification. If it uses a representation that alllows unbounded numbers, there is still the bounded working memory of the execution mechanism.
3. Last, but not least, it abstracts from the execution mechanism and its resources. Without electricity, nothing can be computed at all.

A more realistic specification would be:

Provided there is electricity, a working execution mechanism and enough memory, provided the input is less than sqrt(maxint), after n milliseconds the output will be the square of the input.

Realistic specifications often consist of an assumption A and a commitment C: an artefact has to be an implementation of C only als long as its envronment guarantees A.

Examples

As a very elementary example, consider a three-minute switch as found in, for instance, hotel corridors, i.e. “a switch which switches itself off three minutes after it is switched on”. This description yields, however, only a rather vague picture, which may even be different for different people. Therefore one may propose a formal specification along the following lines, to serve as a contract with the client.

FORALL t: Time. 
	(FORALL t’: [t, t+3 min]. power_in(t’, 220V)) =>
		((EXISTS s: switch. pressed(s, t)) => (FORALL t’: [t, t+3 min]. power_out(t’, 220V))) 
	AND (power_out(t, 220V) => (EXISTS s: switch, t’:[t-3min, t]. pressed(s, t’)))

One may observe 3 issues here.

1. The properties are given in terms of some ‘external behaviour’. In such a specification the internal structure of the ‘box’ is not relevant.
2. Provided that the reader understands the notation, predicate logic is →a good language for such specifications, as it is a formalisation of natural language. There are numerous other specification formalisms, some of which admit more elegant formalisations, for instance differential equantions for dynamic systems, but they are basically all specialisations of predicate logic.
3. Apart from a universal quantifier over time, the example specification consists of two parts, separated by a =>, viz. an assumption which requires certain properties of the environment, and a commitment for the device itself. Specifications which require nothing of the environment are hardly imaginable, but many specification formalisms tend to keep in particular many of these implicit, together with the overall universal quantification(s).

Open questions

{{{open}}}

---

This is a definition from Taxonomy of Computer Science (Hanno Wupper et al. 2008).