An Ada-compatible specification language

This paper describes a notation for the formal specification of software packages. The main influences are the guarded commands of Dijkstra and the Algebraic Semantics of Guttag. However, a novel operator denoted by % is introduced, which allows algorithms to be abstracted in a specification, thereby creating a true specification language rather than another higher level language. The notation, called ADL/1, is designed to be used in conjunction with ADA but is equally suitable for other languages, and has been used for real time software written in Assembler and in a PASCAL-like language.