The Java Modeling Language (JML) is widely used in academic research as a common language for formal methods tools that work with Java. JML is a design by contract language that can be used to specify detailed designs of Java programs, frameworks, and class libraries. Over twenty research groups worldwide have built several tools for checking code and finding bugs (see jmlspecs.org). This tutorial will give background for researchers and practitioners interested in doing formal methods research and in using JML for specifying the sequential behavior of Java classes and interfaces. Attendees will write JML specifications for a data type, including pre- and postconditions for methods and object invariants. They will also learn how to use the most important JML tools. In addition, they will learn how to use model fields to hide the actual field declarations in classes, and how JML supports modular reasoning about subtypes with behavioral subtyping