Languages for the specification of software

A variety of specification languages exist that support one or more phases of software development. This article emphasizes languages that support the functional phase, i.e., languages that can be used to define the observable behavior of a system. The languages surveyed include Z, Prolog, SF, Clear, Larch, PAISLey, Spec, CSP, SEGRAS and BagL. The article divides the languages into four major categories based on the way the language specifies the external behavior of the system and on the ability of the language to specify concurrent systems. Each language section includes a discussion of the constructs of the language, a specification of a problem in the language, and an evaluation of the language. The article is intended to acquaint the reader with a wide range of functional specification languages.