These requirements describe a specification validation tool, called the "Spec Validator". The purpose of the tool is to allow the developer of a specification to test the specification incrementally, as it is being developed. The specification is written as an object/operation model, with formal behavior defined as preconditions and postconditions on the operations.

The testing of the specification entails providing sample inputs and outputs to the specified operations. The test inputs are "plugged in" to the precondition, which is evaluated to produce its boolean result. If the precondition is true, the test outputs are plugged into the postcondition to produce its boolean result. The user then examines the evaluated results to confirm that the precondition and postcondition evaluate as expected.

For a test case of correct behavior, the precondition and postcondition should both evaluate to true. For a test case with invalid inputs, the precondition should be false, and the postcondition nil. A test case can reveal a flaw in the specification if the user expects the results to be true, but the evaluation says otherwise. For example, a postcondition error is detected when a test case has outputs that are known to be correct, but the postcondition evaluates to false.

The functional requirements of the Spec Validator present examples of typical usage. The examples illustrate how the Validator can be a productive part of specification development.