The JML and JUnit Way of Unit Testing and its Implementation
				  by
		  Yoonsik Cheon and Gary T. Leavens

			       Abstract

Writing unit test code is labor-intensive, hence it is often not done
as an integral part of programming.  However, unit testing is a
practical approach to increasing the correctness and quality of
software; for example, Extreme Programming relies on frequent unit
testing.

In this paper we present a new approach that makes writing unit tests
easier.  It uses a formal specification language's runtime assertion
checker to decide whether methods are working correctly; thus code to
decide whether tests pass or fail is automatically produced from
specifications.  Our tool combines this testing code with hand-written
test data to execute tests.  Therefore, instead of writing testing
code, the programmer writes formal specifications (e.g., pre- and
postconditions).  This makes the programmer's task easier, because
specifications are more concise and abstract than the equivalent test
code, and hence more readable and maintainable.  Furthermore, by using
specifications in testing, specification errors are quickly
discovered, so the specifications are more likely to provide useful
documentation and inputs to other tools.  In this paper we describe an
implementation using the Java Modeling Language (JML) and the JUnit
testing framework, but the approach could be easily implemented with
other combinations of formal specification languages and unit testing
tools.

Keywords: Unit testing, automatic test oracle generation, testing tools,
runtime assertion checking, formal methods, programming by contract, 
JML language, JUnit testing framework, Java language.


2000 CR Categories:
D.2.1 [Software Engineering]
        Requirements/ Specifications --- languages, tools, JML;
D.2.2 [Software Engineering]
        Design Tools and Techniques --- 
                computer-aided software engineering (CASE);
D.2.4 [Software Engineering]
        Software/Program Verification --- Assertion checkers,
                class invariants, formal methods, programming by contract,
                reliability, tools, validation, JML;
D.2.5 [Software Engineering]
        Testing and Debugging --- Debugging aids, design, monitors, 
                testing tools, theory, JUnit;
D.3.2 [Programming Languages]
        Language Classifications --- Object-oriented languages;
F.3.1 [Logics and Meanings of Programs]
        Specifying and Verifying and Reasoning about Programs ---
                Assertions, invariants, pre- and post-conditions,
                specification techniques.

Copyright (c) 2004 by Yoonsik Cheon and Gary T. Leavens.