The authors advocate the validation of designs through the use of formal specifications and the testing of those specifications. More specifically, validation is done by testing the consistency between executable requirement specifications, which state the nature of the problem formally and nonalgorithmically, and constructive specifications, which specify the design for a solution.

A simple example in which a UNIX directory identifier is the input and a flattened list showing the underlying tree structure of the directory is the output illustrates the technique. OBJ is used for the requirement specification, and the UMIST OBJ subset is used for the constructive specifications. Regularity and uniformity hypotheses, which are summarized in the paper, are used to choose test cases for the validation.

The conceptual basis for the paper is appealing, but the example is not. Some of the lack of appeal stems from minor problems, such as the choice of “1” to denote both a list variable and the number one. The resulting ambiguity, in the part of the requirement specification which states the directory must contain at least one root, illustrates the difficulty of attaining accurate formal specifications. The inadequacies of OBJ pose a more substantive problem. In particular, because of its strictly linear nature, OBJ is less comprehensible than the usual mathematical notation, which makes effective use of subscripts and superscripts. Also, the lack of powerful operators is a barrier to expressiveness. Because of this lack of expressiveness, the specifications given in the paper tempt me to join those who advocate the use of formal specifications but not the use of executable specifications. Nevertheless, the paper argues the benefits of early design-time testing convincingly enough to warrant encouragement of the search for executable specification languages that are more expressive and comprehensible.