Skip to content
This repository has been archived by the owner on Feb 8, 2021. It is now read-only.

1. JML general outline

Dennis Campagna edited this page Jan 22, 2019 · 1 revision

JML

Design by contract

JML uses a **requires **clause to specify the client’s obligation and an **ensures **clause to specify the implementor’s obligation.

A method’s precondition (JML uses the keyword require) says what must be true to call it, whether a method’s postcondition (JML uses the keyword ensures) says what must be true when it terminates. In languages that support exceptions, we further distinguish normal and exceptional postconditions.

Specification

JML specifications are written in special annotation comments, which start with an at-sign (@). Therefore we can write /@ … @/ or //@ to start an annotation properly.

JML uses Java’s expression syntax to write the predicates used in assertions, such as pre- and postconditions and invariants. The predicates cannot be formal statements, since JML supports informal descriptions which are treated as boolean expressions.

The main restriction is that expressions used in JML’s assertions cannot have side effects, because only pure methods can be called in assertions. One must tell JML that a method to be pure by using the pure modifier in the method’s declaration.

JML supports the notion of information hiding by using Java’s privacy levels and enforces it by ensuring that public specifications can only mention publicly visible names.

A subclass inherits specifications such as preconditions, postconditions and invariants from its superclasses and interfaces that it implements. An interface also inherits specifications of the interfaces that it extends.

Pure functions

In computer programming, a function may be considered a pure function if both below statements about the function hold: The function always evaluates the same result value given the same argument value(s). The function result value cannot depend on any hidden information or state that may change while program execution proceeds or between different executions of the program, nor can it depend on any external input from I/O devices. Evaluation of the result does not cause any semantically observable side effect or output, such as mutation of mutable objects or output to I/O devices.

Invariants

An invariant is a property that should hold in all client-visible states. It must be true when control is not inside the object’s methods. That is, an invariant must hold at the end of each constructor’s execution, and at the beginning and end of all methods. A public invariant clause allows one to define the acceptable states of an object that are client-visible (also called type invariants). In JML one can also specify invariants with more restrictive visibility; such invariants are called representation invariants. Representation invariants can be used to define acceptable internal states of an object.

Quantifiers

JML supports several kinds of quantifiers in assertions: a universal quantifier (\forall), an existential quantifier (\exists), generalized quantifiers (\sum, \product, \min, and \max), and a numeric quantifier (\num_of). In a quantifier there is a declaration of a name that is local to the quantifier. This is followed by an optional range predicate, that restricts the domain to which the quantifier applies. If the range predicate is omitted, there is no restriction on the objects being quantified over, and so all possible objects apply. Finally, the third predicate, the body of the quantifier, must be true of all the objects that satisfy the range predicate.

The quantifiers \max, \min, \product and \sum are generalized quantifiers that return respectively the maximum, minimum, product and sum of the values of their body expression when the quantified variables satisfy the given range expression.

The numerical quantifier, \num_of, returns the number of values for quantified variables for which the range and the body predicate are true.

Clone this wiki locally