3. Invariants

Invariants

Abstract invariant

A method is defined as pure if it doesn’t have side-effects. When writing pre and post-conditions of public methods one can only use method and class public members; such as formal parameters, \result, public pure methods and public attributes.

In JML an abstract invariant is a condition that must be always verified for the abstract object (AOT), whereas a public invariant can only use public attributes and methods. In order to check if an invariant is verified in pure classes one must only take into consideration the formal specific of the constructor(s), not the implementation. Conversely if one have to verify a non-pure class invariant it’s necessary to consider the constructor(s) as well as the modifier methods. If the invariant is verified at the end of the constructor and if it’s verified when the method is called, one must demonstrate that it’s still verified at the end of the mutators execution.

Modifier methods, also called mutators, are non-pure ones, i.e., they can modify fields of objects.

Representation invariant

An Abstract Data Type (ADT) implementation must provide: a representation (rep) for the type’s objects and an implementation of all of the operations. A rep consists of a data structure in order to raprentate its values and a set of private instance variables.

An Abstraction Function (AF) associates to each concrete state one and only one abstract state; it can be total or partial. It defines the meaning of the representation, i.e., establishes how each object of the class implements an object of the abstraction and it’s defined with a private invariant. A private invariant is able to use the class private attributes and methods, too. Its purpose is to couple private attributes and public observers.

Representation invariant (rep or RI) must be written before any implementation and must contain every property that characterizes an abstract state. This coupled with the AF must include everything needed in order to implement methods given the formal specification.

RI must be valid at the end of a constructor and for each method, if it is verified before its call, then rep must be valid at the end of the call, too.