Инвариантное программирование

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

В императивных языках программирования основные организующие структуры — это блоки управления потоком выполнения, такие как цикл со счётчиком (for), цикл с предусловием (while) и условные операторы (if). Такие языки плохо подходят для инвариантного программирования, поскольку они принуждают программиста принимать решения об управлении потоком до написания инвариантов. Более того, такие языки программирования не имеют нужной поддержки для описания спецификаций и инвариантов, поскольку в них нет кванторов и они не могут выражать свойства высшего порядка.

Идея разработки программы совместно с её доказательством восходит к идеям Э. Дейкстры. Написание инвариантов перед блоком операторов описывалось в том числе такими исследователями как M. H. van Emden, John C. Reynolds и Ralph-Johan Back.

Литература

• Лисков Б., Гатэг Дж. Использование абстракций и спецификаций при разработке программ. М.: Мир, 1989. — 424 с.
• Back, Ralph-Johan: Invariant Based Programming: Basic approach and Teaching Experience, Formal Aspects of Computing, 14 February 2008, ISSN 0934-5043 (Print) 1433-299X (Online)