This text is a general, self contained, and tool independent
introduction into the Java Modeling Language, JML. It appears
in a book about the KeY approach and tool for the verification
of Java software, because JML is the dominating starting point
of KeY style Java verification. However, this chapter does not
depend on any specific tool nor verification methodology in
any way. This introduction is written for all readers with an
interest in formal specification of software in general, and
anyone who wants to learn about the JML approach to
specification in particular.