This Article 
 Bibliographic References 
 Add to: 
Testing the Completeness of Specifications
May 1989 (vol. 15 no. 5)
pp. 526-531

A system is described that tests for the completeness of axiomatic specifications of abstract data types. For testing, the system generates a set of test cases and an implementation of the data type from the specifications. The generated implementation is such that if the specifications are not complete, the implementation is not complete, and the behavior of all of the sequences of valid operations on the data type is not defined. This implementation is tested with the generated test cases to detect the incompleteness of specifications. The system is implemented on a VAX system running Unix.

[1] U.S.D. Defense,Reference Manual for the ADA Programming Language. New York: Springer-Verlag, 1983.
[2] J.H. Weber, C. de Vroedt, and D.E. Boekee, "Bounds and constructions for binary codes of length less than 24 and asymmetric distance less than 6,"IEEE Trans. Inform. Theory, submitted for publication.
[3] E. Chang and S. N. Zilles, "Abstract data types in Euclid," inNotes on Euclid, W.D. Elliot and D.T. Barnard, Eds., Comput. Syst. Res. Group, Dep. Comput. Sci, Univ. Toronto, Toronto, Ont., Canada, Tech. Rep. 82.
[4] O. J. Dahl, B. Myhrhaug, and K. Nygaard, "The SIMULA 67 common base language," Norwegian Comput. Cen. Oslo, Norway, Pub. S-22, 1970.
[5] J. Gannon, P. McMullin, and R. Hamlet, "Data-abstraction implementation, specification and testing,"ACM Trans. Program. Lang. syst., vol 3, no. 3, pp. 211-223, July 1981.
[6] N. Gehani, "Specifications: Formal and informal--A case study,"Software Practice Experience, vol. 12, pp. 433-444, 1982.
[7] J. Goguen and J. J. Tardo, "An introduction to OBJ: A language for writing and testing formal algebraic program specifications," inProc. Specification Reliable Software, 1979, pp. 170-189.
[8] J. V. Guttag and J. J. Horning, "The algebraic specifications of abstract data types,"Acta Inform., vol. 10, pp. 27-62, 1978.
[9] J. V. Guttag, "Notes on type abstraction (version 2),"IEEE Trans. Software Eng., vol. SE-6, pp. 13-23, Jan. 1980.
[10] G. Huet and D. C. Oppen, "Equations and rewrite rules," inFormal Language Theory, Perspectives and Open Problems, R. V. Book, Ed. New York: Academic, 1980, pp. 349-397.
[11] P. Jalote, "Synthesizing implementations of abstract data types from axiomatic specifications,"Software: Practice and Experience, vol. 17, no. 11, pp. 847-858, Nov. 1987.
[12] P. Jalote and M. Caballero, "Automated testcase generation for data abstraction," inProc. COMPSAC 88, Chicago, IL, Oct. 1988, pp. 205-210.
[13] R. A. Kemmerer, "Testing formal specifications to detect design errors,"IEEE Trans. Software Eng., vol. SE-11, pp. 32-43, Jan. 1985.
[14] D. E. Knuth and P. E. Bendix, "Simple word problems in universal algebra," inComputational Problems in Abstract Algebra, J. Leech, Ed. New York: Pergamon, 1970, pp. 263-297.
[15] B. H. Liskov and S. N. Zilles, "Specification techniques for data abstractions,"IEEE Trans. Software Eng., vol. SE-1, pp. 7-19, Mar. 1975.
[16] B. Liskovet al., "Abstraction mechanisms in CLU,"Commun. ACM, vol. 20, pp. 564-576, Aug. 1977.
[17] D. A. Musser, "Abstract data type specification in the AFFIRM system,"IEEE Trans. Software Eng., vol. SE-6, pp. 24-32, Jan. 1980.

Index Terms:
completeness testing; axiomatic specifications; abstract data types; test cases; VAX system; Unix; conformance testing; data structures; program testing.
P. Jalote, "Testing the Completeness of Specifications," IEEE Transactions on Software Engineering, vol. 15, no. 5, pp. 526-531, May 1989, doi:10.1109/32.24701
Usage of this product signifies your acceptance of the Terms of Use.