Preliminary Design of JML:

A Behavioral Interface Specification Language for Java

[Top]

[Contents]

[Index]

[ ? ]

Table of Contents

1. Introduction

1.1 Behavioral Interface Specification
1.2 Lightweight Specifications
1.3 Goals
1.4 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

1.5 Outline

2. Class and Interface Specifications

2.1 Abstract Models

2.1.1 Model Fields
2.1.2 Invariants
2.1.3 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

2.1.4 Models and Lightweight Specifications

2.2 Data Groups

2.2.1 Specification of BoundedThing

2.2.1.1 Model Fields in Interfaces
2.2.1.2 Invariants and History Constraint
2.2.1.3 Details of the Method Specifications
2.2.1.4 Adding to Method Specifications
2.2.1.5 Specifying Exceptional Behavior

2.2.2 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

2.3 Types For Modeling

2.3.1 Purity
2.3.2 Money

2.3.2.1 Redundant Examples
2.3.2.2 JMLType and Informal Predicates

2.3.3 MoneyComparable and MoneyOps
2.3.4 MoneyAC
2.3.5 MoneyComparableAC
2.3.6 USMoney

2.4 Use of Pure Classes
2.5 Composition for Container Classes

2.5.1 NodeType
2.5.2 ArcType
2.5.3 Digraph

2.6 Behavioral Subtyping

3. Extensions to Java Expressions

3.1 Extensions to Java Expressions for Predicates
3.2 Extensions to Java Expressions for Store-Refs

4. Conclusions
A. Specification Case Defaults
Bibliography
Example Index
Concept Index