Design of a JML documentation generator
				  by
                             Arun Raghavan

			       Abstract

JML is a behavioral interface specification language designed to
specify Java classes and interfaces. In JML, a Java class or interface
inherits specifications from its superclass and/or
superinterfaces. JML specifications for a class or module can also be
refined or augmented in non-source files. As a result of this, the
complete specification for a class or interface may be split over
several files. To facilitate viewing of these specifications in a
user-friendly manner, some documentation tools are needed to combine
these specifications. This thesis gives a semantics of specification
inheritance and refinement and describes an implementation of JMLDoc
--- a tool for generating HTML pages from the specifications. It
combines specifications from inheritance and refinements and presents
the complete JML specification to the user.

Keywords: specification inheritance, refinement, browsable documentation
generation, HTML, combining specifications, semantics of specifications,
model-based specification, behavioral interface specification
language, behavioral subtyping, formal specification
languages, Eiffel, JML, Java.

2000 CR Categories:
D.2.1 [Software Engineering]
        Requirements/Specifications --- languages, tools, JML;
D.2.2 [Software Engineering]
        Design Tools and Techniques --- modules and interfaces,
        software libraries;
D.2.4 [Software Engineering]
        Software/Program Verification --- formal methods,
        programming by contract, tools, JML;
D.2.7 [Software Engineering]
        Distribution, Maintenance, and Enhancement --- documentation;
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) 2000 by Iowa State University