Введение к работе
Настоящая диссертация посвящена новой технике автоматического доказательства — системам переписывания формул (СПФ). Излагается теория СПФ и описывается применение предложенного формализма в автоматическом доказательстве и автоматической верификации программ.
Актуальность темы. В создании надежного программного обеспечения — важнейшей задачи технологии программирования — значительное место занимает классическая верификация программ, основы которой были заложены в работах Флойда и Хоара. При этом решающую роль для автоматизации процесса верификации программ играет разработка методов автоматического доказательства, ориентированных на верификацию. Выделим методы и техники автоматического доказательства, которые используются в настоящее время в системах верификации.
Первую группу методов составляют универсальные методы, которые включают резолюцию, обратный метод Маслова и полные табличные методы. К достоинствам методов первой группы можно отнести их универсальную применимость, но они обладают большой вычислительной сложностью, в большинстве случаев являются полуразрешающими и затрудняют построение контрпримеров к условиям корректности, что полезно для нахождения ошибок в программах. К тому же они практически не используют особенности конкретной проблемной области при проведении доказательства. Как правило, теоремы, появляющиеся при верификации программ, — длинные формулы, что не позволяет применять универсальные методы, по крайней мере, в чистом виде.
Вторую группу методов составляют разрешающие процедуры для конкретных теорий. Они имеют довольно высокую эффективность, часто позволяют легко строить контрпримеры, но класс таких теорий узок и не способен охватить проблемные области, к которым применяется верификация программ на практике.
Среди техник, применяемых в автоматическом доказательстве, можно выделить технику переписывания термов, основанную на системах переписывания термов (СПТ), и технику сужения.
Техника переписывания термов позволяет приспосабливать доказательство к конкретным проблемным областям. Для этого достаточно
лишь модифицировать СПТ, на основе которой проводится доказательство. СПТ достаточно эффективны, так как основаны на простом механизме сопоставления с образцом и не требуют разбора случаев. Ряд условий корректности, появляющихся при верификации программ, не требует для своего доказательства ничего, кроме применения некоторых лемм, аксиом и теорем, представимых в виде равенств. Доказательство таких условий корректности можно автоматизировать с помощью СПТ. Системы переписывания термов — также хороший аппарат доказательства свойств алгебраических типов данных, используемых в языках спецификаций. В то же время при верификации программ встречаются условия корректности, не позволяющие проводить доказательства по типу замены равных равными, лежащему в основе СПТ. К тому же при проведении доказательства часто требуется разбор случаев. И хотя были разработаны различные обобщения СПТ, они не позволяют доказывать условия корректности автоматически уже для таких хорошо формализованных программ, как программы сортировки. В частности, разбор случаев в этих обобщениях не достаточно мощен, нигде не используется такая упрощающая техника как замена переменных.
Техника сужения представляет собой объединение переписывания и унификации. Эта техника проверки выполнимости формул исторически возникла как средство решения проблемы унификации в эква-циональных теориях (^-унификации), была распространена на условные равенства и нашла применение как механизм, позволяющий объединять логические и функциональные языки. Разрешающие процедуры, основанные на сужении, также легко модифицируются при переходе от одной проблемной области к другой, как и процедуры, основанные на переписывании. Сужение позволяет находить конкретные символические решения (унификаторы) и даже множество всех основных символических решений (наиболее общих унификаторов), если система переписывания, лежащая в их основе, полна (нетерова и конфлю-ентна). Унификация, используемая при сужении, позволяет моделировать такое мощное упрощение формул, как замена переменных. В то же время перебор, возникающий при применении техники сужения, создает большое пространство поиска, что приводит к быстрому исчерпыванию скоростных и временных ресурсов машины. Еще одна сложность, связанная с сужением, — более сложный механизм применения этой техники по сравнению с СПТ, требующий вычисления при каждом
применении правила переписывания наиболее общего унификатора. К сожалению, ориентированность техники сужения в основном на разрешение равенств в эквациональных теориях и не сохранение даже выполнимости, не говоря уже об эквивалентности, при преобразованиях формул привело к тому, что эта перспективная техника почти не используется в верификации программ.
Из вышесказанного следует, что создание новой техники автоматического доказательства, которая бы сочетала достоинства вышеизложенных методов и техник и была бы свободна от их недостатков, — актуальная задача в области автоматической верификации программ.
Цель работы — разработка техники автоматического доказательства, ориентированной на автоматическую верификацию, и ее использование в системе верификации программ СПЕКТР.
Научная новизна работы. Предложена техника автоматического доказательства, наследующая достоинства техник переписывания и сужения и лишенная большинства из перечисленных выше недостатков. Эта техника основана на новом формализме — системах переписывания формул, теория которых разработана в диссертации. Преимущество СПФ по сравнению с сужением проявляется в том, что позиция в формуле, к которой применима СПФ, вычисляется проще, чем для сужения. Для этого необходимо выполнить только сопоставление с образцом и алгоритм синтаксической унификации без правила редукции термов. Пространство поиска при применении СПФ также сокращается но сравнению с сужением, так как применяются не произвольные правила из некоторой СПТ, как в технике сужения, а только конкретные выбранные подмножества этой СПТ. СПФ применяются к замкнутым V- и 3-формулам, а не только к бескванторным равенствам. Более того, в качестве теорий, в рамках которых проводится доказательство, уже можно использовать теории с кванторами, а не только эквациональ-ные или квазиэквацпональные (с условными равенствами) теории. Это происходит за счет того, что условия корректности для СПФ кроме равенств и условных равенств включают также УЗ-формулы. Само понятие корректности для СПФ также изменяется. Если для СПТ оно обычно означает сохранение эквивалентности бескванторных формул при переписывании относительно некоторой алгебры, то для СПФ понятие корректности означает сохранение эквивалентности замкнутых V- и 3- формул относительно некоторой алгебраической системы. Для СПФ показана неразрешимость проблемы нетеровости и разрабо-
таны новые методы доказательства эавершимости, учитывающие более сложный по сравнению с СПТ механизм переписывания формул.
Практическая ценность работы. В рамках проекта СПЕКТР разработан и реализован модуль доказательства условий корректности, базирующийся на СПФ. Апробация осуществлялась для трех классов программ — программ редактирования текстов, сортировки массивов и сортировки последовательных файлов. Эксперименты показали, что комбинирования СПФ с разрешающими процедурами для арифметики Пресбургера и ее расширений, равенства, частичного порядка и равенства на мультимножествах оказалось достаточно, чтобы автоматически верифицировать достаточно широкий класс программ из этих проблемных областей. Результаты диссертации могут быть использованы при разработке автоматических систем верификации, в системах автоматического доказательства, в логическом выводе с удовлетворением ограничений.
Апробация работы. Изложенные в диссертации результаты были представлены на третьем сибирском конгрессе по прикладной и индустриальной математике (Новосибирск, июнь 1998), подробно обсуждались на семинаре "Теоретическое и экспериментальное программирование" ИСИ СО РАН. По теме диссертации, опубликовано 6 работ.
Структура и объем диссертации. Диссертация состоит из введения, трех глав, заключения и списка литературы. Объем основной части работы — 119 страниц, список литературы — 146 названий.
