автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Системы переписывания формул и их применение в автоматической верификации программ

РОССИЙСКАЯ АКАДЕМИЯ НАУК СИБИРСКОЕ ОТДЕЛЕНИЕ

ИНСТИТУТ СИСТЕМ ИНФОРМАТИКИ

ИМ. A.n. ЕРШОВА ' ' ' I1 Л

2 ? 0« щ

На правах рукописи

Ануреев Игорь Сергеевич

Системы переписывания формул и их применение

в автоматической верификации программ

05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов, систем и сетей

Автореферат диссертации па соискание ученой степени кандидата физико-математических наук

Новосибирск — 1998

Работа выполнена в Институте систем информатики им. А.П. Ершова Сибирского отделения Российской академии наук.

Научный руководитель: кандидат физ.-мат. наук

Непомнящий В.А.

Официальные оппоненты: доктор физ.-мат. наук

Диковский А.Я., кандидат физ.-мат. наук Семенов А.Л.

Ведущая организация: Иркутский государственный университет

Защита состоится 20 ноября 1998 г. в 14 час. 30 мин. на заседании специализированного совета К0003.93.01 в Институте систем информатики им. А.П. Ершова СО РАН по адресу:

630090, г. Новосибирск, пр. акад. Лаврентьева, 6.

Автореферат разослан 15 октября 1998 г.

Ученый секретарь специализированного совета

КОООЗ.93.01 к.ф.-м.н.

Бульонков М.А.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Настоящая диссертация посвящена новой технике автоматического доказательства — системам переписывания формул (СПФ). Излагается теория СПФ и описывается применение предложенного формализма в автоматическом доказательстве и автоматической верификации программ.

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

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

Вторую группу методов составляют разрешающие процедуры для

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

Среди техник, применяемых в автоматическом доказательстве, можно выделить технику переписывания термов, основанную на системах переписывания термов (СПТ), и технику сужения.

Техника переписывания термов позволяет приспосабливать доказательство к конкретным проблемным областям. Для этого достаточно

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

Техника сужения представляет собой объединение переписывания и унификации. Эта техника проверки выполнимости формул исторически возникла как средство решения проблемы унификации в эква-циональных теориях (¿-унификации), была распространена на условные равенства и нашла применение как механизм, позволяющий объединять логические и функциональные языки. Разрешающие процедуры, основанные на сужении, также легко модифицируются при переходе от одной проблемной области к другой, как и процедуры, основанные на переписывании. Сужение позволяет находить конкретные символические решения (унификаторы) и даже множество всех основных символических решений (наиболее общих унификаторов), если система переписывания, лежащая в их основе, полна (нетерова и конфлю-ентна). Унификация, используемая при сужении, позволяет моделировать такое мощное упрощение формул, как замена переменных. В то же время перебор, возникающий при применении техники сужения, создает большое пространство поиска, что приводит к быстрому исчерпыванию скоростных и временных ресурсов машины. Еще одна сложность, связанная с сужением, — более сложный механизм применения этой техники по сравнению с СПТ, требующий вычисления при каждом

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

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

Цель работы — разработка техники автоматического доказательства, ориентированной на автоматическую верификацию, и ее использование в системе верификации программ СПЕКТР.

Научная новизна работы. Предложена техника автоматического доказательства, наследующая достоинства техник переписывания и сужения и лишенная большинства из перечисленных выше недостатков. Эта техника основана на новом формализме — системах переписывания формул, теория которых разработана в диссертации. Преимущество СПФ по сравнению с сужением проявляется в том, что позиция в формуле, к которой применима СПФ, вычисляется проще, чем для сужения. Для этого необходимо выполнить только сопоставление с образцом и алгоритм синтаксической унификации без правила редукции термов. Пространство поиска при применении СПФ также сокращается но сравнению с сужением, так как применяются не произвольные правила из некоторой СПТ, как в технике сужения, а только конкретные выбранные подмножества этой СПТ. СПФ применяются к замкнутым V- и 3-формулам, а не только к бескванторным равенствам. Более того, в качестве теорий, в рамках которых проводится доказательство, уже можно использовать теории с кванторами, а не только эквациональ-ные или квазиэквациональные (с условными равенствами) теории. Это происходит за счет того, что условия корректности для СПФ кроме равенств и условных равенств включают также \/3-формулы. Само понятие корректности для СПФ также изменяется. Если для СПТ оно обычно означает сохранение эквивалентности бескванторных формул при переписывании относительно некоторой алгебры, то для СПФ понятие корректности означает сохранение эквивалентности замкнутых V- и 3- формул относительно некоторой алгебраической системы. Для СПФ показана неразрешимость проблемы нетеровости и разрабо-

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

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

Апробация работы. Изложенные в диссертации результаты были представлены на третьем сибирском конгрессе по прикладной и индустриальной математике (Новосибирск, июнь 1998), подробно обсуждались на семинаре "Теоретическое и экспериментальное программирование" И СИ СО РАН. По теме диссертации, опубликовано 6 работ.

Структура и объем диссертации. Диссертация состоит из введения, трех глав, заключения и списка литературы. Объем основной части работы — 119 страниц, список литературы — 146 названий.

СОДЕРЖАНИЕ РАБОТЫ

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

Первая глава посвящена изложению теории СПФ.

В §1 приводятся необходимые сведения из теории СПТ, включая абстрактные системы редукций (§1-1), условные СПТ (§1.2), унификацию и сужение (§1.3).

Пусть ТЛ4(8) обозначает множество всех конечных мультимножеств, состоящих из элементов множества Б; 0(т, М) — число вхождений элемента т в мультимножество М. Пусть X = V) — сигнатура с множеством функциональных символов Т, множеством пре-

дикатных символов V и множеством переменных V; Т обозначает множество всех S-термов; UT — множество всех бескванторных Е-формул с равенством Í — Т УШТ — множество всех Е-выражений и S — множество всех подстановок над Е. Пусть и, v G £, Е С Í. Обозначим Var(u), j\4Var(u) соответственно множество и мультимножество (с учетом числа вхождений) переменных, входящих в и; Л^Увгд(и) — мультимножество переменных, входящих в и, за исключением переменных, входящих в подвыражения и, принадлежащие root(u) — корень и; |ií|je — число переменных, функциональных и предикатных символов, входящих в и, за исключением тех, которые входят в подвыражения и, принадлежащие Е; |«| — число \u\<¡¡\ V(u) — множество позиций в щ uq -- подвыражение выражения и, находящееся в позиции q 6 ~Р(н). — выражение, полученное из и подстановкой в позицию g выражения у; Vom(a) = {х 6 V|xa ф х}, VTZange(cr) = \Jxçx>om(o)Var(xcr) — область определения и область значения подстановки а соответственно.

Пусть S — множество, >--(строгий) частичный порядок на S. Порядок >- называется нетеровым, если не существует такой бесконечной последовательности {s, }, gjV из элементов множества S, что для любого i G N выполнено свойство sí >- s;+1. Бинарное отношение , определенное на FM(S), называется расширением порядка >- на мультимножества из FM(S), если для любых мультимножеств М,М' £ F M (S) M ym M' тогда и только тогда, когда существуют такие мультимножества X,Y £ FM(S), что 0 ф X С M, M' - {M\X)UY и для любого у G Y найдется х £ X такой, что х >- у.

Пусть >--(строгий) частичный порядок на Т. Он называется

- монотонным, если для любых термов t,s, s' £ 7~ и позиции g из s >- s' следует <[s]? >- í(s']9;

- стабильным относительно подстановок, если для любых термов t,s ет к для любой подстановки а из t >- s следует ter >- ser;

- порядком упрощения, если >--монотонный порядок такой, что

для любых t, s € Т, если s — собственный подтерм t, то t у s.

Пусть > — обычный порядок "больше" на множестве N натуральных чисел с нулем.

Единственным новым понятием, введенпом в этом параграфе, является понятие тривиального унификатора — наиболее общего унификатора (НОУ) специального вида. НОУ в подстановок сг и а' называется тривиальным унификатором а и <т', если формула

Vy5z(x<r = xtr' => у = ув)

тождественно-истинна, где х — Vom(a) U Т>от(а'), у = Var(xa = жег'), 2 = УЯапде(в)\у. Подстановки сг и а' тривиально унифицируемы, если существует тривиальный унификатор этих подстановок. Рассмотрим алгоритм нахождения тривиального унификатора для множества уравнений {ti = si, ...,tn = sn}- Будем представлять это множество в виде

tt = i'i, ...,tn = sn, называя его эквациональной целью. Пустая цель (пустое множество уравнений) будет обозначаться □.

Алгоритм поиска тривиального унификатора совпадает с алгоритмом унификации, если из последнего удалить правило редукции термов, и состоит из следующих правил преобразования целей:

1) удаление тривиальных уравнений <= t = t, Е ~> Е)

2) перестановка <^t — x,E —> <= х = t, Е, если t V;

3) элиминация переменной х = t,E —> <= Е(х t), если х £ Var(t).

Последнее правило имеет в качестве побочного результата некоторую подстановку er = (я —> t). Будем считать, что и другие правила имеют такой побочный результат — тождественную подстановку. Последовательность вида тг = Go ~Gi —><73 ... —Gk, где Gi — эквациональные цели и G, получается из с помощью некоторого правила из описанных выше, дающего в качестве побочного результата подстановку о-,-, называется унифицирующей деривацией. Деривация я = Go —><7i Gi -><73 ... Gk называется успешной, если Gk — В этом случае подстановка <т = сг 1<72...о> называется ответом деривации тт. Корректность этого алгоритма обеспечивает следующая

Теорема 1. Пусть G = {xar = х<т'\х € Vom(cr) U Vom{<x')}. Ответ любой успешной деривации, начинающийся в G, — тривиальный унификатор подстановок сг я сг', я если подстановки сг и а' тривиально унифицируемы, то дерево унифицирующих дериваций (относительно алгоритма тривиальной унификации) с корнем G конечно и имеет только успешные ветви.

В §2 даны основные понятия теории СПФ и изложены свойства ключевых характеристик СПФ — корректности и нетеровости. В §2.1 определяются основные синтаксические конструкции, связанные с СПФ.

Пусть В е FS{U!F х £ х £), s £ £. Пара /> = (B,s) называется правилом переписывания формул, если для любой тройки р|/ —> г £ В выражения / и s унифицируемы; В называется основой р, р\1 —> г — ветвью р с посылкой р, левой частью / и правой частью г, s — образ-

дом р. Множество правил переписывания формул образует систему переписывания формул.

В дальнейшем Я — некоторая фиксированная СПФ, р — [В, s) £ Я, я- = р\1 —> г — ветвь правила р, 0Ж — НОУ I и s.

Отпошение переписывания для СПФ строится таким образом, чтобы при выполнении определенных условий замкнутые V- и 3-формулы переписываются в эквивалентные формулы. И те и другие представляются как бескванторные формулы со свободными переменными, но с различной семантикой, определяемой способом связывания свободных переменных (только квантором всеобщности или только квантором су-шествования).

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

Пусть А € UT, х = Var(A). Формула А экзистенциально связана, если истинность (семантика) А определяется как истинность формулы Зх(А). Аналогично, формула Л универсально связана, если истинность А определяется как истинность формулы Vx(A). Особенностью СПФ является тот факт, что они переписывают формулу в конечное мультимножество формул, в конечном счете переписывая мультимножества формул в мультимножества формул. Поэтому введенное определение расширяется на конечные мультимножества бескванторных формул со свободными переменными. Пусть U € TM{UT), А £ U, х,\ = Var{A). Мультимножество U экзистенциально связано, если истинность U определяется как истинность формулы Аналогично, U универсально связано, если истинность U определяется как истинность формулы Алее/Vxa(Л).

Пусть А е TM{UT), д 6 V{A), а € S, ser = Aq, <т и вж тривиально унифицируемы, фп — тривиальный унификатор а и 0Ж. Отношение редукции —>r, порождаемое R, сохраняет тип связывания и определяется следующим образом: ->л= {(А, {{р(т*А[г(т\д)фГ!\'п})\ао всем A, q, р], где * имеет вид Л при экзистенциальном связывании и при универсальном связывании. Это отношение распространяется на конечные мультимножества формул: для любых v £ UU¡V £ FM(UT) если v -»я V,toUü М ->д U UV.

С учетом соответствия между абстрактной системой редукций AS = {FM(UT(T)), -*л) и СПФ R все общие понятия (нетеровость,

конфлюентность, нормальная форма и т. д.) и свойства, определяемые в рамках теории абстрактных систем редукций, распространяются и на СПФ. Например, СПФ R нетерова, если абстрактная система редукций AS нетерова и т. д.

Как и для обычных СПТ, для СПФ определяются понятия редекса и согласования с частичным порядком. Пусть U,V,W £ ТМ(UТ). Выражение t называется редексом R, если найдется правило р £ R такое, что t — sa для некоторой подстановки <т и для любой ветви тг этого правила подстановки вк и и тривиально унифицируемы. СПФ R согласована с частичным порядком >-, если —>лС>~.

В §2.2 определяются достаточные условия эквивалентности переписываний с помощью СПФ. Свойство правила переписывания формул переписывать мультимножества формул из некоторого класса только в эквивалентные мультимножества формул из этого же класса называется корректностью правила относительно данного класса.

Пусть хv — множество переменных ветви -тт. Основа В называется корректной, если для любой ветви тг £ В формула / = г)

истинна. Пусть U С ТМ. {UJ-). Правило р называется корректным относительно U, если для любого U € U и для любого V G ТМ. {UТ) из U —V следует, что U эквивалентно V и V £ U. Правило р сохраняет выполнимость, если р корректно относительно множества всех замкнутых 3-формул. Правило р сохраняет истинность, если р корректно относительно множества всех замкнутых V-формул.

Теорема 2. Пусть х = Un(Var(l) U Var(s)), уж = УТ1апде(вж), пж = (Var(p) U Var(r)) \ (Var(¿) U Var(s)). Если основа В корректна и формула Vx V* 3yr3ñ7r(£ = x9w Арвж) истинна, то правило р корректно относительно класса всех замкнутых V- и 3-формул.

В §2.3 доказана неразрешимость проблемы нетеровости и исследуется связь нетеровости СПФ с порядками упрощения. Проблема нетеровости неразрешима уже для специального класса СПФ — униформных систем, для которых подстановки фп — переименования. Ветвь тт называется униформной, если / = s. Правило называется униформным, если униформны все ветви этого правила. СПФ называется униформной, если она состоит только из униформных правил.

Теорема 3. Проблема нетеровости неразрешима для униформных систем.

Следствие 4. Проблема нетеровости неразрешима для СПФ.

Так как униформные системы отличаются от СПТ только разбо-

ром случаев, а для систем с единственной ветвью сводятся к ним с точностью до переименования переменных, ряд свойств СПТ переносится на униформные системы. Кроме свойства неразрешимости проблемы нетеровости рассматривается еще одно такое свойство — связь нете-ровости с порядками упрощения.

Пусть * обозначает логическую связку =>, V или Л. Отображение Dec называется декомпозицией выражений, если Dec(true) = 0, Dec(false) = 0; Dec(t = t') = {t,t'} для любых термов t и t'\ Dec(^A) = Dec(A), Dec(A * B) = Dec(A) U Dec(B). R убывает относительно строгого частичного >-, если для любого правила р G R и для любой ветви -к этого правила Dec(l) ym Dec(r) U Dec(p).

Теорема 5. Униформная СПФ R нетерова, если найдется стабильный относительно подстановок порядок упрощения У такой, что R убывает отосительно

В §3 рассмотрены специальные классы СПФ. Особенностью систем этих классов являются то, что хотя они не все нетеровы, но все завершаются относительно специальной стратегии применения правил — стратегии "любой самый внутренний". Согласно этой стратегии правила применяются только к таким редексам, которые не содержат редексов в качестве собственных подвыражений. Выбор этих классов обусловлен тем, что условия принадлежности к ним можно проверять автоматически и СПФ, входящие в эти классы, элиминируют определенные функциональные символы (анализаторы).

Разобьем множество всех функциональных и предикатных символов на два непересекающихся множества V анализаторов и С конструкторов. Логические связки и логические константы также отнесем к конструкторам. Пусть G С TliV. Обозначим £(G) и T(G) соответственно множество формул и термов, содержащих функциональные и предикатные символы только из множества G.

Выражение и называется линейным, если для любой переменной z выполнено свойство \ö(z,A4Var(u))\ < 1. Подстановка а называется линейной на X С У, если для любых х,у £ X терм хсг — линейный и выполнено условие а: ф у Var(xa-) П Var(ya) = 0. Выражение и называется конструктивным, если и £ £(С). Подстановка сг называется конструктивной, если для любой переменной z выполнено свойство zu £ Т(С). Пусть gi,<?2 £ <72 Ф Яъ 42 — префикс q\. Выражение и называется вложенным, если найдутся ii,<?2 такие, что root(uqi),root(uq2) € Т>. Выражение и называется простым, если

и не является вложенным. Выражение и называется вызовом, если root (и) ет>.

Пусть Ст{и) обозначает мультимножество всех простых вызовов, входящих в и. Отображение /хс называется мерой конструкторов, если ftc(u) = {|i||i G Cm(u)}. Отображение Decv называется декомпозицией переменных, если Decv(u) = Utecm(u)-MVar(t). СПФ R называется конструктивной с множеством конструкторов С и множеством анализаторов V, если для любого правила р G R, для любой ветви тг этого правила s и ! — простые вызовы.

Первый рассматриваемый класс СПФ составляют системы элиминации анализаторов (§3.1). Ветвь тг называется просачивающей, если ж униформна, р,г просты, Decv(l) Э Decv(p) U Decv(r), ¡ic{l) >m fic{r), fic{l) >m Цс{р)- Ветвь 7г называется элиминирующей, если любой НОУ выражений lus конструктивен и линеен на Var(s), р, г конструктивны. Конструктивная СПФ R называется системой элиминации анализаторов (СЭА), если любой простой вызов — редекс R и правила R состоят только из просачивающих и элиминирующих ветвей.

Теорема 6. СЭА завершаются относительно стратегии "любой самый внутренний".

Еще один класс СПФ, завершающихся относительно стратегии "любой самый внутренний", составляют СЭА со статусом, обобщающие СЭА (§3.2). Идея обобщения состоит в том, что при анализе структуры выражений относительно конструкторов и анализаторов учитываются не все аргументы анализаторов, а только специальным образом выбранные. Такой выбор осуществляется с помощью специальной функции, сопоставляющей каждому анализатору множество позиций выбираемых аргументов.

Функция А : V —» !FS(N) называется аргументным статусом, если A(f) С {1,..., Ar(f)} для каждого f £Т>.

Введенные выше понятия вложенности, меры конструкторов, просачивающей ветви и т. п. изменяются при учитывании аргументного статуса «4.

Выражение и называется вложенным, если найдутся q G 'P(u), / G V и г G A(f) такие, что root(uq) = / и терм uqi не конструктивен. Выражение и называется простым, если и не является вложенным.

Обозначим Ст(и) мультимножество всех простых вызовов, входящих в и, I(t) — мультимножество аргументов вызова t, находящихся в позициях A(root(t)). Отображение цс называется мерой конструкто-

ров, если цс(и) = {Ylt'ei(t) ^ Cm(u)}- Отображение Decv называется декомпозицией переменных, если

Decv(u) = Ut6cm(u) Ut'6/(i) XVar(i').

Ветвь 7Г называется просачиваюшсй, если 7Г униформна, р, г просты и Decv(l) Э Decv{p) U Decv(r), цс{1) >т fic{r), рс(1) >т рс(р). Ветвь 7г называется элиминирующей, если любой НОУ в выражений ! и s конструктивен и линеен на Var(s), р,г конструктивны и для любой х £Е Var(s) имеем, что хО g V => х Ç Us'£i(s)Yar(s')- Конструктивная СПФ R называется СЭЛ со статусом А. если любой простой вызов (не обязательно относительно Л!) — редекс R и правила R состоят только из просачивающих и элиминирующих ветвей.

Теорема 7. СЭЛ со статусом завершаются относительно стратегии "любой самый внутренний".

Третий класс конструктивных систем, завершающихся относительно стратегии "любой самый внутренний", — СЭЛ с базой подстановок (§3.3). Идея таких систем заключается в следующем:

1. Выбирается некоторый класс выражений — база подстановок, обладающий определенными свойствами, и при анализе структуры любого выражения подвыражения, попадающие в этот класс, не учитываются. Пример такого анализа структуры выражений — применение функций Var/j и ||д, не учитывающих подвыражения, входящие в Е.

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

Пусть Е С С, S С S. Множество выражений Е называется замкнутым относительно S, если для любого и £ Е, для любой a £ S выполнено свойство иа £ Е. Е называется полным относительно S, если множества Е, £\(ЕUV) замкнуты относительно S. Е замкнуто (полно) относительно подстановок, если Е замкнуто (полно) относительно S.

Отображение называется мерой конструкторов относительно Е, если jif{u) = {lijjsji £ Ст(и)}. Отображение Decf называется декомпозицией переменных относительно Е, если

Decf(u) = {MVarE(t)\t £ Cm(«)}.

Пусть Е — некоторое множество выражений, полное относительно конструктивных подстановок. Ветвь 7г называется просачивающей относительно Е, если 7г униформна, р, г просты и выполнены условия Оес%(1) 2т Лес?(р)иДес* (г), (I) >т ^(г) и р?(I) >т ц?(р). Ветвь 7г называется элиминирующей относительно Е, если для любого НОУ в выражений I и в имеет место {х0\х 6 Уаг(в)} СЕ и выражения р и г конструктивны. Конструктивная СПФ Я называется СЭА с базой подстановок Е, если любой простой вызов — редекс Я и правила К состоят только из просачивающих и элиминирующих относительно Е ветвей.

Теорема 8. СЭА с базой подстановок завершаются относительно стратегии "любой самый внутренний".

Вторая глава посвящена методологии применения СПФ в автоматическом доказательстве.

В §1 описаны разрешающие процедуры для арифметики Пресбур-гера и ее расширений (§1.1), равенства и частичного порядка (§1.2), равенства мультимножеств (§1.3). Выбор именно этих разрешающих процедур обусловлен тем, что их достаточно, чтобы совместно с СПФ доказать условия корректности, появляющиеся при верификации достаточно широкого класса программ сортировки, а также построить разрешающие процедуры для ряда фрагментов теорий множеств, мультимножеств и кортежей. Алгоритм для теории мультимножеств разработан автором, и его полноту обеспечивает следующая

Теорема 9. Алгоритм проверки выполнимости формул теории равенств мультимножеств полон.

В §2 рассматриваются особенности применения СПФ в многосортных теориях. В §2.1 предложено обобщение сортов, определяемых конструкторами, — теории сортов, определяемые обобщенными конструкторами.

Пусть в,— попарно различные сорта. Будем говорить, что сорт 5 определяется конструкторами сх,..., с* над сортами ¿'1,..., если сорта аргументов конструкторов входят в множество сортов {в, 5х, •■•,сорт в является сортом результата конструкторов и выполнена следующая аксиома исчерпывания для конструкторов:

Уя У1<,<* 3$(х = с,•($•)).

Сорта, определяемые конструкторами, допускают следующее обобщение, идея которого заключается в том, чтобы дать более общий вид аксиомы исчерпывания, а именно: Уг Зу,- (р,- А х = где р,- —

некоторые бескванторные формулы, I; — векторы термов. Совокупность этих формул и термов образуют обобщенные конструкторы для обобщенных аксиом исчерпывания. Пусть р — (р±,...,pi), в = {в у,...,(?;), где 0,- — подстановки вида (ж,- —> <,■). Тогда пара (р, 0) задает всю информацию об обобщенном конструкторе. Пара с = (р, в) называется обобщенным конструктором, если Vom(0i) П VR.ange{dj) — 0 и Vom{0i) PiVar[pj) = 0 для любых 1 < i,j < I. Теория т называется теорией сортов, определяемой обобщенными конструкторами сь ..., с*, если аксиомами этой теории являются в точности аксиомы исчерпывания для обобщенных конструкторов с\,..., дк, имеющие следующий вид: Ух7' Vi<i<u 3yjri Л xi = POj, 1 < j < к, где с, = (p3',^'), P — длина вектора pi, xj = U1<i<iiX'om(i?f) и у-' = Ui<;<ii(V71апде(в\) U Var(pf)).

В §2.2 показана связь между многосортными теориями с выделенными подтеориями сортов, определяемыми обобщенными конструкторами, и достаточными условиями корректности для СПФ. При выполнении определенного синтаксического условия корректности СПФ в такой теории сортов достаточные условия корректности СПФ сводятся к условным равенствам, а не представляют VB-формулы, как в теореме корректности. Пусть теория сортов г определяется конструкторами cj,...,cfc, R — СПФ. R называется корректной в г, если для любого правила р = ({pi\h г,-|1 < г < n},s) £ R пара {р, 9) — обобщенный конструктор теории т (с точностью до переименования переменных), где в = (0и...,вп), 0{ — НОУ U и s.

Теорема 10. СПФ R корректна в теории Т с подтеорией сортов г, определяемой обобщенными конструкторами, если R корректна в г и для любого правила р 6 R и для любой ветви р\1 —> г этого правила формула р => I = г истинна в Т.

Особое место среди сортов занимает выделенный булевский сорт bool. Он определяется конструкторами true п false и включает следующие операции: конъюнкцию Л, дизъюнкцию V и отрицание Пусть DNF(£) — фрагмент теории булевского сорта, состоящий из всех формул вида true, false или А\ Л ... Л Л^, где Д- — литералы. Конечные мультимножества, состоящие из формул фрагмента DNF(H), называются ДНФ-формулами. В §2.3 показано, как разрешающая процедура для пропозициональных формул (теорема 11) и процедура приведения к ДНФ-формулам (теорема 12) выражаются с помощью СПФ. В дальнейшем считаем, что любая СПФ переписывает ДНФ-формулы в ДНФ-формулы. Кроме простоты работы с ДНФ-формулами по срав-

нению с произвольными бескванторными формулами, принятие такого соглашения также позволяет элиминировать некоторые ветви из правил переписывания формул, сохраняя при этом выполнимость.

Теорема 13. Пусть А — алгебраическая система, р, р' — правила переписывания формул такие, что образец правила р — отрицательный литерал, р' получается из р удалением всех ветвей из основы, правая часть которых имеет вид false, и множества редексов правил р и р' совпадают. Тогда если р сохраняет выполнимость в А, то р' также сохраняет выполнимость в А.

В §3 СПФ используются для построения разрешающих процедур для фрагментов теорий целых чисел (§3.1), множеств (§3.2), мультимножеств (§3.3) и кортежей (§3.4). Полнота полученных разрешающих процедур обеспечивается теоремами 14—22.

Третья глава посвящена методологии применения СПФ в верификации программ.

В §1 изложены основы классической теории верификации программ (§1.1), дано краткое введение в систему верификации СПЕКТР (§1.2), на базе которой проводился эксперимент по применению СПФ в верификации программ, и описан язык аннотированных программ (§1.3), используемый в примерах.

В §2 излагается техника применения СПФ, позволяющая исключить операции над структурами данных языков программирования из условий корректности, тем самым сводя условия корректности к формулам, включающим операции только над сортами, определяемыми проблемной областью. В качестве примера приводятся упрощающие процедуры, позволяющие элиминировать операции над такими структурами данных языков программирования, как последовательные файлы (§2.1) и массивы (§2.2). Полнота упрощающих процедур обеспечивается теоремами 23 и 24.

В §3 описана реализация модуля переписывания формул, основанного на СПФ и предназначенного для использования в проблемно-ориентированной системе верификации СПЕКТР. Основная цель реализации модуля — создание прототипа, с помощью которого можно было бы убедиться в силе и практичности аппарата СПФ для задачи автоматической верификации программ. В качестве языка реализации выбран язык SML, позволяющий быстро создавать подобные прототипы.

В §3.1 рассматривается логическая структура модуля — основные компоненты и взаимодействия между ними. Основным понятием, ис-

пользуемым в модуле переписывания формул, является понятие тактики. Под тактикой понимается функция, написанная на языке SML и

преобразующая непустые наборы формул в непустые наборы формул в определенном формате. На логическом уровне тактика переписывает дизъюнкцию всех формул, входящих во входной набор формул, в дизъюнкцию всех формул, входящих в выходной набор. Тактика называется корректной, если она переписывает формулы в формулы с сохранением выполнимости, т. е. входная дизъюнкция формул выполнима тогда и только тогда, когда выполнима выходная дизъюнкция формул. Если тактика не применима к входному набору формул, то выдается исключение tac_not_applied. Каждая тактика хранится в отдельном файле с таким же именем и с расширением tac. Входной набор формул представляется списком формул, а выходной набор может представляться в двух форматах — либо списком формул, либо парой списков формул. Второй формат позволяет проводить частичные преобразования входного набора формул. В первый список попадают формулы, на которых данная тактика закончила свою работу, а во второй — не до конца обработанные формулы, которые в дальнейшем могут либо подаваться, либо не подаваться на вход данной тактики в зависимости от стратегий проведения вывода. Таким образом, второй формат предназначен для увеличения эффективности обработки формул. Выходной набор формул реализован с помощью типа outformnlas, определяемого конструкторами outlormula и part_outformula следующим образом: если I — список формул, то outformula(í) — элемент типа outformula; если 1,1' — списки формул, то part_outforinula(/,/') — элемент типа outformnlas. В модуле предусмотрены средства создания и комбинирования тактик. Функция на языке SML, которая в качестве выхода имеет некоторую тактику, называется тактикалом. Кроме тактик, создаваемых с помощью встроенных тактикалов, пользователь имеет возможность писать на языке свои собственные тактики, называемые базовыми. Проверка корректности базовых тактик ложится на пользователя.

В §3.2 описаны встроенные тактикалы. Тактикал FRS получает на вход СПФ и выдает тактику, применяющую данную систему в соответствии со стратегией "левый самый внутренний". Полученная тактика корректна, если соответствующая СПФ сохраняет выполнимость. Доказательство сохранения выполнимости системой сводится к проверке достаточных условий теоремы корректности и в настоящее время производится вручную. Выбор такой стратегии применения СПФ обусло-

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

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

В §4 даются примеры применения СПФ для доказательства условий корректности программ из описанных выше областей. В §4.1 приведены примеры простых программ редактирования файлов (копирования файла и линейного поиска). В §4.2 рассматриваются программы сортировки массивов (сортировка простой вставкой и быстрая сортировка), а §4.3 посвящен программе сортировки файлов естественным слиянием.

В заключении приводятся основные результаты работы:

1. Разработана новая техника автоматического доказательства, являющаяся обобщением как техники сужения, так и техники переписывания термов, — техника переписывания формул, базирующаяся на системах переписывания формул. Эта техника включает:

- новое понятие корректности — сохранение эквивалентности замкнутых V- и 3-формул при переписываниях;

- метод доказательства корректности (теорема корректности);

- методы проверки завершимости систем переписывания формул (униформные системы, системы элиминации анализаторов и их обобщение на аргументный статус, системы элиминации анализаторов с базой подстановок).

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

- техники применения СПФ такие, как использование СПФ для теорий сортов, определяемых обобщенными конструкторами, элиминация структур данных языков программирования, проиллюстрированная на примере массивов и последовательных файлов, применение СПФ к булевскому сорту (удаление ряда ветвей правила переписывания формул, образец которого начинается с отрицания, с сохранением его корректности, построение разрешающей процедуры для пропозициональных формул и процедуры приведения к дизъюнктивной нормальной форме с помощью СПФ);

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

- разрешающие процедуры для условий корректности, возникающих при верификации программ редактирования текстов, сортировки массивов и сортировки файлов.

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

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Ануреев И. С. Интегрированные правила переписывания термов и их применение в автоматической верификации программ // Проблемы спецификации и верификации параллельных систем. — Новосибирск, 1995. —■ С. 185—213.

2. Ануреев И. С. Системы переписывания формул. —Новосибирск, 1997. — 22 с. — (Препр./РАН. Сиб. отд-ние. ИСИ; N 40).

3. Ануреев И. С. Системы переписывания формул и их применение в автоматической верификации программ. — ИНПРИМ. Тезисы докладов, часть V. — Новосибирск: Изд-во Института математики СО РАН, 1998. — С. 37.

4. Ануреев И.С. Упрощающие процедуры для типов данных, основанные на системах переписывания формул. — Новосибирск, 1998. — 43 с. — (Препр./РАН. Сиб. отд-ние. ИСИ; N 53).

5. Ануреев И.С. Теория систем переписывания формул. — Новосибирск, 1998. — 35 с. — (Препр./РАН. Сиб. отд-ние. ИСИ; N 54).

6. Ануреев И.С. Применение систем переписывания формул в автоматической верификации программ. — Новосибирск, 1998. — 47 с. —

61: дз-1/

РОССИЙСКАЯ АКАДЕМИЯ НАУК СИБИРСКОЕ ОТДЕЛЕНИЕ

ИНСТИТУТ СИСТЕМ ИНФОРМАТИКИ ИМ. Д.П. ЕРШОВА

На правах рукописи

Ануреев Игорь Сергеевич

СИСТЕМЫ ПЕРЕПИСЫВАНИЯ ФОРМУЛ И ИХ ПРИМЕНЕНИЕ В АВТОМАТИЧЕСКОЙ ВЕРИФИКАЦИИ ПРОГРАММ

05.13.11 — математик ^кое и программное обеспечение вычислительных машин, комплексов, сетей и систем

Диссертация на соискание ученой степени кандидата физико-математических наук

Научный руководитель кандидат физико-математических наук, зав.лаб. теоретического программирования ИСИ СО РАН Непомнящий В.А.

Новосибирск — 1998

Содержание

Введение 4

1 Теория систем переписывания формул 13

§1 Основы теории систем переписывания термов .... 14

§1.1 Абстрактные системы редукций................14

§1.2 Системы переписывания термов................17

§1.3 Техника сужения..................................22

§2 Системы переписывания формул........................28

§2.1 Основные определения............................29

§2.2 Корректность систем переписывания формул 32

§2.3 Проблема нетеровости............................35

§3 Завершимость систем переписывания формул .... 37

§3.1 Системы элиминации анализаторов ............38

§3.2 Системы элиминации анализаторов со статусом 42 §3.3 Системы элиминации анализаторов с базой подстановок ............................................44

2 Применение систем переписывания формул в автоматическом доказательстве 48

§1 Разрешимые теории........................................49

§1.1 Арифметика Пресбургера и ее расширения . . 49

§1.2 Теории равенства и частичного порядка . . . 52

§1.3 Теория равенства мультимножеств..............53

§2 Особенности применения систем переписывания формул в многосортных теориях............................57

§2.1 Сорта, определяемые обобщенными конструкторами :........................................58

§2.2 Корректность систем переписывания формул 60

§2.3 Булевский сорт....................................61

§3 Разрешающие процедуры, основанные на системах

переписывания формул ..................................66

§3.1 Фрагменты теории целых чисел ................67

§3.2 Фрагменты теории множеств....................70

§3.3 Фрагменты теории мультимножеств............72

§3.4 Фрагменты теории кортежей....................76

3 Применение систем переписывания формул в автоматической верификации программ 84

§1 Предварительные съедения о верификации ............85

§1.1 Метод Хоара........................................85

§1.2 Система верификации СПЕКТР ................87

§1.3 Модельный язык аннотированных программ 89

§2 Элиминация операций над структурами данных ... 90

§2.1 Последовательные файлы ........................91

§2.2 Массивы............................................94

§3 Модуль переписывания формул в системе СПЕКТР . 97

§3.1 Общая структура модуля ........................98

§3.2 Тактикалы.....................101

§3.3 Результаты эксперимента............104

§4 Примеры автоматической верификации программ . 105

§4.1 Программы редактирования текстов......106

§4.2 Сортировка массивов...............111

§4.3 Сортировка файлов естественным слиянием . 114

Заключение 119

Литература 121

Введение

В создании надежного программного обеспечения — важнейшей задачи технологии программирования — значительное место занимает классическая верификация программ [1, 21, 22, 31, 37, 73. 105, 132], основы которой были заложены в работах Флойда и Хо-ара. При этом решающую роль для автоматизации процесса верификации программ играет разработка методов автоматического доказательства, ориентированных на верификацию. Выделим методы и техники автоматического доказательства, которые используются в настоящее время в системах верификации. При рассмотрении методов и техник автоматического доказательства будем сравнивать их по следующим характеристикам:

- Ориентированность на верификацию, заключающаяся в том. учитывают ли разрешающие процедуры, основанные на том или ином методе или технике, специфику задачи верификации;

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

- Классы формул, к которым применим метод или техника, п классы теорий, в рамках которых проводится доказательство.

Первую группу методов составляют универсальные методы [18. 20, 104], которые включают резолюцию [27, 36], обратный метод Маслова [26] и полные табличные методы [44, 103, 122]. Другие универсальные методы, основанные на том или ином исчислении и чисто дедуктивном выводе, не входят в эту группу, так как они не ориентированы на автоматическое доказательство. К досто-

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

Вторую группу методов составляют разрешающие процедуры для конкретных теорий, например для арифметики Пресбургера и ее расширений [35, 133, 134], теории списков [116, 121], арифметики сложения рациональных чисел [135], комбинации теорий с помощью равенств и дизъюнкций равенств [114, 115]. Достаточно полный обзор таких теорий можно найти в [34]. Они имеют довольно высокую эффективность, часто позволяют легко строить контрпримеры (например метод Шостака для арифметики Пресбургера). но класс таких теорий узок и не позволяет охватить проблемные области, к которым применяется верификация программ на практике.

Среди техник, применяемых в автоматическом доказательстве, можно выделить технику переписывания термов [11, 25, 28, 53, 84]. основанную на системах переписывания термов (СПТ), и технику сужения [69].

Техника переписывания термов [42, 78 — 81, 102] позволяет приспосабливать доказательство к конкретным проблемным областям. Для этого достаточно лишь модифицировать СПТ, лежащую в основе разрешающей проц^д^'ры. СПТ довольно эффективны, так как основаны на простом механизме сопоставления с образном

и не требуют разбора случаев. Ряд условий корректности, появляющихся при верификации программ, не требует для своего доказательства ничего, кроме применения некоторых лемм, аксиом и теорем, представимых в виде равенств. Доказательство таких условий корректности часто можно автоматизировать с помощью СПТ. Системы переписывания термов являются также хорошим аппаратом доказательства свойств алгебраических типов данных [2, 23], используемых в языках спецификаций. В то же время при верификации программ встречаются условия корректности, не позволяющие проводить доказательства по типу замены равных равными, лежащему в основе СПТ. К тому же при проведении доказательства часто требуется разбор случаев. И хотя были разработаны различные обобщения СПТ:

- условные СПТ [60, 64, 94, 112, 128, 146], допускающие применение правила переписывания при выполнении определенного условия,

- эквациональные СПТ [40, 46, 58, 82, 90 — 92,126, 145]. комбинирующие применение правил переписывания с выводом в экваци-ональных теориях,

- СПТ со встроенными разрешающими процедурами [13 — 16].

- СПТ для теорий, которые не являются квазиэквациональными, в частности, для логики первого порядка [96, 125],

- СПТ с разбором случаев [17],

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

Техника сужения представляет собой объединение переписывания и унификации. Эта техника проверки выполнимости формул исторически возникла как средство решения проблемы унифика-

ции в эквациональных теориях (Е'-унификации), была распространена на условные равенства [61, 62, 87, 95] и нашла применение как механизм, позволяющий объединять логические и функциональные языки [70, 74 —76, 110]. Разрешающие процедуры, основанные на сужении, также легко модифицируются при переходе от одной проблемной области к другой, как и процедуры, основанные на переписывании. Эта техника позволяет находить конкретные символические решения (унификаторы) и даже множество всех основных символических решений (наиболее общих унификаторов), если система переписывания, лежащая в ее основе, является полной (нете-ровой и конфлюентной). Унификация, используемая при сужении, позволяет моделировать такое мощное упрощение формул как замена переменных. В то же время перебор, возникающий при применении техники сужения, создает большое пространство поиска, что приводит к быстрому исчерпыванию скоростных и временных ресурсов машины. Еще одной сложностью, связанной с сужением, является более сложный механизм применения этой техники по сравнению с СПТ, требующий вычисления при каждом применении правила переписывания наиболее общего унификатора. Для решения этой проблемы разработано множество стратегий [65, 66] (нормальное сужение [67], базисное сужение [86], комбинация базисного и нормального сужения [120, 129], стратегия "самый внутренний" [70], ленивое сужение [144]), позволяющих уменьшить перебор, но эти стратегии не привязаны к конкретным проблемным областям и уменьшают перебор лишь незначительно. Другое направление, в котором ведутся исследования, является установление полноты сужения при более слабых ограничениях, накладываемых на СПТ. В этом направлении получены некоторые результаты для конфлю-ентных [86] и полуполных (semi-complete) [143] СПТ. К сожалению, ориентированность техники сужения в основном на разрешение

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

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

В настоящей работе предложена техника автоматического доказательства, наследующая достоинства техник переписывания и сужения и лишенная многих из перечисленных выше недостатков. Эта техника основана на новом формализме — системах переписывания формул (СПФ), теория которых разработана в диссертации. СПФ состоит из конечного множества правил переписывания формул, каждое из которых задается некоторой условной системой переписывания термов — основой правила и некоторым выражением — образцом правила. Если ограничиться только применением СПФ к равенствам, то применение правила переписывания формул к некоторому равенству можно представить как одновременное сужение этого равенства в одной и той же позиции при помощи каждого правила из основы. В результате получим ровно столько "суженных" равенств, сколько правил входит в основу, моделируя таким образом ор случаев.

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

щается по сравнению с сужением, так как применяются не произвольные правила из некоторой СПТ как в технике сужения, а только конкретные выбранные подмножества СПТ — основы правил, входящих в СПФ. Но самое главное преимущество СПФ по сравнению с техникой сужения заключается в том, что они применяются к V- и 3-формулам, а не только к бескванторным равенствам. Более того, в качестве теорий, в рамках которых проводится доказательство, уже можно использовать теории с кванторами, а не только эквациональные или квазиэквациональные (с условными равенствами) теории. Это происходит за счет того, что условия корректности для правил переписывания формул кроме равенств и условных равенств включают также \/3-формулы. Само понятие корректности для правил переписывания формул также изменяется. Если для правил переписывания термов оно обычно означает сохранение эквивалентности бескванторных формул при переписывании относительно некоторой алгебры, то для правил переписывания формул понятие корректности означает сохранение эквивалентности замкнутых V- и 3- формул относительно некоторой алгебраической системы.

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

СПФ с разрешающими процедурами для нормальных форм (формул, которые уже не могут быть переписаны).

Сохранение выполнимости и довольно мощный механизм переписывания формул делают СПФ перспективным средством в логическом выводе с удовлетворением ограничений (constraint deduction) [52, 97].

Использование СПФ в качестве упрощающих процедур ставит проблему выделения классов СПФ, которые являлись бы нетеро-выми или хотя бы завершались Относительно некоторой заданной стратегии применения правил. В работе выделен ряд таких классов.

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

В рамках проекта СПЕКТР [30, 32, 118, 119] разработан и реализован модуль доказательства^ условий корректности, базирующийся на СПФ. Апробация осуществлялась для трех классов программ — программ редактирования текстов, сортировки массивов и сортировки последовательных файлов. Эксперименты показали, что комбинирования СПФ с разрешающими процедурами для арифметики Пресбургера и ее расширений, равенства, частичного порядка и равенства на мультимножествах оказалось достаточно, чтобы автоматически верифицировать достаточно широкий класс программ из этих проблемных областей. Это подтверждает практическую ценность результов работы.

Опишем структуру диссертации.

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

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

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

Третья глава посвящен