Class invariant

<h2 id="class-invariants-and-inheritance">Class invariants and inheritance</h2>
<p>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."<a class="footnote-ref" id="fnref:1" href="#fn:1"><sup>1</sup></a>
</p><p>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 <a href="/facts/Composition_over_inheritance/KBF2DslL">composition over inheritance</a> (i.e., inheritance breaks encapsulation).<a class="footnote-ref" id="fnref:2" href="#fn:2"><sup>2</sup></a>
</p><p>However, because class invariants are inherited, the class invariant for any particular class consists of any invariant assertions coded immediately on that class <a href="/facts/Logical_conjunction/62uyyn1d">in conjunction with</a> 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.
</p>
<h2 id="programming-language-support">Programming language support</h2>
<h3>Assertions</h3>
<p>Common programming languages like Python,<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a> PHP,<a class="footnote-ref" id="fnref:4" href="#fn:4"><sup>4</sup></a> JavaScript, C++ and Java support <a href="/facts/Assertion_(computing)/lxSfLdLY">assertions</a> 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. Since methods preserve the invariants, they can assume the validity of the invariant and need not explicitly check for it.
</p>
<h3>Native support</h3>
<p>The class invariant is an essential component of <a href="/facts/Design_by_contract/PjacMRRd">design by contract</a>. So, programming languages that provide full <a href="/facts/Design_by_contract/PjacMRRd">native support for design by contract</a>, such as <a href="/facts/Eiffel_(programming_language)/gEzPjzmn">Eiffel</a>, <a href="/facts/Ada_(programming_language)/Y2yHel4l">Ada</a>, and <a href="/facts/D_(programming_language)/4qIzRjkF">D</a>, will also provide full support for class invariants.
</p>
<h3>Non-native support</h3>
<p>For <a href="/facts/C%252B%252B/Et0F2qn9">C++</a>, the <a href="/facts/Loki_(C%252B%252B)/u7EL1aFL">Loki Library</a> provides a framework for checking class invariants, static data invariants, and exception safety.
</p><p>For Java, there is a more powerful tool called <a href="/facts/Java_Modeling_Language/q3RNMJU6">Java Modeling Language</a> that provides a more robust way of defining class invariants.
</p>
<h2 id="examples">Examples</h2>
<h3>Native support</h3>
<h4>Ada</h4>
<p>The <a href="/facts/Ada_(programming_language)/Y2yHel4l">Ada</a> 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).<a class="footnote-ref" id="fnref:5" href="#fn:5"><sup>5</sup></a>  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.
</p>
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;

<h4>D</h4>
<p><a href="/facts/D_(programming_language)/4qIzRjkF">D</a> programming language has native support of class invariants, as well as other <a href="/facts/Contract_programming/PjacMRRd">contract programming</a> techniques.
Here is an example from the official documentation.<a class="footnote-ref" id="fnref:6" href="#fn:6"><sup>6</sup></a>
</p>
class Date {
  int day;
  int hour;

invariant() {
    assert(day >= 1 && day <= 31);
    assert(hour >= 0 && hour <= 23);
  }
}

<h4>Eiffel</h4>
<p>In <a href="/facts/Eiffel_(programming_language)/gEzPjzmn">Eiffel</a>, the class invariant appears at the end of the class following the keyword invariant.
</p>
class
	DATE

create
	make

feature {NONE} -- 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

<h3>Non-native support</h3>
<h4>C++</h4>
<p>The <a href="/facts/Loki_(C%252B%252B)/u7EL1aFL">Loki (C++)</a> library provides a framework written by Richard Sposato for checking class invariants, static data invariants, and <a href="/facts/Exception_safety/Hevphbsh">exception safety</a> level.
</p><p>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.
</p><p>The geopoint invariants are:
</p>
<ul><li>latitude may not be more than 90° north.</li>
<li>latitude may not be less than -90° south.</li>
<li>longitude may not be more than 180° east.</li>
<li>longitude may not be less than -180° west.</li></ul>
#include <loki/Checker.h>  // Needed to check class invariants.

#include <Degrees.hpp>

class GeoPoint {
 public:
  GeoPoint(Degrees latitude, Degrees longitude);

/// Move function will move location of GeoPoint.
  void Move(Degrees latitude_change, Degrees longitude_change) {
    // The checker object calls IsValid at function entry and exit to prove this
    // GeoPoint object is valid. The checker also guarantees GeoPoint::Move
    // function will never throw.
    CheckFor::CheckForNoThrow checker(this, &IsValid);

latitude_ += latitude_change;
    if (latitude_ >= 90.0) latitude_ = 90.0;
    if (latitude_ <= -90.0) latitude_ = -90.0;

longitude_ += longitude_change;
    while (longitude_ >= 180.0) longitude_ -= 360.0;
    while (longitude_ <= -180.0) longitude_ += 360.0;
  }

private:
  /** @note CheckFor performs validity checking in many functions to determine
   if the code violated any invariants, if any content changed, or if the
   function threw an exception.
   */
  using CheckFor = ::Loki::CheckFor<const GeoPoint>;

/// This function checks all object invariants.
  bool IsValid() const {
    assert(this != nullptr);
    assert(latitude_ >= -90.0);
    assert(latitude_ <= 90.0);
    assert(longitude_ >= -180.0);
    assert(longitude_ <= 180.0);
    return true;
  }

Degrees latitude_;   ///< Degrees from equator. Positive is north, negative is
                       ///< south.
  Degrees longitude_;  ///< Degrees from Prime Meridian. Positive is east,
                       ///< negative is west.
}

<h4>Java</h4>
<p>This is an example of a class invariant in the <a href="/facts/Java_programming_language/9ScgFyAL">Java programming language</a> with <a href="/facts/Java_Modeling_Language/q3RNMJU6">Java Modeling Language</a>.
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 <a href="/facts/Precondition/dWbBdG2e">precondition</a> and <a href="/facts/Postcondition/4tF1Havd">postcondition</a> to help ensure the class invariant.
</p>
public class Date {
    int /*@spec_public@*/ day;
    int /*@spec_public@*/ hour;

/*@invariant day >= 1 && day <= 31; @*/ //class invariant
    /*@invariant hour >= 0 && hour <= 23; @*/ //class invariant

/*@
    @requires d >= 1 && d <= 31;
    @requires h >= 0 && h <= 23;
    @*/
    public Date(int d, int h) { // constructor
        day = d;
        hour = h;
    }

/*@
    @requires d >= 1 && d <= 31;
    @ensures day == d;
    @*/
    public void setDay(int d) {
        day = d;
    }

/*@
    @requires h >= 0 && h <= 23;
    @ensures hour == h;
    @*/
    public void setHour(int h) {
        hour = h;
    }
}

<h2 id="references">References</h2>

<ol>
<li id="fn:1"><p>Meyer, Bertrand. Object-Oriented Software Construction, second edition, Prentice Hall, 1997, p. 570. <a href="/wiki/Object-Oriented_Software_Construction" target="_blank">/wiki/Object-Oriented_Software_Construction</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li>
<li id="fn:2"><p>E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading, Massachusetts, 1995., p. 20. <a href="/wiki/Design_Patterns:_Elements_of_Reusable_Object-Oriented_Software" target="_blank">/wiki/Design_Patterns:_Elements_of_Reusable_Object-Oriented_Software</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li>
<li id="fn:3"><p>Official Python Docs, assert statement <a href="https://docs.python.org/3/reference/simple_stmts.html#grammar-token-assert-stmt" target="_blank">https://docs.python.org/3/reference/simple_stmts.html#grammar-token-assert-stmt</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li>
<li id="fn:4"><p>"PHP assert function". Archived from the original on 2001-03-21. <a href="https://www.php.net/manual/en/function.assert.php" target="_blank">https://www.php.net/manual/en/function.assert.php</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li>
<li id="fn:5"><p>"Ada Reference Manual 7.3.2 Type Invariants". ada-auth.org. Retrieved 2022-11-27. <a href="http://www.ada-auth.org/standards/22aarm/html/AA-7-3-2.html" target="_blank">http://www.ada-auth.org/standards/22aarm/html/AA-7-3-2.html</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></p></li>
<li id="fn:6"><p>"Contract Programming - D Programming Language". dlang.org. Retrieved 2020-10-29. <a href="https://dlang.org/spec/contracts.html" target="_blank">https://dlang.org/spec/contracts.html</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></p></li>
</ol>

Class invariant open-in-new

Class invariant