A language for writing formal specifications, first described by R. M. Burstall and J. A. Goguen in 1977. The language provides a formalism for expressing a complex specification hierarchically as a combination of simpler ones. This formalism can be given a precise semantics using ideas familiar from algebra and category theory.