Data-Abstraction Implementation, Specification, and Testing

Abstract

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.