JML's Rich, Inherited Specifications for Behavioral Subtypes
                                  by
			   Gary T. Leavens

			       Abstract

The Java Modeling Language (JML) is used to specify detailed designs
for Java classes and interfaces. It has a particularly rich set of
features for specifying methods. This paper describes those features,
with particular emphasis on the features related to specification
inheritance. It shows how specification inheritance in JML forces
behavioral subtyping, through a discussion of semantics and
examples. It also describes a notion of modular reasoning based on
static type information, supertype abstraction, which is made valid in
JML by methodological restrictions on invariants, history constraints,
and initially clauses and by behavioral subtyping.

Keywords: Supertype abstraction, behavioral subtype, behavioral
subtyping, modularity, specification inheritance, method specification
refinement, join of method specifications, also, specification case,
invariants, JML, Java.

2006 CR Categories:
D.2.2 [Software Engineering]
        Design Tools and Techniques --- Object-oriented design methods;
D.2.3 [Software Engineering]
        Coding Tools and Techniques --- Object-oriented programming;
D.2.4 [Software Engineering]
        Software/Program Verification --- Class invariants,
        correctness proofs, formal methods,
        programming by contract, reliability, tools, JML;
D.2.7 [Software Engineering]
	Distribution, Maintenance, and Enhancement --- Documentation;
D.3.1 [Programming Languages]
	Formal Definitions and Theory --- Semantics;
D.3.2 [Programming Languages]
	Language Classifications --- Object-oriented languages;
D.3.3 [Programming Languages]
	Language Constructs and Features --- classes and objects,
        inheritance;
F.3.1 [Logics and Meanings of Programs]
        Specifying and Verifying and Reasoning about Programs ---
                Assertions, invariants, logics of programs,
                pre- and post-conditions,
                specification techniques.