|
The Java Modeling Language (JML) follows the design by contract paradigm. It admits the specification of Java programs, using Hoare style pre- and postconditions and invariants. The specifications are added as annotation comments to the Java program, which hence can be compiled with any Java compiler. Design by contract, DBC or Programming by contract is a methodology for designing computer software. ...
A specification language is a formal language used in computer science. ...
Java is an object-oriented programming language developed by James Gosling and colleagues at Sun Microsystems in the early 1990s. ...
Hoare logic (also known as Floyd–Hoare logic) is a formal system developed by the British computer scientist C. A. R. Hoare, and subsequently refined by Hoare and other researchers. ...
In logic a precondition is a condition that has to be met, before a main argument can have any value. ...
A postcondition is a fact that must always be true just after the execution of some section of code. ...
In computer science, optimising compilers and the methodology of design by contract pay close attention to invariant quantities in computer programs, where the set of transformations involved is the execution of the steps of the computer program. ...
Annotation is extra information associated with a particular point in a document or other piece of information. ...
A diagram of the operation of a typical multi-language compiler. ...
There are various verification tools for JML, such as a runtime assertion checker and the Extended Static Checker (ESC/Java).
Overview JML is a behavioural interface specification language for Java modules. This means that JML provides semantics to formally describe the behaviour of a Java module, removing potential ambiguity with regard to the module designers intentions. JML inherits ideas from Eiffel, Larch and the Refinement Calculus, with the goal of providing rigorous formal semantics while still being accessible to any Java programmer. Specifications can be written as annotations in Java program files, or stored in separate specification files. Various tools are available that make use of the extra behavioural information that JML specifications provide, and, because JML annotations take the form of Java comments, whether embedded in Java code or in separate files, Java modules with JML specifications can be compiled unchanged with any Java compiler. The Eiffel Tower Gustave Eiffel, builder of said tower Eiffel programming language Eifel region of Germany (Eiffel is a common misspelling) Eiffel 65, an electronic dance pop band This is a disambiguation page — a navigational aid which lists other pages that might otherwise share the same title. ...
The Larch family of formal specification languages are intended for the precise specification of computing systems. ...
The Refinement Calculus is a formalized approach to stepwise refinement for program construction. ...
Syntax JML specifications are added to Java code in the form of annotations in comments. Java comments are interpreted as JML annotations when they begin with an @ sign. That is, comments of the form //@ <JML specification> or /*@ <JML specification> @*/ Basic JML syntax provides the following keywords requires - Defines a precondition on the method that follows.
ensures - Defines a postcondition on the method that follows.
signals - Defines a condition on when a given Exception can be thrown by the method that follows.
assignable - Defines which fields are allowed to be assigned to by the method that follows.
pure - Declares a method to be side effect free (this shorthand for
assignable nothing). invariant - Defines an invariant property of the class.
also - Declares that a method should inherit conditions from its supertypes.
assert - Defines a JML assertion.
Basic JML also provides the following expressions In logic a precondition is a condition that has to be met, before a main argument can have any value. ...
Used mainly in object-oriented programming, the term method refers to a piece of code that is exclusively associated either with a class (called class methods, static methods, or factory methods) or with an object (called instance methods). ...
A postcondition is a fact that must always be true just after the execution of some section of code. ...
Exception handling is a programming language construct or computer hardware mechanism designed to handle runtime errors or other problems (exceptions) which occur during the execution of a computer program. ...
In computer science, optimising compilers and the methodology of design by contract pay close attention to invariant quantities in computer programs, where the set of transformations involved is the execution of the steps of the computer program. ...
In object-oriented programming, classes are used to group related variables and functions. ...
In computer programming, an assertion is a programming language construct that checks whether an expression is true. ...
result - An identifier for the return value of the method that follows.
old(<name>) - A modifier to refer to the value of variable
<name> at the time of entry into a method. forall - The universal quantifier.
exists - The existential quantifier.
a ==> b - The logical construct
a implies b a <==> b - The logical construct
a if and only if b as well as standard Java syntax for logical and, or, and not. JML annotations also have access to Java objects, object methods and operators that are within the scope of the method being annotated. These are combined to provide formal specifications of the properties of classes, fields and methods. For example, an annotated example of a simple banking class may look like In predicate logic, universal quantification is an attempt to formalise the notion that something (a logical predicate) is true for everything, or every relevant thing. ...
In predicate logic, existential quantification is an attempt to formalize the notion that something (a logical predicate) is true for something, or at least one relevant thing. ...
This article describes the syntax of programming languages. ...
public class BankingExample { public static final int MAX_BALANCE = 1000; private int balance; private boolean isLocked = false; //@ invariant balance >= 0 && balance <= MAX_BALANCE; //@ assignable balance; //@ ensures balance == 0; public BankingExample() { ... } //@ requires amount > 0; //@ ensures balance = old(balance) + amount; //@ assignable balance; public void credit(int amount) { ... } //@ requires amount > 0; //@ ensures balance = old(balance) - amount; //@ assignable balance public void debit(int amount) { ... } //@ ensures isLocked == true; public void lockAccount() { ... } //@ signals (BankingException e) isLocked; public /*@ pure @*/ int getBalance() throws BankingException { ... } } Full documentation (as of 2005, currently still in development) of JML syntax is available [1]. 2005 is a common year starting on Saturday of the Gregorian calendar. ...
Tool Support There are a variety of tools that provide functionality based on JML annotations. The Iowa State JML tools provide an assertion checking compiler jmlc which converts JML annotations into runtime assertions, a documentation generator jmldoc which produces Javadoc documentation augmented with extra information from JML annotations, and a unit test generator jmlunit which generates JUnit testing frameworks from JML annotations. Javadoc is a computer software tool from Sun Microsystems for generating API documentation into HTML format from Java source code. ...
JUnit is a unit testing framework for the Java programming language. ...
In addition to the Iowa State JML tools a number of independent groups are working on tools that make use of JML annotations. These include: ESC/Java2, an extended static checker which uses JML annotations to perform more rigorous static checking than is otherwise possible; Daikon, a dynamic invariant generator; KeY, which provides a theorem prover with a JML front-end; Krakatoa, a theorem prover using the Coq proof assistant; and JMLeclipse, a plugin for the Eclipse integrated development environment with support for JML syntax and interfaces to various tools that make use of JML annotations. Coq is a proof assistant which handles mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. ...
Eclipse is a free software / open source platform-independent software framework for delivering what the project calls rich-client applications, as opposed to thin client browser-based applications. ...
Literature - Gary T. Leavens, Yoonsik Cheon. Design by Contract with JML. Draft tutorial.
- Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A Notation for Detailed Design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), Behavioral Specifications of Businesses and Systems, chapter 12, pages 175-188. Kluwer, 1999.
External links |
Feeds |
Contact