Почему инварианты важны в информатике

Я понимаю «инвариант» в его буквальном смысле. Я также узнаю их, когда набираю код. Но я не думаю, что понимаю значение этого термина в контексте информатики.

Всякий раз, когда я читаю разговоры \ официальные документы о языковом дизайне от известных программистов \ компьютерных ученых, термин «инвариант» появляется как жаргон; и это та часть, которую я не понимаю. Что такого особенного в этом?

Алгоритм - это повторяемый процесс. Если оно повторяется, оно должно иметь атрибуты, которые не меняются при повторении. Это ваши инварианты. Инварианты объединяются и / или оперируют (потенциально) изменяющимися данными, которые будут вводиться в ваш алгоритм.

Таким образом, весь смысл программирования состоит в том, чтобы определить, что не меняется - это, по сути, ваша программа.

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

Понятие инварианта тесно связано с «побочными эффектами». Я считаю, что этому способствовал подход Бертранда Мейера «Проектирование по контракту (DbC)» для разработки программного обеспечения.

DbC обогащает абстрактные типы данных (основу классов) тремя важными понятиями, предусловиями, постусловиями, инвариантами . Это легко объяснить при обращении к процедурам, поэтому я попытаюсь объяснить в связи с этим:

1. Предварительное условие представляет входные данные условия для процедуры, которые должны соблюдаться для вызова этой процедуры. Это предварительное условие должно соблюдаться и соблюдаться клиентом этой конкретной процедуры. Однако разработчик процедуры может защищать от клиентов, которые не соблюдают предварительное условие, утверждая это условие в качестве первых строк процедуры. Например, наличие метода double divide(double dividend, double divisor)является предварительным условием divisor != 0.

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

3. Инвариант можно рассматривать как как предпосылку и послеусловие, но с разным пониманием для предусловия и постусловия из вышеуказанных понятий. Инвариант в основном говорит, что если вход имеет определенное условие, выполненное до того, как была вызвана процедура, то это конкретное условие является действительным после вызова процедуры. Например, действительный инвариант для процедуры boolean search(int term, int array[])может сказать, что состояние arrayперед вызовом такое же, как и после вызова.

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

Инвариант - это логическое свойство, которое сохраняется некоторыми операциями.

• Вам нужны инварианты, чтобы рассуждать о циклах. Поскольку вы заранее не знаете, сколько будет итераций (или вам не понадобится цикл), каждая итерация должна сохранять инвариант, чтобы в конце вы могли доказать какое-то полезное свойство цикла.

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

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

В контексте системы типов языка программирования инвариантный тип является неконвертируемым типом. Например, в java при перегрузке метода все параметры являются инвариантными, а возвращаемый тип - ковариантным (может быть одинаковым или подтипом).