Инварианты, о которых речь здесь выше во всей теме, условно можно отнести к "зависимым типам" ("dependent types" или "liquid types" и прочие вариации). Часто в ООП-среде это дело обзывается как программирование (или моделирование) "по контрактам" и т.п. В общем, термины всякие "резиновые", и речь не о теоретических изысках. Прежде всего, имеется ввиду контракты, зависимые от данных или состояния. Однако, есть пласт инвариантов, где эта зависимость от состояния косвенная или скрытая.
Первый такой слой в программистском жаргоне -- "typestate". Упрощенно, для типа с набором операций важен порядок их применения, и этот порядок задаётся как интерфейс типа. К примеру, в языке Rust попытка реализации typestate провалилась:
http://pcwalton.github.io/blog/2012/12/ ... e-is-dead/Есть проект Vault от MS, расширение для С:
https://www.microsoft.com/en-us/researc ... pldi01.pdfгде объект представляется виртуальным автоматом (попутно в Vault решается и задача управления памятью).
В принципе, можно "выкручиваться" косвенно, как, например, в Dafny имеются ghost-переменные, вводимые лишь для верификации (т.е. "физически" не включаются в тип), и с их помощью в предусловии метода можно контролировать допустимость исполнения. Тем не менее, порядок операций "клиент" типа всё равно вынужден как-то понимать. К тому же механизмы аля ghost-переменных -- сугубо внутренняя реализация типа (для всяких целей, в т.ч. и верификации, тестирования и пр.) и не должны быть в интерфейсе.
Ещё пример (на базе языка Lustre из платформы Esterel, разбираемой здесь на форуме по соседству):
https://pdfs.semanticscholar.org/f570/9 ... 83acca.pdfгде контракт м.б. определен и автоматически как часть вывода типа.
Контракты "typestate" выше -- односторонние, или контракты ресурса. Для двусторонних и более возникает новый пласт -- "session types". Здесь собраны не мало тематических ресурсов:
http://simonjf.com/2016/05/28/session-t ... tions.htmlПо ссылке выше основные решения на базе пи-исчисления процессов. Поэтому там явный "message passing". Контракты -- через системы типов в языке, формулы сессий или спец-языки как Scribble. Последний набирает популярность, имеются всякие расширения аля Parameterised Scribble:
https://groups.inf.ed.ac.uk/abcd/meetin ... las-ng.pdfИли ещё параметры-атрибуты (для анализа времени и др.):
http://mrg.doc.ic.ac.uk/publications/ti ... /paper.pdfКстати, именно в рамках контрактов "type state" и "session types" уже проблематично игнорировать основную пакость для верификаторов. Грубо говоря, анализатор может отслеживать переменную и следить за семантикой вычислений, но когда переменная "улетает", напр., "помещается" в контейнер -- всё, приехали. Когда как в сессиях "разрыв" типа, фактически, неизбежен, или должен быть предусмотрен. Для примера -- реализация "сессионных типов" для Java:
https://www.doc.ic.ac.uk/~rhu/sessionj/ ... safe10.pdfгде на борту run-time механизмы ("typecase" и др.). Или же см. примеры для OCaml, Rust, Scala и др. (в статье-сборнике по сессионным типам по ссылке выше), где "выкручиваются" через статические "хаки" для своих систем типов в языке.
В общем, проблема верификации далеко не только в том, где задавать контракты (в комментариях или нет, согласно соседней теме форума про "виртуальный текст"). И конечно же, жизнь проще, если для всего иметь один язык (как Lustre-like, где программа (верифицируемая) есть и модель взаимодействия процессов, в т.ч. и как контракт для их возможного "разделения").