1. Behavioral Interface Specification 2. Specifying New Pure Types For Modeling 3. Class Specifications 4. Other Features of JML 5. Related Work 6. Future Work and Conclusions Bibliography