Инвариант (программирование)
Инвариа́нтом в программировании называется логическое выражение, истинное после каждого прохода тела цикла (после выполнения фиксированного оператора) и перед началом выполнения цикла, зависящее от переменных, изменяющихся в теле цикла. [1]
Инварианты используются в теории верификации программ для доказательства правильности выполнения цикла. Порядок доказательства работоспособности цикла с помощью инварианта сводится к следующему:
- Доказывается, что выражение инварианта истинно перед началом цикла.
- Доказывается, что выражение инварианта сохраняет свою истинность после выполнения тела цикла; таким образом, по индукции, доказывается, что по завершении цикла инвариант будет выполняться.
- Доказывается, что при истинности инварианта после завершения цикла переменные примут именно те значения, которые требуется получить (это элементарно определяется из выражения инварианта и известных конечных значениях переменных, на которых основывается условие завершения цикла).
- Доказывается (возможно — без применения инварианта), что цикл завершится, то есть условие завершения рано или поздно будет выполнено.
- Истинность утверждений, доказанных на предыдущих этапах, однозначно свидетельствует о том, что цикл выполнится за конечное время и даст желаемый результат.
Также инварианты используют при проектировании и оптимизации циклических алгоритмов. Например, чтобы убедиться, что оптимизированный цикл остался корректным, достаточно доказать, что инвариант цикла не нарушен и условие завершения цикла достижимо.
Понятие инварианта также используется в объектно-ориентированном программировании для обозначения непротиворечивого состояния объекта. Подразумевается, что вызов любого метода оставляет объект в состоянии инварианта.
Примечания
- ↑Построение цикла с помощью инварианта
- Формальные методы
Wikimedia Foundation . 2010 .
Полезное
Смотреть что такое «Инвариант (программирование)» в других словарях:
Инвариант — или инвариантность термин, обозначающий нечто неизменяемое. Конкретное значение термина зависит от той области, где он используется: Инвариант (математика) Инвариант узла в топологии Инвариант (физика) Инвариант (программирование) Инвариант … Википедия
ПРОГРАММИРОВАНИЕ ТЕОРЕТИЧЕСКОЕ — математическая дисциплина, изучающая математич. абстракции программ, трактуемых как объекты, выраженные на формальном языке, обладающие определенной информационной и логич. структурой и подлежащие исполнению на автоматич. устройствах. П. т.… … Математическая энциклопедия
Конструктор (программирование) — У этого термина существуют и другие значения, см. Конструктор. В объектно ориентированном программировании конструктор класса (от англ. constructor, иногда сокращают ctor) специальный блок инструкций, вызываемый при создании объекта.… … Википедия
ДРАКОН — Эта статья предлагается к удалению. Пояснение причин и соответствующее обсуждение вы можете найти на странице Википедия:К удалению/28 сентября 2012. Пока процесс обсуждения не завершён, статью мож … Википедия
ДРАКОН (алгоритмический язык) — У этого термина существуют и другие значения, см. Дракон (значения). Пример блок схемы алгоритма на языке ДРАКОН дракон схемы ДРАКОН (Дружелюбный Русский Алгоритмический язык, Который Обеспечивает Наглядность) визуальный… … Википедия
Конструктор класса — В объектно ориентированном программировании конструктор класса (от англ. constructor, иногда сокращают ctor) специальный блок инструкций, вызываемый при создании объекта, причём или при его объявлении (располагаясь в стеке или в статической… … Википедия
Конструктор объекта — В объектно ориентированном программировании конструктор класса (от англ. constructor, иногда сокращают ctor) специальный блок инструкций, вызываемый при создании объекта, причём или при его объявлении (располагаясь в стеке или в статической… … Википедия
Ковариантность и контравариантность — Ковариантность и контравариантность математическое и физическое понятие, которое описывает то, как величины изменяются при преобразовании системы координат. Координаты геометрического вектора измеряются в какой нибудь конкретной системе… … Википедия
КУЛЬТУРА — (лат. cultura возделывание, воспитание, почитание) универсум искусственных объектов (идеальных и материальных предметов; объективированных действий и отношений), созданный человечеством в процессе освоения природы и обладающий структурными,… … Философская энциклопедия
Шаблон — О шаблонах в Википедии смотрите страницу Википедия:Шаблоны. Шаблон в технике пластина (лекало, трафарет и т. п.) с вырезами, по контуру которых изготовляются чертежи или изделия либо инструмент для измерения размеров. Шаблон в… … Википедия
Инвариант класса — Class invariant
В компьютерном программировании, в частности, объектно-ориентированном программировании, класс инвариант (или инвариант типа ) — это инвариант, используемый для ограничения объектов из класса. Методы класса должны сохранять инвариант. Инвариант класса ограничивает состояние, хранящееся в объекте.
Инварианты класса устанавливаются во время построения и постоянно поддерживаются между вызовами общедоступных методов. Код внутри функций может нарушать инварианты до тех пор, пока инварианты восстанавливаются до завершения публичной функции.
Инвариант объекта или инвариант представления — это конструкция компьютерного программирования, состоящая из набора инвариантных свойств, которые остаются неизменными независимо от состояния объекта . Это гарантирует, что объект всегда будет соответствовать предопределенным условиям, и что методы могут, следовательно, всегда ссылаться на объект без риска сделать неточные предположения. Определение инвариантов классов может помочь программистам и тестировщикам обнаруживать больше ошибок во время тестирования программного обеспечения.
Содержание
- 1 Инварианты классов и наследование
- 2 Поддержка языков программирования
- 2.1 Утверждения
- 2.2 Встроенная поддержка
- 2.3 Ненативная поддержка
- 3.1 Нативная поддержка
- 3.1.1 D
- 3.1.2 Eiffel
- 3.2.1 C ++
- 3.2.2 Java
Инварианты классов и наследование
Полезный эффект инвариантов классов в объектно-ориентированном ПО усиливается при наличии наследования. Инварианты классов наследуются, то есть «инварианты всех родителей класса применяются к самому классу».
Наследование может позволить классам-потомкам изменять данные реализации родительских классов, поэтому было бы возможно класс-потомок, чтобы изменить состояние экземпляров таким образом, чтобы они стали недействительными с точки зрения родительского класса. Беспокойство по поводу этого типа некорректного поведения потомков — одна из причин, по которой разработчики объектно-ориентированного программного обеспечения предпочитают композицию наследованию (т.е. наследование нарушает инкапсуляцию).
Однако, поскольку инварианты классов наследуются, инвариант класса для любого конкретного класса состоит из любых инвариантных утверждений, закодированных непосредственно в этом классе вместе с всеми инвариантными предложениями, унаследованными от родителей класса. Это означает, что даже несмотря на то, что классы-потомки могут иметь доступ к данным реализации своих родителей, инвариант класса может помешать им манипулировать этими данными любым способом, который создает недопустимый экземпляр во время выполнения.
Поддержка языков программирования
Утверждения
Общие языки программирования, такие как Python, JavaScript, C ++ и Java, по умолчанию поддерживают утверждения, которые можно использовать для определения инварианты классов. Обычный шаблон для реализации инвариантов в классах состоит в том, что конструктор класса генерирует исключение, если инвариант не выполняется. Поскольку методы сохраняют инварианты, они могут предполагать действительность инварианта и не должны явно проверять его.
Встроенная поддержка
Инвариант класса является важным компонентом проектирования по контракту. Итак, языки программирования, которые обеспечивают полную нативную поддержку дизайна по контракту, например Rust, Eiffel, Ada и D, также будет обеспечивать полную поддержку инвариантов классов.
Неродная поддержка
Для C ++ Loki Library предоставляет основу для проверки инвариантов классов, инвариантов статических данных и безопасности исключений.
Для Java существует более мощный инструмент под названием Java Modeling Language, который обеспечивает более надежный способ определения инвариантов классов.
Примеры
Встроенная поддержка
D Язык программирования имеет встроенную поддержку инвариантов классов, а также других методов контрактного программирования. Вот пример из официальной документации.
Eiffel
В Eiffel инвариант класса появляется в конце класса после ключевое слово инвариант .
Поддержка неродных версий
Библиотека Loki (C ++) предоставляет платформу, написанную для проверки инвариантов классов, инвариантов статических данных и уровня безопасности исключений.
Это пример того, как класс может использовать Loki :: Checker для проверки того, что инварианты остаются верными после изменения объекта. В этом примере объект географической точки используется для сохранения местоположения на Земле в качестве координат широты и долготы.
- широта не может быть больше 90 ° северной широты.
- широта не может быть оставлена ss, чем -90 ° южной широты.
- долгота не может быть больше 180 ° восточной долготы.
- долгота не может быть меньше -180 ° западной долготы.
Это пример инварианта класса в языке программирования Java с языком моделирования Java. Инвариант должен сохраняться, чтобы Значение true после завершения работы конструктора и при входе и выходе всех общедоступных функций-членов. Открытые функции-члены должны определять предварительное условие и постусловие, чтобы обеспечить инвариант класса.
Что такое инвариант в ООП?
Очень часто в статьях по ООП встречается такое слово, как инвариант:
- . не позволяет модели обеспечивать собственные инварианты
- убедиться в выполнении предусловия можно исходя из постусловий и инвариантов предшествующих вызовов
- Это кстати называется принципом инварианта. собственно инкапсуляция и позволяет сохранять инвариант.
- То есть независимо от одновременного количества потребителей, она будет сохранять свои инварианты и придерживаться контракта.
- У каждого агрегата есть корень (Aggregate Root) и граница, внутри которой всегда должны быть удовлетворены инварианты.
Что имеется ввиду под этим термином? Как выглядят инварианты в коде?
Я нашёл описание термина «инвариант цикла»:
Инвариант цикла – это соотношение, которое истинно перед циклом, истинно в процессе выполнения цикла и истинно при выходе из цикла. Все это описано у Дейкстры в книге «Дисциплина программирования», и детально разжевано у Гриса в книге «Наука программирования».
А хотелось бы понять, что понимают под инвариантом
- в программировании по контракту и
- чистом ООП (я так понял, это имеет отношение к инкапсуляции)
Инвариант в математике — это выражение которое сохраняет свое значение. В программировании инвариантом также называют предикат который всегда истинный.
Таким образом, инвариант объекта в ООП — это либо (чаще) условие которое остается истинным после вызова любых методов объекта в любой последовательности, либо (реже) выражение которое сохраняет свое значение после вызова любых методов.
В коде инварианты чаще всего никак не выражены, но иногда ставятся защитные проверки которые их проверяют.
Ко-вариантность и типы данных
Тема вариантов в программировании вызывает кучу сложностей в понимании, по мне это проблема в том, что в качестве объяснения берут не всегда успешные метафоры — контейнеры.
Я надеюсь что может у меня получиться объяснить эту тему с другой стороны используя метафоры “присвоения” в разрезе лямбд.
Зачем вообще эта вариантность нужна ?
В целом без вариантности можно жить и спокойно программировать, это не такая уж архиважная тема, у нас есть множество примеров языков программирования в которых это качество не отображено.
Ко-вариантность это о типах данных и их контроле со стороны компиляторов. И ровно с этого места надо откатиться и сказать о типах данных и зачем это нам нужно.
Flashback к типам
Типы данных сами по себе тоже не являются сверхважной темой, есть языки в которых тип данных не особенно нужны, например ассемблер, brainfuck, РЕФАЛ.
В том же РЕФАЛ или ассемблере очень легко перепутать к кому типу относиться переменная, и очень легко, например можно допустить что из одной строки я вычту другую строку, просто опечатка, никакого злого умысла.
В языках с поддержкой типов, компилятор увидел бы это опечатку и не дал бы мне скомпилировать программу, но… например JS
JS (JavaScript) Спокойно этот код проглатывает, мне скажут что это не баг, это фича, ок, допустим, тогда я возьму Python
То есть я клоню к тому, что считать багом или фичей — зависит от создателей языка.
А мне как пользователю например вообще без разницы на каком языке написана та или иная программа, мне важно чтоб она работала.
А как программисту, решающему задачу конкретного пользователя, я выберу тот язык, который будет удобен мне для решения задачи и я не хотел бы сильно заварчиваться на особенности языков, знать особенности работы с тем или иным типом данным.
Еще пример: может быть такой мой сценарий, допустим вчера я написал на Groovy вот такой код
И вот таких не совпадений типов данных может быть много и мне действительно надо знать особенности того или иного языка.
Окей, я понимаю, что я сейчас выдумываю на ходу разные проблемы — но это не значит, что прям сейчас надо бросать известный вам язык и переходить на другой язык программирования.
Речь о типах данных
Вариантность как и ко/контр вариантность — это речь о типах данных и их отношениях между собой.
Некоторые языки программирования создавались, чтобы избежать выше описанных проблем.
Один из способов избежать — это введение системы типов данных.
Вот пример на языке TypeScript
Этот код успешно скомпилируется в JS.
Уже не скомпилируется — и это хорошо:
В примере выше функция sub требует принимать в качестве аргументов переменные определенного типа, не любые, а именно number .
Контроль за типы данных я возлагаю уже компилятору TypeScript ( tsc ).
Инвариантность
Рассмотрим пока понятие Инвариантность, согласно определению
Инвариа́нт — это свойство некоторого класса (множества) математических объектов, остающееся неизменным при преобразованиях определённого типа.
Пусть A — множество и G — множество отображений из A в A. Отображение f из множества A в множество B называется инвариантом для G, если для любых a ∈ A и g ∈ G выполняется тождество f(a)=f(g(a)).
Очень невнятное для не посвященных определение, давай те чуть проще:
Инвариантность — это такое качество операций над данными, при котором тип данных в передаваемых в функцию и возвращаемый тип является один и тем же.
Рассмотрим пример операции присвоения переменной, в JS допускается вот такой код
В примере переменная r — может быть и типа string и number и объектом, со стороны интерпретатора сказать какого типа данных возвращает функция fun1 нельзя, пока не запустишь программу.
Так же нельзя сказать какого типа будет переменная r. Тип результата и тип переменной r зависит от типов аргументов функции.
Переменная r по факту может иметь два разных типа:
В конструкции let r = b , переменная r будет иметь такой же тип, как и переменная b.
В конструкции r = c , переменная r будет иметь такой же тип, как и переменная c.
В целом, такое не определенное поведение может сказаться на последующей логике поведения программы негативно.
Можно наложить явным образом ограничения на вызов функции и проверять какого типа аргументы, например так:
Это уже лучше, хоть об ошибке мы узнаем, во время выполнения, но она уже не приведет к негативным последствиям.
Другой же аспект, в том что операция +, — и др… при операциях над числами — возвращают числа — это и есть инвариантность (в широком смысле), а вот над числами и строками или различными типами данных — результат уже менее предсказуем.
В языках со строгой типизацией операция конструкция let r = b и следующая за ней r = c не допустима, она может быть допустима если мы укажем типы аргументов.
И результат компиляции
Здесь в ошибки говориться явно, что переменная типа string не может быть присвоена переменной типа number .
Вариантность — в компиляторах, это проверка допустимости присвоения переменной одного типа значения другого типа.
Инвариантность — это такой случай, когда переменной одного типа присваивается (другая или эта же) переменная этого же типа.
Теперь вернемся к строгому определению: выполняется тождество f(a)=f(g(a))
То есть допустим у нас есть функции TypeScript:
Этот код — вот прям сторого соответствует определению.
В контексте программирования Инвариантность — это не свойство значения функций, а соответствие типов данных, т.е. вот код ниже абсолютно валиден
Уже невалиден (не корректен), так как:
функция g возвращает тип string
а функция f требует тип number в качестве аргумента
и вот такую ошибку обнаружит компилятор TypeScript.
Первый итог
Вариантность и другие ее формы, как например Ин/Ко/Контр вариантность — это качество операции присвоения значения переменной или передачи аргументов в функцию, в которой проверяется типы данных передаваемых/принимаемых в функцию и переменную.
Ко-вариантность
Для объяснения ко-вариантности и контр-вариантности, мне придется прибегнуть не к TypeScript, а к другому языку — Scala, причины я поясню ниже.
Вы наверно уже слышали про ООП и наследование, про различные принципы Solid
Ко-вариантность обычно объясняют через наследование, и что наследуются все свойства и методы родительского класса — это верно, рассмотрим пару примеров
Ко-вариантность это такое качество операции присвоения значения переменной значение переменной другого типа, при котором сохраняются все свойства и операции. —–
Есть несколько типов чисел и их можно расположить в следующей иерархии:
Натуральные числа N
N натуральные числа, включая ноль:
N* натуральные числа без нуля:
Целые числа Z — обладают знаком (+/-) включают в себя натуральные
Рациональные числа Q — дроби (два целых числа), включают в себя все бесконечное множество Z
Вещественные числа R — это и рациональные и иррациональные числа (например ПИ, e, …)
Комплексные числа C — числа вида a+bi, где a,b — вещественные числа, а i — мнимая единица
Давай те рассмотрим более подробно:
Числа мы можем условно расположить согласно такой иерархии
any — любой тип данных
number — некое число
int — целое число
double — (приближенное) дробное число
так мы можем в языке TypeScript написать функции
Это будет случай инвариантного присваивания, т.к. типы полностью совпадают — результат вызова int, и переменная которая принимает результат то же int.
Рассмотрим случай ко-вариантного присваивания
В данном примере res1 — это тип number.
В первом вызове res1 = sum_of_int( 1, 2 ), переменная res1 примет данные типа int, и это корректно, т.к. int это подтип number и по определению сохраняются все свойства и методы класса number
Во втором вызове res1 = sum_of_double( 1.2, 2.3 ) — переменная res1 примет данные типа double и это тоже корректно, так же по определению
О каких же операциях говорят что сохраняются? а все те же, мы все так же как и в первом, так и во втором случае можем выполнить операции проверки на равенство и д.р. для переменной res1:
ок, это работает, но компилятор нам нужен чтоб он за нас решал проблемы с типами, рассмотрим еще более “выпуклый” пример
Допустим у нас есть фигуры: прямоугольник Box и круг Circle
И нам надо подсчитать сумму площадей, прямоугольники можно хранить в одном массиве, а круги в другом
Мы напишем 2 функции по подсчету площади, одну для прямоугольников, другую для кругов
Тогда для подсчета общей суммы площадей код будет примерно таким:
Все выше выглядит ужасно, если вы знакомы с ООП или/и с базовой логикой (родовые, видовые понятия).
Первое, что должно броситься в глаза — так это что свойство площадь применимо к обеим фигурам, а для подсчета суммы площадей, нет прямой необходимости как-то различать типы фигур.
А по сему можно выделить общее абстрактное понятие Фигура и добавить в это абстрактное метод/свойство — area():number.
Вторым шагом, это указать что классы Box и Circle реализуют интерфейс Shape, и перенести areaOfBox, areaOfCircle как реализацию area.
Теперь нет необходимости разделять прямоугольники и круги в разные массивы, и писать сложный код
И в данном примере, ко-вариантность проявляется в инициализации массива
Массив определен как массив элементов типа Shape, мы инициализируем (т.е. присваиваем начальное значение) элементами другого типа под типа (Box, Circle).
Ключевой момент в том, что Box и Circle реализуют необходимые свойства и методы которые требует интерфейс Shape.
Компилятор отслеживает что присваиваемые значения реализуют заданное соглашение, т.е.
Компилятор по факту отслеживает конструкцию let a = b , и возможны несколько сценариев:
переменная a и b — одного типа, тогда инвариантная операция присвоения
переменная a является базовым типом, а переменная b — подтипом переменной a — тогда ко-вариантная операция присвоения
переменная a является подтипом переменной b, а переменная b — базовым (родительским) типом — тогда это контр-вариантная операция — и обычно компилятор блокирует такое поведение.
между переменными a и b — нет общих связей — и тут компилятор блокирует то же поведение.
И вот пример, по пробуем добавить еще один класс который не реализует интерфейс Shape
Результат компиляции — следующая ошибка:
Для типа Foo не найдено свойство area, которое определенно в типе Shape.
Тут уместно упомянуть о SOLID
L — LSP — Принцип подстановки Лисков (Liskov substitution principle): «объекты в программе должны быть заменяемыми на экземпляры их подтипов без изменения правильности выполнения программы». См. также контрактное программирование.
Контр-вариантность
Контр-вариантность, уже сложнее объяснить, для меня примеры с длегатами действовали на нервы, я же разобрался на примере с лямбд.
В качестве примера, возьму язык Scala и подробно попытаюсь его разобрать:
Что нужно знать о Scala:
Тип Any — это базовый тип для всех типов данных
Тип Int, Boolean, String — это подтипы Any
Лямбды то же являются типами, в смысле типы их аргументов и результатов проверяет компилятор
Тип лямбды записывается в следующей форме: (тип_аргументов,через_запятую)=>тип_результата
Любой метод с легкостью преобразуется в лямбду переменная = класс.метод / переменная = объект.метод
val в Scala, то же что и const в JS
В примере мы можем увидеть уже знакомые
Инвариантность в присвоении переменных:
cmp1 — это переменная содержащая лямбду, при том аргументы и результат которые заданы в определении типа лямбды, полностью совпадают с присваемым значением:
Ко-вариантность
Если в случае присвоения call2, тут все понятно, то может быть непонятно с cmp2.
Внезапно отношение String -> к -> Any становится другим — контр-вариантным.
В этом месте, уместно задаться WTF? — Все нормально!
Рассмотрим функции выше
При вызове cmp2( «abc» ) аргумент «abc» будет передан в anyCmp(a:Any) , а по скольку String является под типом Any, то аргумент не дано преобразовывать и можно передать как есть.
Иначе говоря вызов anyCmp( «string» ) и anyCmp( 1 ) , anyCmp( true ) — со стороны проверки типов допустимы операции, по скольку
принимаемые аргументы являются подтипами для принимающей стороны, тела функции
тип принимаемого аргумента является родительским типом (надтипом) со стороны вызова функции
Т.е. можно при передаче аргументов, действуют ко-вариантность со стороны принимающей, а со стороны передающей контр-вариантность.
Еще более наглядно это можно выразить стрелками:
Операция присвоения должна быть ко-вариантна или инвариантна
А операция вызова функции на оборот — контр-варианта или инвариантна
Этим правилом руководствуются многие компиляторы, и они определяют функции так:
Операции передачи аргументов в функции по умолчанию являются контр-вариантны, со стороны вызова функции
Операции присвоения результат вызова функции по умолчанию является ко-вариантны, со стороны вызова функции
Я для себя запомню так
Почему Scala, а не TypeScript
К моему удивлению TypeScript версии 4.2.4 не отрабатывает контр-вариантность в случае функций/лямбд
Вот мой исходник
В строке const f3 : (any)=>boolean = f1; и в const _f3 : (Shape)=>boolean = _f1 (а так же предыдущей) компилятор по моей логике должен был ругаться, но он этого не делал
Потому пришлось взять язык с более жесткой проверкой типов, надеюсь в новых версиях исправят этот баг.
Ко-вариантность/Контр-вариантность и типы
Еще одна важная оговорка связанная с типами и ООП.
Вариантность это не только про иерархию наследования!
В примере о прямоугольнике и круге, я целенаправленно задействовал интерфейсы, хотя обычно используют общий базовый класс.
Ко-Вариантность — это такое качество операции присвоения, когда целевой тип переменной совместим с исходным типом значения.
Контр-вариантность — ровно та же ситуация с противоположным знаком.
Тут надо дать пояснение слова совместимость
Пример с кругами и прямоугольниками может быть написан на языке C или ассемблера, или JS ранних версий, в которых нет понятия классов, но при этом оно все так же будет работать.
ООП с наследованием — это всего лишь способ, задать иерархию реальных типов объектов.
В ряде языков был введен запрет на множественное наследование, и это я не могу назвать большим достижением, оно порождает проблемы.
Например я могу выстроить разные наборы иерархий для одних и тех же сущностей:
Человек (общий класс)
Национальность (под класс)
Социальный статус (под класс)
Человек (общий класс)
Социальный статус (под класс)
Это я клоню к тому, что для одной и той же сущности может существовать множество способов квалификации.
И один из подходов — эту сложную сущность (как например человек) можно рассматривать с различных сторон — и вот уже эти стороны можно выделить в виде интерфейсов.
А уже в рамках того или иного интерфейса описывать интересующие свойства и методы для решения практических задач.
Вариантность — это в первую очередь наличие интересующих нах свойств/методов для наших задач. И это механизм контроля со стороны компилятора, для гарантии наличия этих свойств.
Так, например тот или иной объект может быть не только каким либо под классом, но и реализовывать (через интерфейсы) интересующие нас свойства/методы — именно это я понимаю под словом совместимость.
Далее можно вести разговор о множественном наследовании, трейтах, и прочих прелястях современных языков, но это уже выходит за рамки темы.