Editing Class invariant (section)

===Native support===

====Ada====
The [[Ada (programming language)|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).<ref>{{Cite web|title=Ada Reference Manual 7.3.2 Type Invariants|url=http://www.ada-auth.org/standards/22aarm/html/AA-7-3-2.html|access-date=2022-11-27|website=ada-auth.org}}</ref>  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.

<syntaxhighlight lang="Ada">
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;
</syntaxhighlight>
====D====
[[D (programming language)|D]] programming language has native support of class invariants, as well as other [[contract programming]] techniques.
Here is an example from the official documentation.<ref>{{Cite web|title=Contract Programming - D Programming Language|url=https://dlang.org/spec/contracts.html|access-date=2020-10-29|website=dlang.org}}</ref>

<syntaxhighlight lang="D">class Date {
  int day;
  int hour;

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

====Eiffel====

In [[Eiffel (programming language)|Eiffel]], the class invariant appears at the end of the class following the keyword <code lang="eiffel">invariant</code>.

<syntaxhighlight lang="eiffel">
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
</syntaxhighlight>