Attendees will come out of this tutorial with a firm understanding of the use of specifications in software design and engineering, a basic knowledge of the JML specification languages, and will be knowledgeable about the various tools available for the JML language, particularly the JML tool suite, ESC/Java2, and Kiasan.