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

Основная идея подхода Хоара – доказывать корректность программ на синтаксическом уровне, используя лишь тройки определенной выше формы. Детерминированные последовательные программы конструируются по следующей грамматике:

S ::= skip | x := E | S; S | if B then S else S fi | while B do S od.

Здесь skip – отсутствие операции, x := E – присваивание выражения E переменной x (предполагается, что x и E имеют одинаковый тип), S; S

– композиция операторов. Последние два – альтернатива и итерация, соответственно (B – булево выражение).

Правила вывода должны читаться следующим образом: если все условия, расположенные выше черты, верны, тогда следствие под чертой тоже верно. Для правил с условием true записывается только следствие. Эти правила вывода называются аксиомами. Формальная система для последовательных детерминированных программ изображена в табл. 1.

 

Таблица 1. Формальная система для частичной корректности последовательных программ.

Аксиома для skip
Аксиома для  присваивания
Последовательная  композиция
Альтернатива
Итерация
Следствие

 

Правило вывода для оператора skip, который ничего не делает, вполне ожидаемо: при любых условиях, если φ верно перед оператором, то оно верно и после него.

В соответствии с аксиомой для присваивания, начинают с постусловия φ и определяют предусловие подстановкой φ[x := k]. Эта подстановка означает формулу φ, в которой во всех вхождениях  x заменено на k. Например,

{k² четно и k = y} x := k {x² четно и x = y}.

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

Правило последовательной композиции использует промежуточный предикат χ, который характеризует финальное состояние S₁  и стартовое состояние S₂.

Правило альтернативы использует булево выражение B, значение которого определяет, что именно исполняется: S₁ или S₂.

Правило для итерации требует пояснения. Оно  определяет, что предикат  φ  выполняется после окончания while B do S od, если справедливость φ  может быть поддержана в течение каждого исполнения тела цикла S. Это объясняет, почему φ  называется инвариантом. Одна из основных трудностей в доказательстве правильности программ с помощью рассматриваемого подхода состоит в нахождении подходящих инвариантов. В частности, это усложняет автоматизацию таких доказательств.

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

Правило следствия позволяет усиливать предусловия и ослаблять постусловия. При этом оно облегчает применение остальных правил. В частности, это правило позволяет заменять  пред- и постусловия эквивалентными. Тем не менее, следует отметить, что доказательство импликаций вида φ Þ φ' в общем случае неразрешимо.

Теперь обсудим тотальную корректность. Системы доказательств в табл. 1 недостаточно для доказательства того, что последовательная программа останавливается. Единственная синтаксическая конструкция, которая  может вести к зависающим (не останавливающимся) вычислениям, – это итерация. Для доказательства наличия останова можно усилить правило вывода для итерации следующим образом:

Здесь вспомогательная переменная N не входит в φ, B, n или S. Смысл этого правила заключается в том, что N является стартовым значением n, и на каждой итерации значение n уменьшается, но остается неотрицательным. Эта конструкция в точности ликвидирует бесконечные вычисления, так как n не может уменьшаться бесконечно часто без нарушения условия n ≥ 0. Переменная n называется вариантой.

 

 

Автоматическая  генерация и доказательство условий  корректности

 

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

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

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

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

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

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

Рисунок 1 – Типовая схема верификатора.

 

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

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

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

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

1. Все условия верификации истинны. Работа завершается.
2. Доказательство отдельных условий верификации не завершено. Такие условия возвращаются на доказательство с применением дополнительной информации (аксиом пользователя), вводимой пользователем в ходе работы верификатора.
3. Среди условий верификации обнаружены ложные. В этом случае ошибки могут быть как в спецификации программы, так и в операторах самой программы, причем формально разделить эти ситуации невозможно. Пользователь может выполнить модификацию аннотированной программы и повторить всю процедуру ее обработки.

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

 

 

 

Специфика верификации  недетерминированных и параллельных программ

 

Одной из основных проблем параллельной отладки является недетерминизм, вольно или невольно вносимый программистами в код. Недетерминизм играет важную роль в области параллельных и распределенных вычислений. С одной стороны программа, с детерминированным поведением обладает исключительными для многих областей применения свойствами, и исследователи считают, что надежное программное обеспечение должно быть детерминированным [10]. С другой, — использование недетерминированных коммуникационных операций позволяет повысить степень параллелизма в программе за счет снятия жестких ограничений на порядок обмена данными между процессами. Как следствие, недетерминизм позволяет достигнуть более высокой производительности и полнее использовать потенциальные возможности параллельной вычислительной системы.

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

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

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

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

Источники недетерминизма достаточно разнообразны:

• неравномерная загрузка узлов вычислительной системы;

• влияние менеджера процессов операционной системы на каждом узле;

• механизм виртуальной памяти;

• задержки и конфликты в сети.

В MPI программах влияние этих источников проявляется  в последовательности приема сообщений  для тех операций MPI Recv (и аналогичных), где передающий процесс определяется по маске (например, MPI ANY SOURCE), а также результатах выполнения асинхронных операций. Кроме того, недетерминизм выполнения программы (как параллельной, так и последовательной) может вызываться обращением к различным системным функциям, таким как генератор псевдослучайных чисел.

Недетерминизм программы требует от отладочных средств функциональных возможностей по решению следующих задач:

1. воссоздание  поведения параллельной программы,  записанного на стадии тестирования, для повторного детерминированного выполнения. В противном случае ошибка, обнаруженная на тестовом наборе, может не проявиться при выполнении программы под отладчиком;

2. анализ всех  теоретически возможных вариантов  выполнения недетерминированной  параллельной программы. В силу наличия точек недетерминизма параллельная программа допускает изменение порядка передаваемых сообщений между процессами, при этом выполнение программы должно приводить к корректным результатам;

3. минимизация  влияния отладочных средств на поведение отлаживаемой программы.

 

 

Литература

 

1. Котов В.Е., Сабельфельд В.Н. Теория схем программ. – М.: Наука, 1991, 247 с.
2. Грис Д. Наука программирования. — М.: Мир, 1984, 416 с.
3. Роганов Е.А. Основы информатики и программирования. — М.: МГИУ, 2001, 315 с.
4. Непомнящий В.А., Рокин А.М. Прикладные методы верификации программ. — М.: Радио и связь, 1988, 255 с.
5. Агафонов В.Н. Спецификация программ: понятийные средства и их организация. — Новосибирск: Наука, 1990.
6. Лисков Б., Гатэг Г. Использование абстракций и спецификаций при разработке программ. — М.: Мир, 1989, 424 с.
7. Хоар Ч. Взаимодействующие последовательные процессы. — М.: Мир, 1989, 264 с.
8. Гордеев В.А., Молчанов А.Ю. Системное программное обеспечение. — СПб.: Питер, 2002, 736 с.
9. Питерсон Дж. Теория сетей Петри и моделирование систем. — М.: Мир, 1984, 264 с.
10. Котов В.Е. Сети Петри. — М.: Наука, 1984, 158 с.