Автоматизация верификации программ
Автоматизация верификации программ
Верификация программ - трудоемкий процесс, и его целесообразно автоматизировать. Проблемы корректности программы алгоритмически неразрешимы, поэтому не следует рассчитывать на полную автоматизацию. Не могут быть автоматическими аннотирование программы и доказательство условий верификации. Синтез инвариантов циклов можно автоматизировать, однако на практике этого не делают из-за ограниченности разработанных методов. Генерацию условий верификации можно выполнять автоматически. В связи с этим применение компьютеров для верификации программ в настоящее время идет преимущественно по пути создания автоматизированных систем верификации, предусматривающих диалог с пользователем на некоторых этапах работы. Для краткости будем называть такую программу верификатором. Типовая схема верификатора показана на рисунке 2.4.
На вход системы поступает подготовленная пользователем аннотированная программа. В ней, в частности, предусмотрены формулы логического языка спецификации для входного и выходного условий программы, а также инвариант для каждого цикла.
В ходе анализа программы выполняется контроль лексической и синтаксической правильности аннотированной программы подобно тому, как это делается в трансляторах. Программа переводится на промежуточный язык. В качестве такого языка обычно используется одна из форм бесскобочной записи. Анализ аннотированной программы выполняется автоматически.
Рисунок 2.4 – Типовая схема верификатора
Генерация условий верификации основана на применении аксиоматической системы используемого языка программирования и также осуществляется без участия пользователя. Имеются два альтернативных алгоритма генерации условий верификации: алгоритм прямого прослеживания и алгоритм обратного прослеживания. Алгоритм прямого прослеживания строит формулы условий, просматривая программу от начала к концу. При этом в соответствии с семантикой операторов программы их предусловия преобразуются в постусловия. Обратное прослеживание происходит от конца программы к ее началу и предполагает последовательное преобразование постусловий операторов в их предусловия. Естественно, правила вывода, образующие аксиоматическую систему одного и того же языка программирования, будут различны для разных алгоритмов прослеживания.
При доказательстве условий верификации могут выполняться некоторые эквивалентные преобразования и упрощения условий верификации. Например, арифметические и логические выражения приводятся к канонической форме, определенные части выражений замещаются логическими константами и т.д. Каноническая форма арифметического выражения - это упорядоченная сумма произведений. Логическое выражение представляется как последовательность конъюнкций более простых выражений, не содержащих других логических операций, кроме отрицания. В некоторых случаях элементарные упрощения позволяют убедиться в истинности отдельных условий верификации.
На этом этапе могут также вычисляться истинностные значения тех частей условий верификации, которые сформулированы в рамках достаточно простых аксиоматических теорий. Подстановка результатов таких вычислений в условия верификации позволяет упростить их, а в ряде случаев доказать или опровергнуть. При необходимости возможно применение системы аксиом пользователя.
Результаты доказательства условий верификации исследуются анализатором доказательства. Он может обнаружить следующие ситуации.
1 Все условия верификации истинны. Работа завершается.
2 Доказательство отдельных условий верификации не завершено. Такие условия возвращаются на доказательство с применением дополнительной информации (аксиом пользователя), вводимой пользователем в ходе работы верификатора.
3 Среди условий верификации обнаружены ложные. В этом случае ошибки могут быть как в спецификации программы, так и в операторах самой программы, причем формально разделить эти ситуации невозможно. Пользователь может выполнить модификацию аннотированной программы и повторить всю процедуру ее обработки.
Принятие окончательных решений в ходе анализа верификатором результатов доказательства возлагается на пользователя.