"Do as I Say, Not as I Do"

John McCreight 2006


Abstract

Software specifications can be useful in providing crucial information about the behavior of software to programmers, system designers, and other stackeholders. Specifications are useful in establishing the intent of code, which then further facilitates the design of tests based on intent. Carrying the idea further, a formal way of creating specifications can even permit automated test generation if the specifications are detailed enough. With some additional effort, it is also possible to generate useful test data, which almost frees programmers from writing test software completely.

This paper introduces the Java Modeling Language (JML), a formal Behavioral Interface Specification Language (BISL) for Java. JML specifications are provided annotations similar to Java code, granting the ability to create both tests and documentation as nesscessary. Further, this paper examines the current generation of tools implementing JML, and proposes an approach to implementing the for_example clause already present in the JML specification such that it be usable in testing.