Preliminary Design of JML:

A Behavioral Interface Specification Language for Java

• 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 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 Invariant 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 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

This document was generated on 22 November 2004 using texi2html 1.56k.