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...
Specification Facets for More Precise, Focused Documentation (2007)
Gary Leavens Iowa, Gary T. Leavens, Clyde Ruby
Specification languages could aid reuse to a larger extent if they could document all important facets of software, not just functional behavior. Since a specification language designer cannot know...
Specification Facets for More Precise, Focused Documentation (2007)
Gary Leavens, Gary T. Leavens, Clyde Ruby, Clyde Ruby
Specification languages could aid reuse to a larger extent if they could document all important facets of software, not just functional behavior. Since a specification language designer cannot know...
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...
Gary T. Leavens, Joint Yoonsik Cheon, Curt Clifton, Clyde Ruby, Arun Raghavan, ...
much easier to maintain than code .Rigorous semantics: can use for verification Approach .Java expressions for assertions ( la Eiffel) .Model-based specifications (Larch, VDM) Contribution .Language...
Gary T. Leavens, Albert L. Baker, Clyde Ruby
assertion checkers, class invariants, formal methods, programming
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...
How the Design of JML Accommodates Both Runtime Assertion Checking and Formal Verification (2004)
Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, David R. Cok
Specifications that are used in detailed design and in the documentation of existing code are primarily written and read by programmers.
JML Reference Manual DRAFT, $Revision: 1.29 $ (2003)
Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby
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...
How the design of JML accommodates both runtime assertion checking and formal verification (2003)
Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, David R. Cok, Gary T. Leavens, ...
Techniques — modules and interfaces, object-oriented design methods; D.2.4
Preliminary design of JML (2001)
Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, Clyde Ruby, Clyde Ruby
specification techniques. Copyright c fl 1998, 1999 by Iowa State University. This document s distributed under the terms of the GNU General Public License as published by the Free Software...
JML: notations and tools supporting detailed design in Java (2000)
Gary T. Leavens, K. Rustan, M. Leino, Erik Poll, Clyde Ruby, Bart Jacobs, ...
2000 ACM. Permission to make digital or hard copies of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial...
Safely Creating Correct Subclasses without Seeing Superclass Code (2000)
Clyde Ruby, Clyde Ruby, Gary T. Leavens, Gary T. Leavens
A major problem for object-oriented frameworks and class libraries is how to provide enough information about a superclass, so programmers can safely create new subclasses without giving away the...
JML: notations and tools supporting detailed design in Java (2000)
Gary T. Leavens, Gary T. Leavens, Clyde Ruby, Clyde Ruby, K. Rustan, ...
JML is a notation for specifying the detailed design of Java classes and interfaces. JML's assertions are stated using a slight extension of Java's expression syntax. This should make it...
JML: A Notation for Detailed Design (1999)
Gary T. Leavens, Albert L. Baker, Clyde Ruby
JML is a behavioral interface specification language tailored to Java. It is designed to be written and read by working software engineers, and should require only modest mathematical training. It...
Preliminary Design of JML: A Behavioral Interface Specification Language for Java (1999)
Gary T. Leavens, Albert L. Baker, Clyde Ruby
JML is a behavioral interface specification language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to verification and debugging. JML is designed to be used...
Preliminary Design of JML: A Behavioral Interface Specification Language for Java (1999)
Copyright Gary, Gary T. Leavens, Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, ...
JML is a behavioral interface specification language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to verification and debugging. JML is designed to be used...
JML: A notation for detailed design (1999)
Gary T. Leavens, Albert L. Baker, Clyde Ruby
JML is a behavioral interface specification language tailored to Java. It is designed to be written and read by working software engineers, and should require only modest mathematical training. It...
Preliminary design of JML: A behavioral interface specification language for Java (1998)
Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, Clyde Ruby, Clyde Ruby
JML is a behavioral interface specification language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to verification and debugging. JML is designed to be used...
Preliminary design of JML: A behavioral interface specification language for Java (1998)
Copyright Gary, T. Leavens, Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, ...
JML is a behavioral interface specification language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to verification and debugging. JML is designed to be used...
JML: a Java Modeling Language (1998)
Gary T. Leavens, Albert L. Baker, Clyde Ruby
JML is a behavioral interface specification language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to verification and debugging. JML is designed to be used...
Preliminary Design of JML: A Behavioral Interface Specification Language for Java (1998)
Copyright Gary, Gary T. Leavens, Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, ...
JML is a behavioral interface specification language tailored to Java. JML is designed to be used by working software engineers, and requires only modest mathematical training. To achieve this goal,...
Preliminary Design of JML: A Behavioral Interface Specification Language for Java (1998)
Copyright Gary, Gary Leavens, Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, ...
JML is a behavioral interface specification language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to verification and debugging. JML is designed to be used...
Preliminary design of JML: A behavioral interface specification language for Java (1998)
Gary T. Leavens, Albert L. Baker, Clyde Ruby
theory, Larch, Ei el, JML, ESC/Java; D.2.4 [Software Engineering] Software/Program Veri cation
Preliminary design of JML: A behavioral interface specification language for Java (1998)
Copyright Gary, T. Leavens, Gary T. Leavens, Gary T. Leavens, Albert L. Baker, Albert L. Baker, ...
JML is a behavioral interface speci cation language tailored to Java. It also allows assertions to be intermixed with Java code, as an aid to veri cation and debugging. JML is designed to be used by...
Preliminary design of JML: A behavioral interface specification language for Java (1998)
Gary T. Leavens, Albert L. Baker, Clyde Ruby
assertion checkers, class invariants, formal methods, programming
Gary T. Leavens, Clyde Ruby, Gary T. Leavens, Clyde Ruby
F.3.1 [Logics and Meaning of Programs] Specifying and verifying and reasoning about programs | Assertions, invariants, pre- and post-conditions, speci cation techniques.