In
computer programming
Computer programming or coding is the composition of sequences of instructions, called computer program, programs, that computers can follow to perform tasks. It involves designing and implementing algorithms, step-by-step specifications of proc ...
, specifically
object-oriented programming
Object-oriented programming (OOP) is a programming paradigm based on the concept of '' objects''. Objects can contain data (called fields, attributes or properties) and have actions they can perform (called procedures or methods and impl ...
, a class invariant (or type invariant) is an
invariant used for constraining
objects of a
class
Class, Classes, or The Class may refer to:
Common uses not otherwise categorized
* Class (biology), a taxonomic rank
* Class (knowledge representation), a collection of individuals or objects
* Class (philosophy), an analytical concept used d ...
.
Methods of the class should preserve the invariant. The class invariant constrains the state stored in the object.
Class invariants are established during
construction
Construction are processes involved in delivering buildings, infrastructure, industrial facilities, and associated activities through to the end of their life. It typically starts with planning, financing, and design that continues until the a ...
and constantly maintained between calls to public methods. Code within functions may break invariants as long as the invariants are restored before a public function ends. With
concurrency, maintaining the invariant in methods typically requires a critical section to be established by locking the state using a
mutex.
An object invariant, or representation invariant, is a computer programming construct consisting of a set of invariant properties that remain uncompromised regardless of the state of the object. This ensures that the object will always meet predefined conditions, and that methods may, therefore, always
reference
A reference is a relationship between objects in which one object designates, or acts as a means by which to connect to or link to, another object. The first object in this relation is said to ''refer to'' the second object. It is called a ''nam ...
the object without the risk of making inaccurate presumptions. Defining class invariants can help programmers and testers to catch more bugs during
software testing
Software testing is the act of checking whether software satisfies expectations.
Software testing can provide objective, independent information about the Quality (business), quality of software and the risk of its failure to a User (computin ...
.
Class invariants and inheritance
The useful effect of class invariants in object-oriented software is enhanced in the presence of inheritance. Class invariants are inherited, that is, "the invariants of all the parents of a class apply to the class itself."
Inheritance can allow descendant classes to alter implementation data of parent classes, so it would be possible for a descendant class to change the state of instances in a way that made them invalid from the viewpoint of the parent class. The concern for this type of misbehaving descendant is one reason object-oriented software designers give for favoring
composition over inheritance (i.e., inheritance breaks encapsulation).
However, because class invariants are inherited, the class invariant for any particular class consists of any invariant assertions coded immediately on that class
in conjunction with all the invariant clauses inherited from the class's parents. This means that even though descendant classes may have access to the implementation data of their parents, the class invariant can prevent them from manipulating those data in any way that produces an invalid instance at runtime.
Programming language support
Assertions
Common programming languages like Python, PHP, JavaScript, C++ and Java support
assertions by default, which can be used to define class invariants. A common pattern to implement invariants in classes is for the constructor of the class to throw an exception if the invariant is not satisfied. For mutable classes, e.g., in the presence of setter methods or when they depend on other mutable objects, one might in addition want to check after each modification whether the invariant was correctly re-established, which guarantees that method implementations indeed preserve the class invariants.
Native support
The class invariant is an essential component of
design by contract. So, programming languages that provide full
native support for design by contract, such as
Eiffel,
Ada,
Dafny, and
D, will also provide full support for class invariants.
Non-native support
For
C++, the
Loki Library provides a framework for checking class invariants, static data invariants, and exception safety.
For Java, there is a more powerful tool called
Java Modeling Language that provides a more robust way of defining class invariants.
Examples
Native support
Ada
The
Ada programming language has native support for type invariants (as well as pre- and postconditions, subtype predicates, etc.). A type invariant may be given on a private type (for example to define a relationship between its abstract properties), or on its full definition (typically to help in verifying the correctness of the implementation of the type). Here is an example of a type invariant given on the full definition of a private type used to represent a logical stack. The implementation uses an array, and the type invariant specifies certain properties of the implementation that enable proofs of safety. In this case, the invariant ensures that, for a stack of logical depth N, the first N elements of the array are valid values. The Default_Initial_Condition of the Stack type, by specifying an empty stack, ensures the initial truth of the invariant, and Push preserves the invariant. The truth of the invariant then enables Pop to rely on the fact that the top of the stack is a valid value, which is needed to prove Pop's postcondition. A more complex type invariant would enable the proof of full functional correctness, such as that Pop returns the value passed into a corresponding Push, but in this case we are merely trying to prove that Pop does not return an Invalid_Value.
generic
type Item is private;
Invalid_Value : in Item;
package Stacks is
type Stack(Max_Depth : Positive) is private
with Default_Initial_Condition => Is_Empty (Stack);
function Is_Empty(S : in Stack) return Boolean;
function Is_Full(S : in Stack) return Boolean;
procedure Push(S : in out Stack; I : in Item)
with Pre => not Is_Full(S) and then I /= Invalid_Value,
Post => not Is_Empty(S);
procedure Pop(S : in out Stack; I : out Item)
with Pre => not Is_Empty(S),
Post => not Is_Full(S) and then I /= Invalid_Value;
private
type Item_Array is array (Positive range <>) of Item;
type Stack(Max_Depth : Positive) is record
Length : Natural := 0;
Data : Item_Array (1 .. Max_Depth) := (others => Invalid_Value);
end record
with Type_Invariant => Length <= Max_Depth and then
(for all J in 1 .. Length => Data (J) /= Invalid_Value);
function Is_Empty(S : in Stack) return Boolean
is (S.Length = 0);
function Is_Full(S : in Stack) return Boolean
is (S.Length = S.Max_Depth);
end Stacks;
D
D programming language has native support of class invariants, as well as other
contract programming techniques.
Here is an example from the official documentation.
class Date
Eiffel
In
Eiffel, the class invariant appears at the end of the class following the keyword
invariant
.
class
DATE
create
make
feature -- Initialization
make (a_day: INTEGER; a_hour: INTEGER)
-- Initialize `Current' with `a_day' and `a_hour'.
require
valid_day: a_day >= 1 and a_day <= 31
valid_hour: a_hour >= 0 and a_hour <= 23
do
day := a_day
hour := a_hour
ensure
day_set: day = a_day
hour_set: hour = a_hour
end
feature -- Access
day: INTEGER
-- Day of month for `Current'
hour: INTEGER
-- Hour of day for `Current'
feature -- Element change
set_day (a_day: INTEGER)
-- Set `day' to `a_day'
require
valid_argument: a_day >= 1 and a_day <= 31
do
day := a_day
ensure
day_set: day = a_day
end
set_hour (a_hour: INTEGER)
-- Set `hour' to `a_hour'
require
valid_argument: a_hour >= 0 and a_hour <= 23
do
hour := a_hour
ensure
hour_set: hour = a_hour
end
invariant
valid_day: day >= 1 and day <= 31
valid_hour: hour >= 0 and hour <= 23
end
Non-native support
C++
The
Loki (C++) library provides a framework written by
Richard Sposato for checking class invariants, static data invariants, and
exception safety level.
This is an example of how a class can use Loki::Checker to verify that invariants remain true after an object changes. The example uses a geopoint object to store a location on Earth as a coordinate of latitude and longitude.
The geopoint invariants are:
* latitude may not be more than 90° north.
* latitude may not be less than -90° south.
* longitude may not be more than 180° east.
* longitude may not be less than -180° west.
#include // Needed to check class invariants.
#include
class GeoPoint
Java
This is an example of a class invariant in the
Java programming language
Java is a high-level, general-purpose, memory-safe, object-oriented programming language. It is intended to let programmers ''write once, run anywhere'' ( WORA), meaning that compiled Java code can run on all platforms that support Jav ...
with
Java Modeling Language.
The invariant must hold to be true after the constructor is finished and at the entry and exit of all public member
functions. Public member functions should define
precondition
In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification.
If a precondition is violated, the effect of the ...
and
postcondition In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions w ...
to help ensure the class invariant.
public class Date
References
{{Reflist, 2
Class (computer programming)