Issue No. 03 - May (1983 vol. 9)
P.R. McMullin , Applied Physics Laboratory, The Johns Hopkins University
This paper describes our experience specifying, implementing, and validating a record-oriented text editor similar to one discussed in . 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.
testing, Data types, specification
J.D. Gannon, P.R. McMullin, "Combining Testing with Formal Specifications: A Case Study", IEEE Transactions on Software Engineering, vol. 9, no. , pp. 328-335, May 1983, doi:10.1109/TSE.1983.236869