Demonstration of JML Tools
				  by
	   Gary T. Leavens, Yoonsik Cheon, and David R. Cok

			       Abstract

The Java Modeling language (JML) is a behavioral interface
specification language tailored to Java.  This demonstration presents
some of the basic tools for generating and browsing documentation,
runtime assertion checking, and unit testing.

Keywords: specification languages, runtime assertion checking,
documentation, tools, formal methods, program verification,
programming by contract, Java language, JML 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,
                testing tools, theory;
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.