Автоматизация верификации C-программ с использованием символического метода элиминации инвариантов циклов

При дедуктивной верификации программ, написанных на императивных языках программирования, особую сложность вызывает порождение и доказательство условий корректности, соответствующих циклам, поскольку каждый из них должен быть снабжён инвариантом, построение которого часто является нетривиальной задачей. Методы синтеза инвариантов циклов, как правило, носят эвристический характер, что затрудняет их применение. Альтернативой является символический метод элиминации инвариантов циклов, предложенный В.А. Непомнящим в 2005 году. Его идея состоит в представлении тела цикла в виде специальной операции замены при выполнении определённых ограничений. Такая операция в символической форме выражает действие цикла, что позволяет ввести в аксиоматическую семантику правило вывода для циклов, не использующее инварианты. В данной работе представлено дальнейшее развитие этого метода. Он расширяет метод смешанной аксиоматической семантики, предложенный для верификации C-light программ. Данное расширение включает в себя метод верификации итераций над изменяемыми массивами с возможным выходом из тела цикла в C-light программах. Метод содержит правило вывода для итерации без инвариантов циклов. Данное правило было реализовано в генераторе условий корректности, являющемся частью системы автоматизированной верификации C-light программ. Для проведения автоматического доказательства в используемой системе ACL2 были разработаны и реализованы два алгоритма: первый порождает операцию замены на языке системы ACL2, а второй генерирует вспомогательные леммы, позволяющие системе ACL2 успешно доказать получаемые условия корректности в автоматическом режиме. Применение вышеуказанных методов и алгоритмов проиллюстрировано примером.