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







Deposit Papers 


Leavens, Gary T., Cheon, Yoonsik, Clifton, Curtis, Ruby, Clyde and Cok, David R. (2004) How the Design of JML Accommodates Both Runtime Assertion Checking and Formal Verification. Technical Report 03-04a, Computer Science, Iowa State University.

Full text available as:Adobe PDF

This is the latest version of this eprint.


Specifications 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 side-effect 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.

Keywords:specification languages, runtime assertion checking, documentation, tools, formal methods, program verification, programming by contract, Java language, JML language, Eiffel language, Larch family of specification languages
Subjects:Software: PROGRAMMING TECHNIQUES (E): Object-oriented Programming
Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Semantics of Programming Languages (D.3.1)
ID code:00000333
Deposited by:Gary T. Leavens on 11 May 2004
Alternative Locations:

Available Versions of This Paper

Contact site administrator at: