[Top] [Contents] [Index] [ ? ]

Preliminary Design of JML

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

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  

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  



This document was generated by Gary Leavens on March, 16 2009 using texi2html