SPILL - A LOGIC LANGUAGE FOR WRITING TESTABLE REQUIREMENTS SPECIFICATIONS

A requirements specification is the first formal description of a prog ram. 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 s pecification languages do not easily support both inspection and testi ng. We propose a specification language, Spill, which has been designe d 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 t ime the specification is testable - it can be treated as a program tha t allows the user to test whether the object so described would indeed have the desired properties, i.e., whether the formal specification c orresponds to the intuitively-understood intentions. (C) 1997 Elsevier Science B.V.