JML Reference Manual DRAFT, $Revision: 1.220 $ $Date: 2008/01/08 22:43:42 $ (2008)
Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, ...
Permission is granted for you to make copies of this manual for educational and scholarly purposes, and for commercial use in specifying software, but the copies may not be sold or otherwise used for...
with contributions from (2008)
Joseph R. Kiniry, Patrice Chalin, Clément Hurlin, Cees-bart Breunesse, Julien Charles, ...
Automatic verification by means of extended static checking (ESC) has seen some success in industry and academia due to its lightweight and easy-to-use nature. Unfortunately, ESC comes at a cost: a...
with contributions from (2008)
Joseph R. Kiniry, Patrice Chalin, Clément Hurlin, Cees-bart Breunesse, David Cok, ...
Automatic verification by means of extended static checking (ESC) has seen some success in industry and academia due to its lightweight and easy-to-use nature. Unfortunately, ESC comes at a cost: a...
JML Reference Manual DRAFT, $Revision: 1.65 $ (2007)
Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, ...
Permission is granted for you to make copies of this manual for educational and scholarly purposes, and for commercial use in specifying software, but the copies may not be sold or otherwise used for...
L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. R. Kiniry, G. T. Leavens, ...
An overview of JML tools and applications www.jmlspecs.org
Lilian Burdy, Yoonsik Cheon, David Cok, Michael D. Ernst, Joe Kiniry, Gary T. Leavens, ...
Abstract. 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...
Beyond assertions: Advanced specification and verification with JML and ESC/Java2 (2006)
Erik Poll, Patrice Chalin, David Cok, Joe Kiniry, Gary T. Leavens
Abstract. Many state-based specification languages, including the Java Modeling Language (JML), contain at their core specification constructs familiar to most computer science and software...
Design by Contract and Extended Static Checking for Java with JML and ESC/Java2 (2005)
Organizers []joe Kiniry, Erik Poll, David Cok
ecoop05_tutorial.txt
Leavens JML Framed! 3 Behavioral Interface Specification (2004)
Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Rustan Leino, Bart Jacobs, Erik Poll, ...
Behavioral interface specification language, tailored to Java • Records detailed designs • Pre- and postconditions, invariants,... • Synthesizes ideas in sequential specification
Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, ...
this document. The specification of the method largest is given on lines 7 through 15. Line 7 says that this is a public, normal behavior specification. JML permits several di#erent specifications...
An overview of JML tools and applications (2003)
Www Jmlspecs Org, Lilian Burdy, Yoonsik Cheon, David Cok, Michael D. Ernst, Joe Kiniry, ...
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...
An overview of JML tools and applications (2003)
Lilian Burdy, Yoonsik Cheon, David Cok, Michael D. Ernst, Joe Kiniry, Gary T. Leavens, ...
1 Introduction JML [25, 26], which stands for "Java Modeling Language", is useful for specifying detailed designs of Java classes and interfaces. JML is a behavioral interface specification...