Что такое инварианты, как их можно использовать, и использовали ли вы их когда-либо в своей программе?

48

Я читаю Coders at Work , и в нем много говорят об инвариантах. Насколько я понял, инвариант - это условие, которое выполняется до и после выражения. Они, помимо прочего, полезны для доказательства правильности цикла, если я правильно помню курс по логике.

Мое описание верно, или я что-то пропустил? Вы когда-нибудь использовали их в своей программе? И если да, то как они выиграли?

gablin
источник
@ Роберт Харви: Да, я только что прочитал это на самом деле. Но мне кажется, что инварианты полезны только тогда, когда вы пытаетесь что-то доказать. Это правильно (не каламбур)?
Габлин
Это мое понимание; когда вы пытаетесь рассуждать о своей программе, чтобы доказать ее правильность.
Роберт Харви
3
@ user9094: Утверждение - это объявление, что что-то истинно в определенный момент времени выполнения и представлено в коде. Инвариант - это утверждение (можно надеяться, что оно обосновано), которое всегда будет верным, когда бы оно ни применялось, и не будет представлено в самом коде.
Дэвид Торнли
1
Инварианты действительно полезны для доказательства правильности, но они не ограничиваются этим случаем. Они также полезны для защитного программирования и во время отладки. Они не только помогают доказать, что ваш код корректен, но и помогают понять код и найти расположение ошибок, близких к исходным.
Нечетное

Ответы:

41

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

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

Я иногда использую функцию-член объекта, чтобы проверить, что инвариант держится. Если это не так, утверждается. И метод вызывается в начале и выходе каждого метода, который изменяет объект (в C ++ это только одна строка ...)

Ксавье Ноде
источник
11
+1 для упоминания инвариантов не обязательно должно быть правдой в середине исполняемого метода.
Нечетное
1
@ Нечетное мышление Лучше всего избегать этого, когда это возможно. Было бы легко войти в неизменное состояние и забыть восстановить все правильно, прежде чем вернуться. Исключения также могут доставить вам неприятности.
Александр
3
@ Александр: Для нетривиальных инвариантов этого почти невозможно избежать. Если вам необходимо обновить более одной переменной в методе, как описано в ответе, существует момент, когда обновлена ​​только одна переменная, а инвариант имеет значение false. Есть достаточно ограничений на написание хорошего кода без добавления новых.
Странное мышление
@ Странно, да, это часто совершенно неизбежно. Но, например, если есть группа переменных, которые логически связаны друг с другом (например, массив и индекс «выбранного» элемента в массиве), то, вероятно, стоит выделить их в тип. Оттуда, мутации массива или типа могут быть выражены как одно присваивание нового экземпляра этого типа
Александр
13

Хорошо, материал, который я вижу в этой теме, великолепен, но у меня есть определение «инварианта», которое мне очень помогло на работе.

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

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

Также это определение полезно, потому что оно позволяет использовать обобщение «Инварианты плохие».

Например, механизм переключения передач в автомобиле с механической коробкой передач спроектирован так, чтобы избежать инварианта. Если бы я хотел, я мог бы построить трансмиссию с одним рычагом для каждой передачи. Этот рычаг может быть вперед («включен») или назад («отключен»). В такой системе я создал «инвариант», который можно задокументировать так:

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

И так, можно было бы обвинить сломанные передачи на небрежном вождении. Современные автомобили, однако, используют одну палку, которая вращается среди передач. Он сконструирован таким образом, что на современном автомобиле с переключением передач невозможно задействовать две передачи одновременно.

Таким образом, мы могли бы сказать, что передача была разработана для «удаления инварианта», потому что она не позволяет механически конфигурировать себя таким образом, который нарушает логическое правило.

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

Даниэль Бербанк
источник
1
Если инвариантом является любое логическое правило, которому необходимо следовать на протяжении всего выполнения вашей программы, и ваше логическое правило заключается в том, что нельзя одновременно задействовать две шестерни, то не является инвариантом, что две шестерни не могут быть задействованы одновременно время? Без этого инварианта ваша передача может быть на двух передачах одновременно и, таким образом, разорвется на части. Во-первых, разве один сдвиг палки фактически не обеспечивает этот инвариант? Во-вторых, почему инвариант должен быть хорошим или плохим?
Дастин Кливленд
1
Сравнение с автомобильными передачами мне очень понятно. Спасибо!
Мареки
«Инвариант - это любое логическое правило, которому необходимо следовать при выполнении вашей программы, которое может быть передано человеку, но не вашему компилятору». - Мне это очень нравится, лаконично и легко запоминается.
ZeroKnight
@DustinCleveland Я думаю, что в этом примере механизмы, стоящие за сдвигом палочек, являются «компилятором», который «обеспечивает соблюдение» правил, тогда как драйвер, который в противном случае мог бы вызвать инцидент, является одним из многих клиентов, которые должны потреблять и запоминать информацию, были «задокументированы, обсуждены, прокомментированы или иным образом переданы».
Эбернард
Блестящее объяснение! Теперь я действительно понимаю, почему наличие инвариантов в вашем коде - плохая практика.
Бен С Ван
3

Инвариант (в обычном смысле) означает некоторые условия, которые должны выполняться в определенный момент времени или даже всегда, когда ваша программа выполняется. Например, PreConditions и PostConditions могут использоваться для утверждения некоторых условий, которые должны быть истинными, когда функция вызывается и когда она возвращается. Инварианты объекта могут использоваться для подтверждения того, что объект должен иметь действительное состояние в течение всего времени его существования. Это дизайн по принципу контракта.
Я использовал инварианты неформально, используя проверки в коде. Но в последнее время я играю с библиотекой контрактов кода для .Net, которая напрямую поддерживает инварианты.

softveda
источник
3

Основываясь на следующей цитате из Coders At Work ...

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

... Я думаю, "invariant" = "условие, которое вы хотите поддерживать, чтобы обеспечить желаемый эффект".

Кажется, что инвариант имеет два смысла, которые отличаются тонким способом:

  1. Что-то, что остается прежним.
  2. Что-то, что вы пытаетесь сохранить прежним, чтобы достичь цели X (например, «время просмотра журнала» выше).

Так что 1 похоже на утверждение; Я думаю, что 2 - это инструмент для проверки правильности, производительности или других свойств. См. Статью Wikipedia для примера 2 (доказательство правильности решения головоломки MU).

На самом деле третье чувство инварианта это:

0,3. Что должна делать программа (или модуль или функция); другими словами, его цель.

Из того же интервью Coders At Work:

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

Джонатан Акино
источник
1

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

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

Это может быть запись в БД или что-то еще, но сейчас давайте предположим, что каждая учетная запись пользователя представлена ​​объектом класса.

class userAccount {private char * pUserName; private char * pParentAccountUserName;

...}

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

Pemdas
источник
Инварианты проверяют состояние программы. Они не дизайнерские решения.
Ксавье Нодет
3
Инварианты ничего не проверяют. Вы можете проверить состояние программы, чтобы увидеть, является ли инвариант ИСТИНА или ЛОЖЬ, но сами инварианты ничего не делают.
Pemdas
2
Как правило, в C ++ вы увидите некую инвариантность класса, такую ​​как член x должен быть меньше 25 и больше 0. Это инвариант. Любые проверки этого инварианта являются утверждениями. В приведенном выше примере мой инвариант: если pParentAccountUserName равно NULL или пусто, то это родительская учетная запись. Инварианты - это продуманные решения.
Пемдас
Как проверить, что если pParentAccountUserName имеет значение NULL или пусто, этот объект является родительской учетной записью? Ваше утверждение определяет только то, что должно представлять нулевое / пустое значение. Инвариант заключается в том, что система соответствует этому, то есть pParentAccountUserName может быть пустым или пустым, только если это родительская учетная запись. Это тонкое различие.
Кэмерон
1

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

Поэтому, как правило, эти вещи важны как проверки работоспособности, но сами по себе они не могут доказать правильность.

Омега Центавра
источник
1
-1 Инварианты в физике разные. Вычисление решения - это не то же самое, что доказательство правильности алгоритма. Для последнего инварианты могут оказаться правильными.
Ааронастерлинг