В программировании , в частности объектно-ориентированном программировании , инвариант класса (или инвариант типа ) — это инвариант, используемый для ограничения объектов класса . Методы класса должны сохранять инвариант. Инвариант класса ограничивает состояние, хранящееся в объекте .
Инварианты класса устанавливаются во время построения и постоянно поддерживаются между вызовами публичных методов. Код внутри функций может нарушать инварианты, если инварианты восстанавливаются до завершения публичной функции. При параллелизме поддержание инварианта в методах обычно требует установления критической секции путем блокировки состояния с помощью мьютекса .
Инвариант объекта или инвариант представления — это конструкция компьютерного программирования, состоящая из набора инвариантных свойств, которые остаются неизменными независимо от состояния объекта. Это гарантирует, что объект всегда будет соответствовать предопределенным условиям, и что методы, следовательно, всегда могут ссылаться на объект без риска делать неточные предположения. Определение инвариантов класса может помочь программистам и тестировщикам обнаружить больше ошибок во время тестирования программного обеспечения .
Полезный эффект инвариантов классов в объектно-ориентированном программном обеспечении усиливается при наличии наследования. Инварианты классов наследуются, то есть «инварианты всех родителей класса применяются к самому классу». [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 полагаться на тот факт, что вершина стека является допустимым значением, что необходимо для доказательства постусловия Pop. Более сложный инвариант типа позволил бы доказать полную функциональную корректность, например, что Pop возвращает значение, переданное в соответствующий Push, но в этом случае мы просто пытаемся доказать, что Pop не возвращает Invalid_Value.
универсальный тип Item является закрытым ; Invalid_Value : в Item ; пакет Stacks имеет тип Stack ( Max_Depth : Positive ) является закрытым с Default_Initial_Condition => Is_Empty ( Stack ); функция Is_Empty ( S : in Stack ) возвращает логическое значение ; функция Is_Full ( S : in Stack ) возвращает логическое значение ; procedure Push ( S : in out Stack ; I : in Item ) с Pre => not Is_Full ( S ) и затем I /= Invalid_Value , Post => not Is_Empty ( S ); procedure Pop ( S : in out Stack ; I : out Item ) с Pre => not Is_Empty ( S ), Post => not Is_Full ( S ) и затем I /= Invalid_Value ; private type Item_Array is array ( Positive range <>) of Item ; тип Stack ( Max_Depth : Positive ) — это запись Длина : Натуральная := 0 ; Данные : Элемент_массива ( 1 .. Max_Depth ) := ( другие => Недопустимое_значение ); конец записи с Type_Invariant => Длина <= Max_Depth и затем ( для всех J в 1 .. Длина => Данные ( J ) /= Недопустимое_значение ); 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]
класс Дата { int день ; int час ; инвариант () { утвердить ( день >= 1 && день <= 31 ); утвердить ( час >= 0 && час <= 23 ); } } В Eiffel инвариант класса появляется в конце класса после ключевого слова invariant.
класс ДАТАсоздать сделатьфункция { НЕТ } -- Инициализация make ( a_day : INTEGER ; a_hour : INTEGER ) -- Инициализируем `Current' с `a_day' и `a_hour'. require valid_day : a_day >= 1 и a_day <= 31 valid_hour : a_hour >= 0 и a_hour <= 23 do day := a_day hour := a_hour ensure day_set : day = a_day hour_set : hour = a_hour end особенность -- Доступ день : ЦЕЛОЕ ЧИСЛО -- День месяца для `Текущего' час : ЦЕЛОЕ ЧИСЛО — Час дня для «Текущего» особенность -- изменение элемента set_day ( a_day : INTEGER ) -- Установить `day' в `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 ) -- Установить `hour' в `a_hour' require valid_argument : a_hour >= 0 and a_hour <= 23 do hour := a_hour ensure hour_set : hour = a_hour end инвариант valid_day : день >= 1 и день <= 31 valid_hour : час >= 0 и час <= 23 конец Библиотека Loki (C++) предоставляет структуру, написанную Ричардом Спосато для проверки инвариантов классов, инвариантов статических данных и уровня безопасности исключений .
Это пример того, как класс может использовать Loki::Checker для проверки того, что инварианты остаются верными после изменения объекта. В примере используется объект geopoint для хранения местоположения на Земле в виде координат широты и долготы.
Инвариантами геоточки являются:
#include <loki/Checker.h> // Необходимо для проверки инвариантов класса. #include <Градусы.hpp> класс GeoPoint { public : GeoPoint ( Градусы широты , Градусы долготы ); /// Функция Move переместит местоположение GeoPoint. void Move ( Degrees latitude_change , Degrees longitude_change ) { // Объект проверки вызывает IsValid при входе и выходе функции, чтобы доказать, что объект GeoPoint // действителен. Проверка также гарантирует, что функция GeoPoint::Move никогда не выдаст исключение. CheckFor :: CheckForNoThrow checker ( this , & IsValid ); широта_ += изменение_широты ; если ( широта_ >= 90.0 ) широта_ = 90.0 ; если ( широта_ <= -90.0 ) широта_ = -90.0 ; долгота_ += изменение_долготы ; пока ( долгота_ >= 180,0 ) долгота_ -= 360,0 ; пока ( долгота_ <= -180,0 ) долгота_ += 360,0 ; } private : /** @note CheckFor выполняет проверку допустимости во многих функциях, чтобы определить, нарушил ли код какие-либо инварианты, изменилось ли какое-либо содержимое или выдала ли функция исключение. */ using CheckFor = :: Loki :: CheckFor < const GeoPoint > ; /// Эта функция проверяет все инварианты объекта. bool IsValid () const { assert ( this != nullptr ); assert ( latitude_ >=- 90.0 ); assert ( latitude_ <= 90.0 ); assert ( longitude_ >=- 180.0 ); assert ( longitude_ <= 180.0 ); return true ; } Градусы широты_ ; ///< Градусы от экватора. Положительное значение — север, отрицательное — ///< юг. Градусы долготы_ ; ///< Градусы от нулевого меридиана. Положительное значение — восток, отрицательное — ///< запад. } Это пример инварианта класса в языке программирования Java с Java Modeling Language . Инвариант должен сохранять значение true после завершения конструктора и при входе и выходе всех открытых функций-членов. Открытые функции-члены должны определять предусловие и постусловие , чтобы гарантировать инвариант класса.
public class Date { int /*@spec_public@*/ день ; int /*@spec_public@*/ час ; /*@invariant день >= 1 && день <= 31; @*/ //классовый инвариант /*@invariant час >= 0 && час <= 23; @*/ //классовый инвариант /*@ @requires d >= 1 && d <= 31; @requires h >= 0 && h <= 23; @*/ public Date ( int d , int h ) { // конструктор 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 час == h; @*/ public void setHour ( int h ) { час = h ; } }