Combining Testing with Formal Specifications: A Case Study

1 May 1983

journal article
Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering

Vol. SE-9 (3) , 328-335
https://doi.org/10.1109/tse.1983.236869

Abstract

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.

Keywords

This publication has 3 references indexed in Scilit:

Data Abstraction, Implementation, Specification, and Testing
ACM Transactions on Programming Languages and Systems, 1981
Mathematical specifications
ACM SIGPLAN Notices, 1980
Testing programs with finite sets of data
The Computer Journal, 1977