Инвариант класса

В программировании, в частности объектно-ориентированном программировании, инвариант класса (или инвариант типа) — накладываемое программистом условие, когда объект того или иного типа находится в корректном состоянии.

Во время создания классов устанавливаются их инварианты, которые постоянно поддерживаются между вызовами публичных методов. Временное нарушение классовой инвариантности между частными вызовами метода возможно, хотя и нежелательно.

Инвариант объекта представляет собой конструкцию программирования, состоящую из набора инвариантных свойств. Это гарантирует, что объект всегда будет соответствовать предопределенным условиям, и поэтому методы могут всегда ссылаться на объект без риска сделать неточные презумпции. Определение инвариантов классов может помочь программистам и тестировщикам обнаружить больше ошибок при тестировании программного обеспечения.

Объект «строка переменной длины» содержит указатель, длину выделенного буфера и длину строки, и инварианты таковы:

1. Указатель никогда не NULL. Для строки без буфера будет («\0», 0, 0).
2. Если же буфер выделен — он во владении данного объекта и должен быть возвращён при уничтожении.
3. Записанная в объекте длина буфера согласуется с выделенной.
4. Длина строки не больше, чем длина выделенной памяти минус 1 — кроме упомянутого случая («\0», 0, 0).
5. Символ указатель[длина_строки] имеет код 0.

Одни из этих свойств легко проверяются добавленными в код самопроверками, другие — только подразумеваются.

Полезный эффект инвариантов класса в объектно-ориентированном программировании увеличивается при наличии наследования. Инварианты класса наследуются, то есть инварианты всех родителей класса относятся к самому классу.^[1]

Наследование позволяет классам-потомкам изменять данные реализации родительских классов, поэтому класс потомков может изменять состояние экземпляров таким образом, чтобы сделать их недействительными с точки зрения родительского класса. Обращение к этому типу неверного потомка является одной из причин, по которой объектно-ориентированные разработчики программного обеспечения дают предпочтение инкапсуляции наследованию.^[2]

Однако, поскольку инварианты класса наследуются, инвариант класса для любого конкретного класса состоит из любых инвариантных утверждений, закодированных непосредственно в этом классе, совмещено со всеми инвариантными предложениями, унаследованными от родителей этого класса. Это означает, что, хотя классы потомков могут иметь доступ к данным реализации своих родителей, инвариант класса может помешать им манипулировать этими данными любым способом, который создаёт недопустимый экземпляр во время выполнения.

Такие языки программирования, как C++ и Java, поддерживают утверждения по умолчанию, что может использоваться для определения инвариантов класса. Общим примером реализации инвариантов в классах является то, что конструктор класса генерирует исключение, если инвариант не выполняется. Поскольку методы сохраняют инварианты, они могут принять справедливость инварианта и не должны явно проверять его.

Инвариант класса является существенным компонентом контрактного программирования. Таким образом, языки программирования, обеспечивающие полную поддержку контрактного программирования, такие как Eiffel, Ада и D, также будут обеспечивать полную поддержку инвариантов классов.

В Java существует более мощный инструмент, называемый Java Modeling Language, который обеспечивает более надежный способ определения инвариантов класса.

Язык программирования D имеет встроенную поддержку инвариантов класса, а также другие методы программирования контрактов. Вот пример из официальной документации.

class Date {
  int day;
  int hour;

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

В 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: 1 <= a_day and a_day <= 31
			valid_hour: 0 <= a_hour 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: 1 <= a_day 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: 0 <= a_hour and a_hour <= 23
		do
			hour := a_hour
		ensure
			hour_set: hour = a_hour
		end

invariant
	valid_day: 1 <= day and day <= 31
	valid_hour: 0 <= hour and hour <= 23
end

Это пример инварианта класса в языке программирования Java с Java Modeling Language. Инвариант должен иметь значение true после завершения конструктора и при входе, и выходе всех членов публичной функции, которые должны определять предварительное условие и постусловие, чтобы обеспечить инвариант класса.

public class Date {
    int /*@spec_public@*/ day;
    int /*@spec_public@*/ hour;

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

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

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

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

1. ↑ Bertrand Meyer. Object-Oriented Software Construction. — 2-е изд. — 1997. — С. 570.
2. ↑ E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. — 1995. — С. 20.