\BOOKMARK [1][-]{section.1}{Motivation}{} \BOOKMARK [2][-]{subsection.1.1}{Design by Contract}{section.1} \BOOKMARK [2][-]{subsection.1.2}{Documentation}{section.1} \BOOKMARK [2][-]{subsection.1.3}{Blame Assignment}{section.1} \BOOKMARK [2][-]{subsection.1.4}{Efficiency}{section.1} \BOOKMARK [2][-]{subsection.1.5}{Modularity of Reasoning}{section.1} \BOOKMARK [2][-]{subsection.1.6}{The Cost of Modularity}{section.1} \BOOKMARK [2][-]{subsection.1.7}{Contracts and Intent}{section.1} \BOOKMARK [1][-]{section.2}{What is JML?}{} \BOOKMARK [1][-]{section.3}{Simple Examples}{} \BOOKMARK [2][-]{subsection.3.1}{Informal Specifications}{section.3} \BOOKMARK [2][-]{subsection.3.2}{Formalization}{section.3} \BOOKMARK [3][-]{subsubsection.3.2.1}{JML Specification Expressions}{subsection.3.2} \BOOKMARK [3][-]{subsubsection.3.2.2}{Information Hiding in Specifications}{subsection.3.2} \BOOKMARK [3][-]{subsubsection.3.2.3}{Non-Null Annotations}{subsection.3.2} \BOOKMARK [3][-]{subsubsection.3.2.4}{Underspecification}{subsection.3.2} \BOOKMARK [3][-]{subsubsection.3.2.5}{Semantics}{subsection.3.2} \BOOKMARK [2][-]{subsection.3.3}{Invariants}{section.3} \BOOKMARK [1][-]{section.4}{Basic Tool Usage}{} \BOOKMARK [2][-]{subsection.4.1}{Overview of Tools}{section.4} \BOOKMARK [2][-]{subsection.4.2}{JML Compiler}{section.4} \BOOKMARK [1][-]{section.5}{Other Things in JML}{} \BOOKMARK [2][-]{subsection.5.1}{Quantifiers}{section.5} \BOOKMARK [2][-]{subsection.5.2}{Inheritance of specifications}{section.5} \BOOKMARK [2][-]{subsection.5.3}{Model Fields}{section.5} \BOOKMARK [1][-]{section.6}{Summary}{} \BOOKMARK [1][-]{section.A}{Installing JML Tools}{}