This paper describes our experience specifying, implementing, and validating a record-oriented text editor similar to one discussed in [7]. Algebraic axioms served as the specification notation; and the implementation was tested with a compiler-based system that uses the axioms to test implementations with a finite collection of test cases. Formal specifications were sometimes difficult to produce, but helped reveal errors during unit testing. Thorough exercising of the implementations by the specifications resulted in few errors persisting until integration.

Abstract DAISTS (Data Abstraction Implementation, Specification and Testing System)1 is a compiler tool‐base for program development. The compiler combines an automated ‘oracle’, which checks consistency conditions derived from algebraic specifications of modules, with run‐time routines that judge the quality of a user's test data according to statement and expression coverage criteria. This paper describes some of the implementation techniques used in DAISTS.

A compiler-based system DAISTS that combines a data-abstraction implementation language (derived from the SIMULA class) with specification by algebraic axioms is described.The compiler, presented with two independent syntactic objects in the axioms and implementing code, compiles a "program" that consists of the former as test driver for the latter.Data points, in the form of expressions using the abstract functions and constant values, are fed to this program to determine if the implementation and axioms agree.Along the way, structural testing measures can be applied to both code and axioms to evaluate the test data.Although a successful test does not conclusively demonstrate the consistency of axioms and code, in practice the tests are seldom successful, revealing errors.The advantage over conventional programming systems is threefold:(1) The presence of the axioms eliminates the need for a test oracle; only inputs need be supplied.(2) Testing is automated: a user writes axioms, implementation, and test points; the system writes the test drivers.(3) The results of tests are often surprising and helpful because it is difficult to get away with "trivial" tests: what is not significant for the code is liable to be a severe test of the axioms, and vice versa.