A Tool for Writing and Debugging Algebraic Specifications

Despite their benefits, programmers rarely use formalspecifications, because they are difficult to write and theyrequire an up front investment in time. To address these issues,we present a tool that helps programmers write anddebug algebraic specifications. Given an algebraic specification, our tool instantiates a prototype that can be used just like any regular Java class. The tool can also modifyan existing application to use the prototype generatedby the interpreter instead of a hand-coded implementation.The tool improves the usability of algebraic specificationsin the following ways: (i) A programmer can "run" an algebraicspecification to study its behavior. The tool reportsin which way a specification is incomplete for a client application.(ii) The tool can check whether a specification anda hand-coded implementation behave the same for a particularrun of a client application. (iii) A prototype can beused when a hand-coded implementation is not yet available.Two case studies demonstrate how to use the tool.