Автоматизация верификации программ

• Верификация программ – метод установления правильности программ при помощи строгих средств.
• При этом программа будет считаться правильной, если решит поставленную задачу.
• В основе метода верификации лежит предположение о том, что существует некоторая программная документация, соответствие которой нужно доказать.

• Верификация программ - трудоемкий процесс, и его целесообразно автоматизировать. Проблемы корректности программы алгоритмически неразрешимы, поэтому не следует рассчитывать на полную автоматизацию.

Нельзя автоматизировать:

• процесс аннотирования программы
• доказательство истинности условий верификации.
• Синтез инвариантов циклов можно автоматизировать, однако на практике этого не делают из-за ограниченности разработанных методов. Генерацию условий верификации можно выполнять автоматически.

 

• В связи с этим применение компьютеров для верификации программ в настоящее время идет преимущественно по пути создания автоматизированных систем верификации, предусматривающих диалог с пользователем на некоторых этапах работы. Такие программы также называют  верификаторами.

 

 

• На вход системы поступает подготовленная пользователем аннотированная программа. В ней предусмотрены формулы логического языка спецификации для входного и выходного условий программы, а также инвариант для каждого цикла.

 

• В ходе анализа программы выполняется контроль лексической и синтаксической правильности аннотированной программы подобно тому, как это делается в трансляторах. Затем программа переводится на промежуточный язык, в качестве которого обычно используется одна из форм бесскобочной записи. Анализ аннотированной программы выполняется автоматически.

• Генерация условий верификации основана на применении аксиоматической системы используемого языка программирования и также осуществляется без участия пользователя.

 

Аксиоматической системой называется способ задания множества путем указания исходных элементов (аксиом исчисления) и правил вывода, каждое из которых описывает, как строить новые элементы из исходных элементов.

• Имеются два альтернативных алгоритма генерации условий верификации:
• алгоритм прямого прослеживания;
• алгоритм обратного прослеживания.

• Алгоритм прямого прослеживания строит формулы условий, просматривая программу от начала к концу. При этом в соответствии с семантикой операторов программы их предусловия преобразуются в постусловия.
• Обратное прослеживание происходит от конца программы к ее началу и предполагает последовательное преобразование постусловий операторов в их предусловия. Естественно, правила вывода, образующие аксиоматическую систему одного и того же языка программирования, будут различны для разных алгоритмов прослеживания.

 

 

• При доказательстве условий верификации могут выполняться некоторые эквивалентные преобразования и упрощения условий верификации. Например, арифметические и логические выражения приводятся к канонической форме, определенные части выражений замещаются логическими константами и т.д.

 

• Каноническая форма арифметического выражения - это упорядоченная сумма произведений. Логическое выражение представляется как последовательность конъюнкций более простых выражений, не содержащих других логических операций, кроме отрицания. В некоторых случаях элементарные упрощения позволяют убедиться в истинности отдельных условий верификации.

 

Результаты доказательства условий верификации исследуются анализатором доказательства. Он может обнаружить следующие ситуации:

• Все условия верификации истинны. Работа завершается.
• Доказательство отдельных условий верификации не завершено. Такие условия возвращаются на доказательство с применением дополнительной информации (аксиом пользователя), вводимой пользователем в ходе работы верификатора.

 

 

• Среди условий верификации обнаружены ложные. В этом случае ошибки могут быть как в спецификации программы, так и в операторах самой программы, причем формально разделить эти ситуации невозможно. Пользователь может выполнить модификацию аннотированной программы и повторить всю процедуру ее обработки.

 

• Принятие окончательных решений в ходе анализа верификатором результатов доказательства возлагается на пользователя.