Errors in algebraic specifications and an experimental mutation testing tool

There is an increasing trend towards more formality in the development of specifications of software systems in order to reduce the likelihood of errors as early as possible in the development process. The algebraic approach to specification, with its equational form, leads to the added advantage of executability via the process of term rewriting. Nevertheless, erroneous algebraic specifications can still be developed. As evidence of possible errors, the algebraic specifications produced by students have been analysed and the results are presented. The paper describes OBJTEST, a prototype testing system for algebraic specifications. The two principal facets of the system are the user-guided automatic generation of sets of test expressions from a specification, and then the use of these test expressions in mutation testing of the given specification. Some preliminary experience with the system is reported