What is JML Good For?
” really boils down to the following question: what good is formal specification for Java program modules? The two main benefits in using JML are: • the precise, unambiguous specification of the behavior of Java program modules (i.e., classes and interfaces), and documentation of Java code, • the possibility of tool support [Burdy-etal03]. Although we would like tools that would help with reasoning about concurrent aspects of Java programs, the current version of JML focuses on the sequential behavior of Java code. While there is work in progress on extending JML to support concurrency, the current version of JML does not have features that help specify how Java threads interact with each other. JML does not, for example, allow the specification of elaborate temporal properties, such as coordinated access to shared variables or the absence of deadlock. Indeed, we assume, in the rest of this manual, that there is only one thread of execution in a Java program annotated with JML, and we
