An overview of JML tools and applications
详细信息 查看全文
- 作者：Lilian Burdy ; Yoonsik Cheon ; David Cok ; Michael D. Ernst ; Joe Kiniry ; Gary T. Leavens ; K. Rustan ; M. Leino ; Erik Poll
- 关键词：formal methods ; formal specification ; Java ; runtime assertion checking ; static checking ; program verification
- 刊名：Electronic Notes in Theoretical Computer Science
- 出版年：2003
- 出版时间：August 2003
- 年：2003
- 卷：80
- 期：Complete
- 页码：75-91
- 全文大小：163 K
文摘
The Java Modeling Language (JML) can be used to specify the detailed design of Java classes and interfaces by adding annotations to Java source files. The aim of JML is to provide a specification language that is easy to use for Java programmers and that is supported by a wide range of tools for specification type-checking, runtime debugging, static analysis, and verification.
This paper gives an overview of the main ideas behind JML, the different groups collaborating to provide tools for JML, and the existing applications of JML. Thus far, most applications have focused on code for programming smartcards written in the Java Card dialect of Java.