A declarative approach to software requirement specification languages

The authors present a declarative approach to a software requirement specification language which is able to specify requirements for software systems under the emerging methodology. The language presented is based on first-order predicate logic, but augments standard first-order logic by introducing hierarchies and exceptions to its generalizations, to allow for a more natural description of the problem domain. The proposed requirement language is valid and can be determined to be internally consistent. A theorem prover that can interpret the language is implemented.<>