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

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

На правах рукописи СУЛИМОВ Александр Александрович

Ш 5'9.68

ФУНКЦИОНАЛЬНЫЕ СРЕДСТВА СПЕЦИФИКАЦИИ ТРАНСЛЯТОРОВ И ИХ ПРИМЕНЕНИЕ В ПРОБЛЕМНО-ОРИЕНТИРОВАННОИ СИСТЕМЕ ВЕРИФИКАЦИИ ПРОГРАММ

05.13.11 - математическое и программное обеспечение

/

зцч^слптЕ/.ыгггх кахиш» хсэяшшхссоз 3

сис-гйх! :х сатсй

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

Новосибирск - 1991

Работа выполнена в Институте систем информатики СО АН СССР.

Научный руководитель: кандидат физико-математических наук, старший научный сотрудник Непомнящий В.А.

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

Серебряков В.А..

кандидат физико-математических наук Чебдакоз Б.Г.

Ведущая организация - Институт математики и информатики Латвийского университета

Защита состоится " _193' г. в ¡^ — час-

на заседании специализированного совета К 003.93.01 по защите диссертаций на соискании ученой степени кандидата ка.ук при Инстистуте систем информатики СО АН СССР 630090, НоЕосибирск-90, пр. Академика Лаврентьева, б.

С диссертацией можно ознакомиться г. читальном зале отделения ГПНТБ СО АН СССР, пр. Академика Лаврентьева, 6.

Автореферат разослан " " 1991 г.

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

К.ф.-М-Н.

Сабельфельд В.К.

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

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

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

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

В целом проблема доказательства правильности трансляторов до сих пор является нерешенной для сколько-нибудь реальных языков программирования.

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

з

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

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

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

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

- аннотировать программы трансляторов, т.е. задать входные и выходные условия и инварианты циклов;

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

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

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

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

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

4

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

Предложенные средства использованы для спецификации трансляторов с подмножеств языка Бейсик и Паскаль. Проведено аннотирование этих трансляторов, л доказана их правильность с помощью системы верификации.

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

Апробация работы. Изложенные в диссертации результаты были представлены на Всесоюзной конференции "Методы трансляции и конструирования программ" (Новосибирск, октябрь 1984), Всесоюзной конференции "Проблемы совершенствования синтеза, тестирования, верификации и отладки программ" (Рига, ноябрь 1986), Международной конференции по конструированию программ (Будапешт, ишь 1988 г.). Всесоюзной конференции "Методы трансляции и конструирования программ" (Новосибирск, ноябрь 1988), на семинарах ВЦ СО АН СССР и ИСИ СО АН СССР. Результаты диссертации вошли в НИР, внедренную в п/я А-1332. Эта НИР заняла второе место в конкурсе прикладных работ Сибирского отделения АН СССР за 1989 год.

По теме диссертации опубликовано 9 печатных работ.

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

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

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

Первая глава посвящена разработке метода и средств спецификации и верификации трансляторов. В §1 представлена аксиомати-

5

ческая система Хоара для языка Паскаль, с помощью правил вывода которой генерируются условия правильности- Стандартная аксиоматическая система описана в п.1.1, а в п-1.2 приведены модификации правил вывода для оператора вызова процедур и операций над файлами, позволяющие упростить аннотирование программ трансляторов и генерировать по ним более простые условия правильности. Модификация правила вызова процедур заключается в разделении параметров-переменных процедур на два класса: параметры-файлы, над которыми в теле процедуры производится только операция get (read), и остальные изменяемые параметры. Параметру -файлу Г сопоставляется счетчик сдвигов головки буфера файла - lj.. В результате I используется как неизменяемый в процедуре массив неопределенной длины, a if - его индекс. В аннотациях счетчик используется только в сочетании с операцией get - get1 (индекс I опускается, связь с файлом определяется по контексту).

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

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

- сочетаемость достаточной выразительности аксиом и эффективности их применения;

- естественность записи аксиом.

Аксиомы имеют вид ^ & ... & Ад => с, где А1 - это либо отношение (равенство, неравенство и т.п.), либо принадлежност множеству; С - равенство или неравенство. Посылки могут отсут ствовать.

Функции второго класса (л.2.4-), которые будем называть мо?

6

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

В пл. 2.3, 2.5 и 2.6 определяются функции третьего класса, специфицирующие конкретные действия трансляторов. В качестве внутреннего представления рассматривается постфиксная польская запись. Чтобы показать возможности рассматриваемых средств спецификаций и системы верификации, специфицирующие функции определяются в двух вариантах. В одном варианте они связаны с конструкциями входного языка в польской форме и предназначены для спецификации трансляторов с описанием перевода в польскую запись. Во втором варианте перевод не специфицируется, и все грамматические конструкции представлены в обычном виде. В п.2.3 обсуждается анализирующая грамматика,используемая для описания и аннотирования грамматического разбора в трансляторах. В точках тела программы или процедуры транслятора, в которых требуется аннотация;, проанализированная часть входной программы записывается как bEPTtGET1(RIGHT(lQ))) (в дальнейшем Ф(f0) будет обозначать данное выражение), где Г0 - начальное значение файла I (в котором записана входная программа) при входе в процедуру; LEFTCi) - такой файл, что последовательность его элементов совпадает либо с 1 в случае истинности eof(l), либо с прочитанной частью Г в случае ложности eol(f); RlGHKf) - непрочитанная часть £. Спецификация синтаксической корректности данной части программы - это предикат ф(£0) Ш N, а некорректности - отрицание данного предиката NOT(<?»(f0) IN К), где N -либо нетерминал, либо конечная последовательность элементов

7

грамматики. Поэтому анализирующая грамматика должна содержать нетерминалы, соответствующие кавдой рекурсивной процедуре разбора и подходящие для записи предикатов в инвариантах циклов. По этой грамматике автоматически строится функция, которая устанавливает истинность предикатов, специфвщирущих синтаксическую корректность обрабатываемых транслятором программ- Для специфицирования перевода во внутреннее представление кроме анализирушвя грамматики задается вторая грамматика, которую будем называть польской. Элементы польской грамматики располагается в порядке, в котором последовательно сгенерированный по ним код будет выполняться. Каадому правилу анализирующей грамматики сопоставляется правило польской грамматики с тем же набором нетерминалов. По анализирующей и польской грамматикам определяется функция Р01Ш, описывающая перевод в польскую запись. Если генерация кода совмещена с синтаксическим разбором, функция РОК® не связывается с какими-либо программными переменными, а служит вспомогательным средством для определения функций, специфицирующих семантический анализ и генерации кода. В трансляторе, в котором генерация кода отделена от синтаксического анализа, функция РОМЫ сопоставляется с программной переменной (например, файлом), содержащей запись входной программы во внутреннем представлении.

П.2.5 посвящрн спецификации семантического анализа. Рассматриваются спецификации действий по проверке следующих семантических соглашений:

1) все идентификаторы.(константы, переменньв, массивы и пр.) ' должны быть определены;

2) вид идентификатора должен соответствовать его синтаксической позиции (например, использование простой переменной в позиции идентификатора массива с индексом или процедуры некорректно);

3) тип переменной в левой части оператора присваивания должен быть согласован с типом выражения в правой части;

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

специальной функции МУРЕ, определяемой аксиоматически. Аксио-

8

мы предусматривают семантически корректные случаи. В остальных случаях значение FTYTE предполагается равным 'ERROR'. Спецификация семантического анализа заклшается в использовании в аннотациях отношений PTYPE(^(1Q)____)=STYPE и ?TYPE(^(i0),...X>

'ERROR', где STIPE - программная переменная, которая равна 'ERROR', если обнаружено нарушение какого-либо семантического соглашения.

В п.2.б рассматривается спецификация генерации кода трансляторов, в которых синтаксический анализ и генерация кода объединены в одну фазу (операции генерации кода совмешэны с операциями разбора). Функция, специфицирующая генерацию кода, обозначается GC. В зависимости от языка количество аргументов функции GC и их смьсл могут быть различными. Главным аргументом GC является грамматическая конструкция входного языка, остальные аргументы считашся дополнительными. Аргументами GC могут быть множзство описания переменных, уровень вложенности, начальный адрес генерируемых команд и т.п. Значением функции GC является последовательность команд объектного языка.

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

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

9

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

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

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

Инициальные условия - это последовательность равенств вида Х=Х0, где X - параметр-переменная (типа VAR или VC), a Xq -его начальное значение. Такие равенства необходимы для доказательства- соотношений между начальными и заключительными значениями параметров. Применяется три равенства: í=GET1(f0), í=f0 и СХ=СХ0, где I - файл лексем входной программы, а СХ - индексная переменная массива, в который записываются сгенерированные команды. Основой входных условий процедур и инвариантов циклов является формула ((SIYFEO'ERROR') & (*(f0) IN Л)) ->

((FIYPE(POLON(fí>(I0)).....CXo)<>,EER0R') &

GC (РОЬШ(<£(10)).....СХо)=С0БЕ[СХо..СХ-1].

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

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

((STY?E=' ERROR') OR N0T(<Mío) Ш N)) ->

GEN(ERROR,О,0) IN COBE[CX0..CX-1], где GEN(ERROR,О,0) означает код, сигнализирующий об ошибке. ■

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

10

ниях отсутствует функция POION, и для каждой процедуры используется своя функция» специфицирунпзя генерацию кода.

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

Второя глава посвящена применении описанных средств к конкретным трансляторам. Все трансляторы переводят программы в язык стековой машины, которая имеет, однако, многие черты, присущие реальным машинам. Описание этой машины и ее языка (в модифицированном нами варианте) приводится в §1. Трансляторы написаны с помощью метода рекурсивного спуска с использованием итераций. Операции генерации кода совмещены с синтаксическим разбором. Аннотирование проводится со спецификацией перевода в польскую запись. Транслятор с П/м, кроме того, аннотируется без спецификации польского перевода.

В §2 описан транслятор с языка ПЛ/О и его спецификация. Язык ПЛ/О прост, в ему этого транслятор с него не слишком громоздок, в то же время он демонстрирует большинство основных принципов трансляции языков вьсокого уровня. ПЛ/О - небольшое подмножество Паскаля с операторами: присваивания, условным, циклом while, составным и вызовом процедур без параметров. Семантический контроль заключается в проверке первых двух, описанных в п.2.5 главы 1, семантических соглашений. Все аксиомы, определяющие функцию PTYPE, с помощью которой описывается семантический анализ, имеют заключение в виде, неравенства FIYPE(—)о'ERROR'. Функция GC, специфицирующая генерацию кода, имеет в качестве аргументов последовательность элементов польской грамматики с контекстами; множество описаний, уровень вложенности и начальный адрес генерируемых команд.

В §3 описан транслятор и его спецификация с языка MINIBASIC. В язык входят операторы присваивания, безусловного перехода, условного перехода, заголовка цикла и конца цикла, перехода на подпрограмму, возврата. Предварительно транслятор отводит 350 ячеек стека, которые распределяются следующим образом. 10 ячеек отводится для организации стека возвратов из подпрограмм. В языке фиксированное число переменных - 286,

11

каждой отводится постоянная ячейка памяти с 11 по 296. Остальные ячейки (с 297 по 350) используются при обработке операторов циклов для запоминания значений выражений, соответствующих шагу к окончанию циклов. В программе транслятора переменная J содержит число занятых таким образом ячеек. Семантический анализ отдельно не специфицируется, единственное семантическое соглашение, связанное с оператором цикла, проверяется при определении функции GC. Аргументами GC, кроме последовательности элементов грамматики с контекстами, являются аналог счетчика дополнительных переменных в цикле POR (его изменения описывает модифицирующая функция АИЖЮ) и начальный адрес генерируемых команд. Выходные условия процедур и инварианты имеют более простой вид по сравнению с аннотациями языка fUI/o, т.к. исключена семантическая функция PTYPE.

В §4 описан транслятор с языка П/м и его спецификация- Язык П/м является расширением ПЛ/0. Добавлены структуры данных: массивы, записи без вариантов, указатели, параметры процедур. Параметры двух типов: параметры-переменные и параметры-значения, но параметрами-значениями могут быть только простые перемещав и выражения. Стуктуры передаются только как параметры-перемекнье. Нельзя присваивать одной сложной переменной другую, исклшение касается только указателей. Все семантические соглашения, описанные в п.2.5 главы 1, имеют место в языке П/м и специфицируются функцией STYPE. Функция GC, специфицирующая генерацию кода для языка П/м для обоих видов аннотирования, определяется в соответствии с описанием, данным: в п.2.6 главы 1. В частности, она имеет два дополнительных по сравнению с функцией GC для ПЛ/О аргумента, которые являются (при разборе оператора вызова процедуры) аналогами адреса идентификатора процедуры и порядкового номера параметра. Выходаыз условия некоторых процедур и инварианты имеют дополнительные по сравнению с аннотациями языка IWO отношения, связанные с модифицирующими функциями.

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

12

основных частей (каждой посвящзн соответствующий параграф).

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

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

3. Препроцессор преобразует деревообразную форму условий правильности в некоторое линейное представление, приводит арифметические выражения в каноническую форму. Условие правильности после обработки препроцессором имеет вид:

- левая часть (посыпки) находится в конъюнктивной нормальной форме;

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

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

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

5. Дзказатель устанавливает, истинны или нет условия пра-

13

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

На вход доказателю подается условие правильности. Упроститель преобразует условие к совокупности формул вида

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

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

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

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

Если заключение имело вид равенства функции, специфицирующей генерацию кода, и массива комавд - СС(...)=ССШЕ..., оно передается преобразователю. Обрабатывая это заключение, преобразователь либо получает тождество и тогда выводит информацию о его истинности, либо возврашдет информацию о его ложности.

В управляющий модуль-встроены программные реализации общей

14

части определения функции ЯС и базовых функций.

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

Система реализована на языке Рефал и функционирует на ЭВМ 1ВМ РС АТ. Объем исполняемых модулей зависит от языка, т-к- часть их порождается по спецификациям. Для языка МЗМ-вжгс он составляет 170К, для ръ/о - ЮТ, для П/м - 195К. Время доказательства условий правильности зависит от их сложности и занимает от нескольких секунд до 4 минут- Для транслятора с языка ШЖ-ВАБ1С сгенерировано 51 условие правильности. РЪ/о - 47, п/м - 136. Все они были доказаны.

ЗАКЛЮЧЕНИЕ

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

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

2. Предложены эффективные средства верификации, включающие

- модифицированные правила вывода для оператора вызова процедур и операций работы с файлами;

- специальный вид аннотаций, позволяющий выражать требуемые свойства трансляторов;

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

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

4. Средства спецификации и верификации применены к программам трансляторов, и проведен машинный эксперимент по дока-

15

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

Список опубликованных работ по теме диссертации:

1. Сулимов A.A. Функциональные спецификации транслятора// В сб.: Трансляция и преобразование программ. - Новосибирск: ВЦ СО АН СССР. - 1984. - с.137-150.

2. Непомнящий В-А., Сулимов A.A. Базисные средства спецификации и верификации трансляторов// В сб.: Методы трансляции

и конструирования программ. - Новосибирск: ВЦ СО АН СССР. -

1986. - с.78-89.

3. Непомнящий В.А., Воробьев С.Г., Сулимов A.A. Проблемно-ориентированная система верификации программ// Тез. докл. Всесоюз. конф. "Проблемы совершенствования синтеза, тестирования, верификации и отладки программ". - Рига. - 1986. - с.46-48.

4'. Сулимов A.A. Система Еерификации трансляторов// Тез. докл. Всес. конф. "Проблемы совершенствования синтеза, тестирования, верификации и отладки программ". - Рига- - 1986. - с.106-107.

5. Непомнящий В.А., Воробьев С.Г., Сулимов A.A. Проблемно-ориентированная система верификации СПЕКТР// Кибернетика. -

1987. - N 6. - с. 31-37.

6. Сулимов A.A. Модуль верификации трансляторов в системе СПЕКТР// В сб.: Высокопроизводительные вычислительные системы и их программное обеспечение. - Новосибирск: ВЦ СО АН СССР.

- 1987. - с.105-114.

7.' Sullmov A.A. System of Compilers Proving// Foutrh coni. of program deslngners. - Budapest. - 1988. - P.63-68.

8. Сулимов A.A. Об автоматической верификации трансляторов. // Тез. докл. Всесоюз. конф. "Метода трансляции и конструирования программ". - Новосибирск: ВЦ СО АН СССР. - 1988. -

с.104-106.

9. Сулимов A.A. Система верификации генерации кодов трансляторов// В сб.: Теоретические проблемы систем обработки информации. - Новосибирск: ИСИ СО АН СССР. - 1990. - с-151-159.