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

В компьютерном программировании , особенно объектно-ориентированном программировании , инвариант класса (или инвариант типа ) — это инвариант, используемый для ограничения объектов класса в . Методы класса должны сохранять инвариант. Инвариант класса ограничивает состояние, хранящееся в объекте.

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

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

Инварианты классов и наследование [ править ]

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

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

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

Поддержка языков программирования [ править ]

Утверждения [ править ]

Распространенные языки программирования, такие как Python, ^[3] PHP, ^[4] JavaScript, ^{[ нужна ссылка ]} C++ и Java по умолчанию поддерживают утверждения , которые можно использовать для определения инвариантов классов. Распространенным шаблоном реализации инвариантов в классах является создание исключения конструктором класса, если инвариант не удовлетворяется. Поскольку методы сохраняют инварианты, они могут предполагать допустимость инварианта и не нуждаются в его явной проверке.

Встроенная поддержка [ править ]

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

Неродная поддержка [ править ]

Для C++ библиотека Loki предоставляет основу для проверки инвариантов классов, инвариантов статических данных и безопасности исключений.

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

Примеры [ править ]

Встроенная поддержка [ править ]

Есть [ править ]

Язык программирования Ada имеет встроенную поддержку инвариантов типов (а также пред- и постусловий, предикатов подтипов и т. д.). Инвариант типа может быть задан для частного типа (например, для определения связи между его абстрактными свойствами) или для его полного определения (обычно для помощи в проверке правильности реализации типа). ^[5] Вот пример инварианта типа, заданного в полном определении частного типа, используемого для представления логического стека. Реализация использует массив, а инвариант типа определяет определенные свойства реализации, которые обеспечивают доказательство безопасности. В этом случае инвариант гарантирует, что для стека логической глубины N первые N элементов массива являются допустимыми значениями. Default_Initial_Condition типа Stack, указывая пустой стек, обеспечивает начальную истинность инварианта, а Push сохраняет инвариант. Тогда истинность инварианта позволяет Попу полагаться на тот факт, что вершина стека является допустимым значением, что необходимо для доказательства постусловия Попа. Более сложный инвариант типа позволил бы доказать полную функциональную корректность, например, что Pop возвращает значение, переданное в соответствующий Push, но в этом случае мы просто пытаемся доказать, что Pop не возвращает 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 имеет встроенную поддержку инвариантов классов, а также других методов контрактного программирования . Вот пример из официальной документации. ^[6]

class Date {
  int day;
  int hour;

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

Эйфелева [ править ]

В Eiffel инвариант класса появляется в конце класса после ключевого слова invariant.

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

Неродная поддержка [ править ]

С++ [ править ]

Библиотека Loki (C++) предоставляет платформу, написанную Ричардом Спосато, для проверки инвариантов классов, инвариантов статических данных и безопасности исключений уровня .

Это пример того, как класс может использовать Loki::Checker для проверки того, что инварианты остаются верными после изменения объекта. В примере используется объект геоточки для хранения местоположения на Земле в виде координат широты и долготы.

Инварианты геоточки:

широта не может быть выше 90° северной широты.
широта не может быть ниже -90° южной широты.
долгота не может быть более 180° восточной долготы.
долгота не может быть меньше -180° западной долготы.

#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.
}

Ява [ править ]

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

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;
    }
}

Ссылки [ править ]

^ Мейер, Бертран. Объектно-ориентированное построение программного обеспечения , второе издание, Prentice Hall, 1997, стр. 570.
^ Э. Гамма, Р. Хелм, Р. Джонсон и Дж. Влиссидес. Шаблоны проектирования: элементы объектно-ориентированного программного обеспечения многократного использования . Аддисон-Уэсли, Ридинг, Массачусетс, 1995 г., с. 20.
^ Официальная документация Python, утверждение утверждения
^ «Функция утверждения PHP» . Архивировано из оригинала 21 марта 2001 г.
^ «Справочное руководство Ada 7.3.2 Инварианты типов» . ada-auth.org . Проверено 27 ноября 2022 г.
^ «Контрактное программирование — язык программирования D» . dlang.org . Проверено 29 октября 2020 г.

[1] Мейер, Бертран. Объектно-ориентированное построение программного обеспечения , второе издание, Prentice Hall, 1997, стр. 570.

[2] Э. Гамма, Р. Хелм, Р. Джонсон и Дж. Влиссидес. Шаблоны проектирования: элементы объектно-ориентированного программного обеспечения многократного использования . Аддисон-Уэсли, Ридинг, Массачусетс, 1995 г., с. 20.

[3] Официальная документация Python, утверждение утверждения

[4] «Функция утверждения PHP» . Архивировано из оригинала 21 марта 2001 г.

[5] «Справочное руководство Ada 7.3.2 Инварианты типов» . ada-auth.org . Проверено 27 ноября 2022 г.

[6] «Контрактное программирование — язык программирования D» . dlang.org . Проверено 29 октября 2020 г.

[1]

[2]

[3]

[4]

[5]

[6]