Teaching Materials

This page contains course materials, including exercises, projects, and slides, from a variety of courses and tutorials that use JML. You’ll also find links to course websites.

We're also developing a repository of screencasts and other resources for Learning Formal Methods Online? using JML.

Instructors: Share your resources. Join us in building the community. See the note below for more on how you can contribute.

Courses and Tutorials using JML

• Verification-centric Development in Java using BON, JML, and ESC/Java2, by Joe Kiniry and others
• Formal Methods in Specification and Design, by Curtis Clifton
• Course "Testing, Debugging, and Verification" held at Chalmers University of Technology; Paper published at TFM 09 on the concepts behind the course. The course uses among other tools the KeY-Hoare system. There is a paper at Formed 08 on the KeY-Hoare System.
• Secret Ninja Formal Methods, by Joe Kiniry and Dan Zimmerman
• JML Tutorial at OOPSLA 2009, by Gary T. Leavens, Curt Clifton, and Hridesh Rajan (based on the earlier CAV 2007 tutorial below), including:
  • Annotated Slides
  • Presentation Slides
• JML Tutorial at CAV 2007, by Gary T. Leavens, Joe Kiniry, and Erik Poll, including:
  • Annotated Slides
  • Presentation Slides
  • Handouts
  • Examples, including some intentional errors for demonstration purposes
  • LaTeX source for the above is available in this zip file
• Formal Methods in the Software Life Cycle, by Erik Poll
• Design by Contract with JML (draft), by Gary T. Leavens and Yoonsik Cheon
• Specification and Verification for Java-like Languages, a reading seminar at Iowa State, led by Gary T. Leavens
• Iowa State JML Seminar, by Gary T. Leavens. Related homework.
• Design with JML, part of an OOA&D course by Gary T. Leavens. In particular, see:
  • Outline-files.txt for summary information;
  • junit.txt, jml.txt, and jml-junit.txt for JML-specific lectures; and
  • README.txt for notation.
  • Related homework and associated file.

Slides

• Supertype abstraction, specification inheritance and behavioral subtyping in JML (ppt), by Gary T. Leavens
• Design by Contract with JML (ppt) , by Yoonsik Cheon

Exercises and Projects

These exercises and projects are made available for other instructors to use, or for individuals who want to practice on their own. To protect academic integrity, we don’t share the solutions. Instructors may contact the authors to request solutions by following the links.

• Example ESC/Java Quicksort Homework by Cormac Flanagan
• More ESC/Java2 exercises suitable for undergrads (Bag, Amount, Taxpayer) by Erik Poll
• Lab exercise on JML and JUnit, by Simanta Mitra

Examples

• The Examples Page has more examples, not necessarily related to teaching
  • The samples in org.jmlspecs.samples.dbc use the design-by-contract style that is useful for teaching and works well with ESC.

Reference Information

The following might also be useful references:

• The main JML web page
• JML Documentation
  • The Preliminary Design Document (dated, but a good high level introduction)

Other Materials on Formal Methods

Here are some additional materials on teaching formal methods. These aren’t necessary JML-related.

• Lecture notes on building a verifying compiler for Spec♭, by K. Rustan M. Leino (bib entry)
• Lecture notes on Specification and Verification of Object-Oriented Software using Dafny, by K. Rustan M. Leino (bib entry)

Formal Verification

• The Formal Verification of Object-Oriented Software project maintains a significant list of teaching materials on formal verification, including some using JML.

---

How to Contribute

Do you have teaching materials that you can share with the community? We would love to add them here. Send links, slides, exercises, or projects to clifton at rose-hulman dot edu. Or, if you’re a member of the JMLSpecs team on SourceForge, you can even add them yourself, just:

1. commit your materials to a new folder in the JMLSpecs Teaching Materials SVN repository under TeachingMaterials/trunk, then
2. edit this page to add a link to the materials. The wiki syntax for this looks like:

[http://sourceforge.net/apps/trac/jmlspecs/export/HEAD/TeachingMaterials/trunk/path_to_file filename]}}}

for example:

[http://sourceforge.net/apps/trac/jmlspecs/export/HEAD/TeachingMaterials/trunk/README.pdf README.pdf]

and appears in the wiki like this:

README.pdf

---