| [Top] | [Contents] | [Index] | [ ? ] |
The Java Modeling Language (JML) is a notation for formally specifying the behavior and interfaces of Java classes and methods. This document gives an overview of JML's design.
1. Introduction 2. Class and Interface Specifications 3. Extensions to Java Expressions 4. Conclusions A. Specification Case Defaults Bibliography Example Index Concept Index
-- The Detailed Node Listing ---
Introduction
1.1 Behavioral Interface Specification 1.2 Lightweight Specifications 1.3 Goals 1.4 Tool Support 1.5 Outline
Tool Support
1.4.1 Type Checking Specifications 1.4.2 Generating HTML Documentation 1.4.3 Run Time Assertion Checking 1.4.4 Unit Testing with JML
Class and Interface Specifications
2.1 Abstract Models 2.2 Data Groups 2.3 Types For Modeling 2.4 Use of Pure Classes 2.5 Composition for Container Classes 2.6 Behavioral Subtyping
Abstract Models
2.1.1 Model Fields 2.1.2 Invariants 2.1.3 Method Specifications 2.1.4 Models and Lightweight Specifications
Method Specifications
2.1.3.1 The Assignable Clause 2.1.3.2 Old Values 2.1.3.3 Reference Semantics 2.1.3.4 Correct Implementation
Data Groups
2.2.1 Specification of BoundedThing 2.2.2 Specification of BoundedStackInterface
Specification of BoundedThing
Specification of BoundedStackInterface
2.2.2.1 Data Groups and Represents Clauses 2.2.2.2 Redundant Specification 2.2.2.3 Multiple Specification Cases 2.2.2.4 Pitfalls in Specifying Exceptions 2.2.2.5 Redundant Ensures Clauses
Types For Modeling
2.3.1 Purity 2.3.2 Money 2.3.3 MoneyComparable and MoneyOps 2.3.4 MoneyAC 2.3.5 MoneyComparableAC 2.3.6 USMoney
Money
2.3.2.1 Redundant Examples 2.3.2.2 JMLType and Informal Predicates
Composition for Container Classes
2.5.1 NodeType 2.5.2 ArcType 2.5.3 Digraph
Extensions to Java Expressions
3.1 Extensions to Java Expressions for Predicates 3.2 Extensions to Java Expressions for Store-Refs