Введение к работе
Актуальность темы. Широкое применение вычислительной техники, возрастающая тенденция разработки универсальных и специализированных языков программирования приводят к необходимости создания надежных трансляторов, т.к. ошибки в них обходятся особенно дорого. Как и в случае обычных программ, тестирование даже на большом количестве примеров не дает гарантии, что в трансляторе отсутствуют ошибки.
Созданию надежных трансляторов посвящено много работ, в которых исследуются формальньв методы определения семантики языков программирования. Предложен критерия корректности трансляторов, который заключается в том, что семантики исходной и сгенерированной транслятором объектной программ должны быть эквивалентны. На пути установления такого сорта эквивалентное-тей возникает ряд проблем: семантическая сложность многих языков и связанная с этим трудность полной формализации семантики, различие между семантическими областями и, как следствие, трудности алгоритмического задания соответствия между ними. Несмотря на большую сложность и громоздкость определений в этих работах, корректность описания семантики, как правило, не обсуждается, достаточно ясные критерии правильности определений языков отсутствуют, хотя и даны некоторш метода доказательства непротиворечивости и полноты определений.
Б большинстве подобных исследований в качестве трансляторов рассматривается не программа, а некоторая модель или функция, слеодфицируодая трансляций. Эта функция показывает, что должен делать транслятор, но не как он это делает. В одних случаях предполагается автоматическая генерация трансляторов по уже проверенным спецификациям. В других просто считается, что достаточно проверки спецификаций, хотя совсем неочевидно соответствие им построенной программы транслятора.
В целом проблема доказательства правильности трансляторов до сих пор является нерешенной для сколько-нибудь реальных языков программирования.
В то же время разработан метод Хоара, суть которого в том, что программа считается правильной, если формально доказано ее
соответствие спецификациям (т.е. программа выполняет в точности те действия, которые задумывались при ее разработке). На его основе создаются автомагические системы верификации. Однако универсальные процедуры логического вывода типа метода резолюций при практическом применении в системах верификации работают недостаточно быстро. Естественный путь повышения эффективности процесса верификации - это разработка средств, позволяющих проводить верификацию программ с учетом особенностей проблемных областей.
В связи с этим актуальной является задача создания методов формальной спецификации трансляторов и автоматических систем для их верификации.
Цель'работы. Разработка методики и средств спецификаций и верификации, позволяющих
описать (специфицировать) основные действия транслятора: синтаксический анализ, проверку семантических соглашений, перевод во внутреннее представление и генерацию кода;
аннотировать программы трансляторов, т.е. задать входные и выходные условия и инварианты циклов;
автоматически доказать правильность выполнения данных действий трансляторов относительно спецификаций.
Научная новизна. Предложен подход к проблеме верификации трансляторов, основанный на применении метода Хоара.
В рамках этого подхода разработаны функциональные средства спецификаций, с помощью которых можно описать этапы работы по переводу программ с одного языка на другой, а также описан метод аннотирования процедур трансляторов, позволяющий выражать требуемые свойства-
Для средств спецификаций разработано аксиоматическое представление, которое позволяет однозначно определять функции и ориентировано на автоматический перевод их в программные конструкции.
На базе данных средств разработана и реализована система верификации трансляторов, позволяющая автоматизировать трудоемкий процесс верификации. В ней наряду с известными правилами вывода аксиоматической системы Хоара применяются новые правила для процедур и файлов. Система является проблемно-ориентиро-
ванной и предназначена для верификации программ трансляторов, хотя возможно ее использование для доказательства формул в других проблемных областях.
Предложенные средства использованы для спецификации трансляторов с подмножеств языка Бейсик и Паскаль. Проведено аннотирование этих трансляторов, и доказана их правильность с помощью системы верификации.
Практическая ценность диссерации. Результаты диссертации могут быть использованы при создании языков спецификация программных систем, при разработке автоматических систем верификации, при доказательстве правильности и поиске ошибок в трансляторах и препроцессорах.
Апробация работы. Изложенные в диссертации результаты были представлены на Всесоюзной конференции "Методы трансляции и конструирования программ" (Новосибирск, октябрь 1984), Всесоххзной конференции "Проблемы совершенствования синтеза, тестирования, верификации и отладки программ" (Рига, ноябрь 1986), Международной конференции по конструированию программ (Будапешт, ишь 1988 г.), Всесоххзной конференции "Методы трансляции и конструирования программ" (Новосибирск, ноябрь 1988), на семинарах ВЦ СО АН СССР и ИСЙ СО АН СССР. Результаты диссертации вошли в НИР, внедренную в п/я А-1332. Эта НИР заняла второе место в конкурсе прикладных работ Сибирского отделения АН СССР за 1989 год.
По теме диссертации опубликовано 9 печатных работ.
Структура и объем диссертации. Диссертация состоит из введения, трех глав, заключения, списка литературы и приложения. Объем основной части работы - по страниц, приложения - 14 страниц, список литературы - 91 название.
