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

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

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

Идея разработки программы вместе с ее доказательством возникла у Э. У. Дейкстры . Написание инвариантов перед операторами программы в различных формах рассматривалось М. ​​Х. ван Эмденом, Дж. К. Рейнольдсом и Р. Дж. Бэком .

См. также

• Эйфель (язык программирования)