SPECIAL - A Specification and Assertion Language.
Luke Robinson, Olivier Roubine · Defense Technical Information Center (DTIC) · 1976
SPECIAL is a specification language developed in conjunction with the SRI methodology for design, implementation, and formal verification of software systems. Some of the language features are specific to the SRI methodology. Others, such as its non-procedural nature, concept of type, and aggregate data types, are generally useful for software specification and verification. A description of the features of the language is supplied, along with several examples of its use. The language has proved useful in the design of several large software systems, including an operating system. A discussion of the issues in the design of SPECIAL is presented, followed by a description of its features and some examples. (Author)