Введение

Инвариантное программирование — это методология программирования, в которой спецификации и инварианты записываются до фактических операторов программы. Запись инвариантов в процессе программирования имеет ряд преимуществ: она требует от программиста четко сформулировать свои намерения относительно поведения программы до её реализации, а инварианты могут динамически проверяться во время выполнения для выявления распространенных ошибок программирования. Более того, если инварианты достаточно сильны, они могут быть использованы для доказательства корректности программы на основе формальной семантики операторов программы. Для полной верификации нетривиальных программ обычно требуется комбинированный язык программирования и спецификаций, подключенный к мощной системе формального доказательства. В этом случае возможна и высокая степень автоматизации доказательств. В большинстве существующих языков программирования основными структурами организации кода являются блоки управления потоком, такие как циклы for, циклы while и операторы if. Такие языки могут быть не оптимальны для программирования, основанного на инвариантах, поскольку они вынуждают программиста принимать решения о потоке управления до записи инвариантов. Кроме того, большинство языков программирования не обеспечивают хорошей поддержки для записи спецификаций и инвариантов, поскольку в них отсутствуют кванторы и обычно невозможно выразить свойства высшего порядка. Идея разработки программы вместе с её доказательством принадлежит Э. В. Дейкстре. Фактическое написание инвариантов перед операторами программы в различных формах рассматривалось М. Х. ван Эмденом, Дж. К. Рейнольдсом и Р. Дж. Бэком.