Spill — A logic language for writing testable requirements specifications

A requirements specification is the first formal description of a program. Formal methods of program construction can be practically useful only when the requirements specification can be shown to be adequate. This must be done by informal means: inspection and testing. Current specification languages do not easily support both inspection and testing. We propose a specification language, Spill, which has been designed with the express purpose of providing such support. Our language is based on the ideas of logic programming, and can be thought of as both an extended and a restricted version of pure Prolog. A specification written in Spill can be read as a declarative, precise description of the properties of the specified object. The description can be used as a starting point in the formal derivation of a program. At the same time the specification is testable — it can be treated as a program that allows the user to test whether the object so described would indeed have the desired properties, i.e., whether the formal specification corresponds to the intuitively-understood intentions