How the Design of JML Accommodates Both Runtime Assertion Checking and Formal Verification 


Leavens, Gary T., Cheon, Yoonsik, Clifton, Curtis, Ruby, Clyde and Cok, David R. (2003) How the Design of JML Accommodates Both Runtime Assertion Checking and Formal Verification. Technical Report TR0304, Computer Science, Iowa State University.
There is a later version of this eprint available: Click here to view it. AbstractSpecifications that are used in detailed design and in the documentation of existing code are primarily written and read by programmers. However, most formal specification languages either make heavy use of symbolic mathematical operators, which discourages use by programmers, or limit assertions to expressions of the underlying programming language, which makes it difficult to write complete specifications. Moreover, using assertions that are expressions in the underlying programming language can cause problems both in runtime assertion checking and in formal verification, because such expressions can potentially contain side effects. The Java Modeling Language, JML, avoids these problems. It uses a sideeffect free subset of Java's expressions to which are added a few mathematical operators (such as the quantifiers \forall and \exists). JML also hides mathematical abstractions, such as sets and sequences, within a library of Java classes. The goal is to allow JML to serve as a common notation for both formal verification and runtime assertion checking; this gives users the benefit of several tools without the cost of changing notations.
Available Versions of This Paper
Contact site administrator at: ssg@cs.iastate.edu 