Paper Info
Title
How the design of JML accommodates both runtime assertion checking and formal verification
Abstract
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 exact 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.
Year
DOI
Venue
2005
10.1016/j.scico.2004.05.015
FMCO
Keywords
Field
DocType
specification languages,runtime assertion checking,formal methods,program verification,programming by contract,java language,jml language
Specification language,Programming language,Programming language specification,Computer science,Design by contract,Formal specification,Runtime verification,Formal methods,Java Modeling Language,Formal verification
Journal
Volume
Issue
ISSN
55
1-3
Science of Computer Programming
Citations 
PageRank 
References 
85
7.03
54
Authors
7
Name
Order
Citations
PageRank
Gary T. Leavens12593211.29
Yoonsik Cheon277056.20
Curtis Clifton321115.56
Clyde Ruby454443.46
David R. Cok565140.73
GT Leavens6857.03
DR Cok7857.03