ПРОГРАММИРОВАНИЕ, 2008, № 6, с. 5-23
■ ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ
УДК 004.92+004.94
О ГЕНЕРАЦИИ УСЛОВИЙ КОРРЕКТНОСТИ ДЛЯ ИМПЕРАТИВНЫХ ПРОГРАММ*
© 2008 г. Н. В. Шилов, И. С. Ануреев, Е. В. Бодин
Институт систем информатики СО РАН 630090 Новосибирск, пр. Лаврентьева, 6 E-mail: shilov@iis.nsk.su, anureev@iis.nsk.su, bodin@iis.nsk.su Поступила в редакцию 21.04.2008 г.
Верификация императивных программ по Флойду-Хоару - подход к доказательству корректности программ, аннотированных предусловиями, постусловиями и инвариантами циклов, основанный на генерации условий корректности. В структурном детерминированном случае задача генерации условий корректности кажется тривиальной, так как решается синтаксически-управляемым алгоритмом, сложность которого линейна по числу управляющих конструкций. Напротив, в неструктурированном и недетерминированном случае априорно кажется, что сложность генерации условий корректности экспоненциально зависит от числа операторов программы. В статье представлен и обоснован эффективный и полный алгоритм генерации условия корректности, который может использоваться в обоих случаях (то есть в неструктурированном недетерминированном так же, как в структурном детерминированном). Сложность алгоритма линейно зависит от числа управляющих конструкций и/или операторов программы.
1. ВВЕДЕНИЕ
Формальная верификация программ - это математически строгое доказательство корректности программ. Верифицирующий компилятор -это системная программа, которая не только транслирует программу на исходном языке в эквивалентный исполняемый машинный код, но и автоматически верифицирует исходный код. По мнению А. Хоара [1], разработка верифицирующего компилятора - это одна из крупнейших проблем программирования как науки.
Настоящая статья посвящена проблеме эффективной генерации условий корректности неструктурированных недетерминированных императивных (вычислительных) программ, аннотированных в стиле Р. Флойда [2] предусловиями (на входные данные), постусловиями (на результаты вычислений) и инвариантами циклов. Актуальность исследования обусловлена тем,
*Это исследование частично поддержано грантом РФФИ 06-01-00464-а.
что неструктурированные средства используются многими программистами на практике, а недетерминизм возникает, например, в статическом анализе программ при применении метода абстракции данных.
Можно также заметить, что на проблему эффективности генерации условий корректности вплоть до начала нового тысячелетия не обращали должного внимания. По-видимому, такая ситуация сложилась из-за того, что в структурированном случае условия корректности можно построить при помощи прозрачного синтаксически-управляемого алгоритма, который следует правилам вывода аксиоматической семантики языка программирования в стиле А. Хоара [3] и использует метод обратного просачивания для слабейшего предусловия Э. Дейкстры [4]. В результате число сгенерированных условий корректности получается линейным по числу управляющих конструкций структурированной программы.
Однако сложность генерации условий корректности даже в структурированном случае не исчерпывается числом построенных условий
корректности: к сожалению, каждое "классическое" условие корректности может иметь экспоненциальный размер из-за ветвления в программе и многократных вхождений переменных в формулы. А в неструктурированном случае даже число условий корректности экспоненциально зависит от числа управляющих конструкций в программе (из-за экспоненциального числа возможных путей по программе).
Впервые на проблему экспоненциальной сложности генерации условий корректности для структурированных детерминированных программ обратили внимание С. Фланиган и Дж. Сакс в докладе [5]. В цитируемой работе использован оригинальный метод преобразования аннотированных ациклических структурированных детерминированных программ в эквивалентную так называемую "пассивную" форму без присваиваний. Одновременно с этим преобразованием вычисляется подстановка переменных, аккумулирующая эффект всех присваиваний по разным путям (используются новые вспомогательные переменные для избежания дублирования). Преобразование в пассивную форму и вычисление подстановки осуществимо за линейное время. По программе в пассивной форме можно построить два условия корректности: за линейное время - условие нормального завершения, и за квадратичное время - условие абнормального завершения. Нормальное завершение означает, что программа может быть исполнена (то есть существует трасса от начала до конца программы) без возникновения исключительных ситуаций. Абнормаль-ное завершение означает, что существует трасса от начала до конца программы, во время которой возникают исключительные ситуации. Исходная аннотированная ациклическая структурированная детерминированная программа корректна тогда и только тогда, когда построенная эквивалентная программа в пассивной форме имеет нормальное завершение и не имеет абнормального завершения. Следовательно, верификация исходной программы сводится к проверке условия нормального завершения эквивалентной пассивной программы и опровержению условия ее абнормального завершения. Позже метод из [5] был распространен М. Барнеттом и Р. Лейно в докладе [6] на случай неструктурированных детерминированных программ с аннотированными циклами. Однако, оба доклада [5, 6] не снабжены доказательствами, и за ними
не последовало публикаций с обоснованием корректности (и полноты) предложенных методов.
В данной статье мы предлагаем и полностью обосновываем новый алгоритм генерации условий корректности по Флойду-Хоару в самом общем случае - для неструктурированных недетерминированных программ с аннотированными циклами. Наш алгоритм линейно зависит от числа управляющих конструкций программы и числа операторов, но квадратично зависит от общего размера программы, предусловия, постусловия и инвариантов циклов.
2. ПРЕДВАРИТЕЛЬНЫЕ ПОНЯТИЯ И ОПРЕДЕЛЕНИЯ
В данной работе мы предполагаем, что выбраны и зафиксированы:
• многосортное непустое множество значений, все элементы которого однозначно разбиты на непересекающиеся сорта (которые мы условно будем называть типами), и на значениях каждого типа определено равенство "=",
• множество операций (включая константы), каждая из которых имеет свое уникальное имя и сигнатуру (типы аргументов и тип результатов) и является всюду определенной (то есть всякий раз, когда аргументы имеют соответствующие сигнатуре типы, результат определен и его тип соответствует сигнатуре) ,
• множество отношений, каждое из которых имеет свое уникальное имя и сигнатуру (типы аргументов) и является всюду определенным (то есть всякий раз, когда аргументы имеют соответствующие сигнатуре типы, результат проверки того, что аргументы удовлетворяют отношению, всегда определен).
В частности, в примерах (и приложениях [7, 8]) мы предполагаем, что сорта Z и Zм предназначены для элементов кольца всех целых чисел и элементов кольца вычетов по модулю М (для всех М > 2).
Кроме того, мы предполагаем, что у нас выбраны и зафиксированы:
• множество типизированных переменных (то есть однозначно расписанных по типам, соответствующим выбранной многосортной
системе], причем для каждого типа множество переменных этого типа бесконечно;
• для любой сигнатуры (то есть набора типов аргументов) существует бесконечно много неинтерпретированных символов предикатов этой сигнатуры.
В качестве языка утверждений мы принимаем полуинтерпретированный типизированный язык первого порядка, построенный из типизированных переменных, операций и отношений фиксированной многосортной системы, а также неинтерпретированных символов предикатов (или предикатных символов). В этом языке типизированные переменные и операции с сигнатурой позволяют определить множество термов и их тип обычным образом.
Синтаксис языка состоит из утверждений. Элементарные утверждения - это равенства типизированных термов, отношения (может быть, многоместные) между термами, а также неин-терпретированные символы предикатов, в которые подставлены термы в качестве аргументов (типы которых соответствуют сигнатуре). Утверждения строятся из элементарных при помощи обычных логических связок и кванторов: отрицания "-1", конъюнкции "А", дизъюнкции "V", универсального "V" и экзистенциального "3" кванторов. (Можно также использовать импликацию "—т-" и эквивалентность "-и-", понимаемые как общепринятые сокращения.) Обычным образом определяется понятие свободных и связных вхождений переменных в утверждения: связное вхождение переменной находится в области действия соответствующего квантора, а свободное - нет. Утверждение называется базовым, если оно не использует неинтерпретированных предикатных символов. Утверждение называется бескванторным, если оно не использует кванторов.
Для любого терма г его размер |г| - общее число вхождений переменных и операций в этот терм. Для любого утверждения ф его размер \ф\ - это общее число вхождений логических связок и кванторов, переменных, операций и предикатов в ф. Для любого утверждения ф, переменной х и терма г обозначим через фт/х результат подстановки г в ф вместо всех свободных вхождений X.
Например, пусть х и у - переменные целого типа Z, ъ, а - переменная для массивов целых чисел, индексированных целыми индексами (то есть переменная для "хранения" всю-
ду определенных целочисленных функций целого аргумента / : Z —> Е)] пусть Р - неин-терпретированный предикатный символ, сигнатура которого определяется следующим образом: два первых аргумента имеют тип целых чисел, а тип третьего - массивы целых чисел с целыми индексами. Тогда следующая формула первого порядка ф над целыми числами является утверждением нашего языка: (Р(х,у,а)А А а[х + 3] = у) V Vа. Зх. (а[5] = х + 1). Пример подстановки терма вместо свободных вхождений переменной - утверждение фу_2/х = (Р(У~ -2,у,а)Ла[у-2 + 3] = у) V Vа. Зх. (а[5] = ж + 1).
Семантика утверждений определяется в состояниях после интерпретации предикатных символов.
Интерпретация сопоставляет каждому неин-терпретированному предикатному символу отношение той же сигна
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.