- 2 -
СОДЕЕШИЕ
стр.
Введение..................................................... 4
■ Глава I. Обзор литературы ................................. 7
Глава П. Логика програш....................................14
§ I. Система Хоара.....................................14
§ 2. Полнота системы Хоара.............................21
§ 3. Модифицированная система Хоара....................25
Выводы........................._........................32
Глава Ш. Контроль типов с использованием верификации
программ..........................................33
§ I. Анализ поведения программы на совокупности
типов данных .................................... 33
§ 2. Система проверки правильности программ относительно структуры объектов 40
§ 3. Пример построения вывода утверждения о
программе....................................... 43
§ 4. Непротиворечивость системы . . ................54
Выводы..................................................54
Глава ІУ.Формализация предметных областей в автоматическом доказательстве.......................................55
§ I. Упрощающие стратегии ............................ 55
§ 2. Пример формального описания: задача об
"испорченной" шахматной доске.....................61
§ 3. Автоматическое доказательство.....................66
Выводы..................................................71
Глава У. Машинный эксперимент........................ . . 72
§ I. Общая характеристика системы проверки утверждений о программах СПРУТ .............................. 72
- 3 -
§ 2. Иллюстрация работы системы.....................74
§ 3. Примеры вернфикавди программ...................80
Выводы............................................... 87
Заключение..................................................88
Литера тура...............................................90
Приложение I. Таблица соответствия синтаксических конструкций языков ирограшщрования
Паскаль, Сетл и Лисп.....................'. 98'
Приложение 2. Распечатки результатов экспериментов по проверке правильности программ на системе СПРУТ.............................................................................................. ТОО
- 4 -
ВВЩЕМСЕ
Исследование математического подхода в описании поведе-нил программ при вычислении - одно из новых, интенсивно развивающихся направлений в программировании, которое имеет приложение в разработке математического обеспечения вычислительных машин и систем. Известно, как много усилий тратится на то, чтобы удостовериться, что программа работает так, как это предполагалось. Если задавать поведение программы с помощью логических условий на входные и выходные значения переменных и доказывать ее свойства математически, то появляется возможность проверять свойства программы для всевозможных значений переменных. К числу свойств, представляющих наибольший интерес, относится понятие правильной програм-м ы , которая для любых значений переменных, удовлетворяющих входному условию, вычисляет значения переменных, удовлетворяющие выходному условию.
В развитии методов проверки правильности программ к середине 70-х годов были получены важные результаты, которые заложили основу для практических систем верификации. Были предложены различные способы формализации семантики языков программирования, разработаны языки спецификации программ и построены системы автоматического доказательства теорем на базе логики предикатов первого порядка.
Настоящая диссертация посвящена исследованию м е т о -да индуктивных высказываний, который состоит в следующем: в программе выбираются контрольные точки так, чтобы любой циклический путь проходил хотя бы через одну такую точку. Каждой контрольной точке сопоставляется логическое условие, называемое и ндуктивным высказыванием , которое остается истинным при
- 5 -
всех возвратах вычисления в эту точку программы. По программе с индуктивными высказываниями, входными и выходными условиями. строится конечное множество логических формул, называемых условиями правильности , тождественная истинность которых равносильна правильности программы.
В главе I дан обзор современного состояния верификации прогрш.-пл методом индуктивных высказываний.
В главе П описывается система Хоара для верификации алгол о-подобных програш. Исследуются логические свойства этой системы.
В главе III рассматривается проверка правильности програш относительно структуры объектов. Описывается формальная система, средствами которой осуществляется контроль типов в алгол о-подобных програшах, не содержащих описаний значеній переменных.
В главе ІУ исследуется способ формального описания предметных областей на основе прикладного исчисления предикатов первого порядка. Описывается организация автоматического доказательства теорем в рамках выбранных средств.
В главе У дается характеристика практической системы верификации програш, реализованной с помощью языка программирования Лисп. Приводится иллюстрация ее работы.
В заключение приведем основные защищаемые положения диссертации:
1. Доказательство свойства полноты системы Хоара, не содержащей рекурсивных процедур, относительно арифметики.
2. Построение аксиоматической системы для проверки правильности программ относительно структуры объектов, не требу-
- 6 -
. ющей сопоставления индуктивных высказываний циклам. Доказательство свойства непротиворечивости данной системы.
3. Разработка способа формализации предметных областей программ на основе исчисления предикатов первого порядка, использующего аксиоматику процедурного характера для повышения эффективности автоматического доказательства теорем.
4. Практическая реализация системы верификации программ методом индуктивных высказываний, которая носит экспериментальный характер и предназначена для апробации методов задания семантики и формализации предметных областей программ.
Штерпальг диссертации опубликованы в работах:
1. Черноброд Л.В. Правильность и эквивалентность программ. -Программирование, 1976, & 6, с. 16-25.
2. Черноброд Л.В. Проверка правильности программ: формализация операщш над множествами.- В сб.: Теория и практика системного программирования, Новосибирск, Б.й., 1977,
с. 86—94.
3. Черноброд Л.В. Решение с помощью ЭВМ задачи об "испорченной" шахматной доске.- В сб.: Языки и системы программирования, Новосибирск, Б.и., 1979, с. 37-46.
4. Черноброд Л.В. Система проверки утверждений о программах СПРУТ.- Новосибирск, Б.и., 1980,- 42 с. (Препринт/ВЦ СО АН СССР; 223).
5. Черноброд Л.В. О контроле типов значений переменных с использованием доказательства свойств программ.- Программирование, 1982, $ 4, с. 14-24.
6. Черноброд Л.В. Верификация программ в системе СПРУТ.- В сб.: Первый чехословацко-советский семинар молодых ученых по математической информатике, Смолешще, Чехословакия, 1980,
с. 47-54.
- 7 -
ГЛАВА I
ОБЗОР ЛИТЕРАТУРЫ
Хоар [I] уточнил метод индуктивных высказываний проверки правильности программ, который неформально был изложен в работе Флойда [ 2 ] , предложив логическую систему для доказательства утвервдеиий о программах вида Р { Л \ О. , где Р5 С} - входное и выходное условия, Я - программа. Утверждение Р { Л } О. интерпретируется следующим образом: если условие Р истинно для входных значений переменных, то по завершению работы программы Я условие О истинно для выходных значений переменных. В системе Хоара нельзя выразить и доказывать остановочность программ. Однако с помощью дополнительных средств, таких как введение счетчиков циклов [ 3 ] или использование вполне упорядоченных множеств [ 4 ] , идея которого была высказана Флойдом [ 2 ] , логика Хоара может применяться для доказательства правильности и остановочности программ.
Первоначальная формулировка системы включала правила вывода для операторов присваивания, условного, композиции, цикла. В работе [ 5 ] в систему были включены процедуры и приняты ограничения на употребление параметров процедур.
Аналогичные системе Хоара способы задания семантики языков программирования были рассмотрены в ряде работ. Манна [ 6 ] предложил алгоритм, который по программе с входным и выходным условиями строит две предикатные формулы. Первая формула означает частичную правильность (правильность при условии остановочности) программы, если существует такая интерпретация вспомогательных предикатных символов, входящих в
- 8 -
формулу, при которой она истинна. Вторая формула означает полную правильность (правильность и остановочность) программы, если при любых интерпретациях вспомогательных предикатных символов, входящих в формулу, она ложна. Вспомогательные предикатные символы в первой формуле выполняют роль индуктивных высказываний. Исследования, проведенные Манной сначала для программ, представленных интерпретированными стандартными схемами, были в дальнейшем продолжены для рекурсивных функциональных схем [7 ] . Относительно алгоритма доказаны свойства полноты и непротиворечивости. Метод, предложенный Дейкстрой [8Д , состоит в следующем: по программе и постусловию строится слабейшее предусловие, характеризующее начальное состояние работы программы, при котором она закончит работу и ее результат будет удовлетворять заданному постусловию. Метод подцелевой индукции, предложенный Моррисом и Вегбрейтом [9] представляет собой частный случай вычислительной индукции и позволяет проверять частичную правильность некоторых программ, пользуясь только входным и выходным условиями цикла. Метод прерывистых утверждений, предложенный Манной и Волдингером [ 10 ] , предназначен для установления полной правильности программ и состоит в следующем: в программу вводятся прерывистые утверждения, которые удовлетворяют условию, что при вычислении программы они в некоторый момент станут истинными.
С помощью прерывистых утверждений относительно программы доказывается, что если перед началом ее вычисления выполнено утверждение Р , то в процессе ее вычисления будет достигнута точка, удовлетворяющая утверждению 0 .
Наибольшее распространение получил метод Хоара, развитие которого осуществлялось как в теоретическом, так и в прикладном аспекте. В систему были добавлены правила вывода для
- 9 -
оператора передачи управления и процедур-функций [11,12*] . Правило вывода дяя оператора присваивания элементу массива [ I ] было заменено более общим правилом [13,14] , допускающим использовать в позиции индексированной переменной произвольное выражение, значением которого служит массив, запись или структура с указателями. Исследовались правила вывода дяя процедур с более широкими возможностями употребления параметров [15] . Была рассмотрена задача верификации программ с абстрактными типами данных, включающая проверку правильности реализации, т.е. представления абстрактного типа в терминах более "конкретных” типов [16] • Логика Хоара использовалась при описании семантики взаимодействующих процессов над общими ресурсами, управление которыми осуществляется с помощью монитора [17] , при описании поведения недетерминированных [18} и последовательно-параллельных программ' [19] .
Исследовались логические свойства системы Хоара. Установлена ее непротиворечивость [15,20-22] . Кук [21] ввел понятие полноты системы Хоара относительно некоторого языка, позволяющего выразить все необходимые индуктивные высказывания, которое доказал сначала для структурированных циклических программ, а затем - для программ с нерекурсивными процедурами, операторами блока и глобальными переменными [22] . Автором диссертации независимо была доказана полнота системы Хоара относительно арифметики дяя программ с нерекурсивными процедурами [23] .
Было установлено, что дяя того, чтобы алгоритмический язык ле имел относительно полную аксиоматизацию, необходимо и достаточно, чтобы в Д(, была разрешима проблема оста-новочности дяя конечных интерпретаций [24] . Относительно ; полные системы Хоара построены дяя простых рекурсивных про-
- 10 -
цедур (не содержащих в качестве параметров процедуры) [25,26], в том числе для процедур с более широкими возможностями употребления параметров [15] , дяя неструктурированных программ с оператором передачи управления [27 ] . Введение в язык
программирования более сложных механизмов, таких как сопрограммы, процедуры-параметры, при существовании в этом языке рекурсии и других обычных средств управления, делает относительно полную аксиоматизацию невозможной [28] .
Большое влияние на развитие верификации программ оказала новая методология программирования, нацеленная на создание надежного математического обеспечения ЭВМ. Получила распространение идея верификации программы при ее построении методом сверху-вниз [29] . Появились языки программирования, предусматривающие развитые средства контроля за выполнением программ, затрудняющие написание неправильных программ, а также ориентированные на математическое исследование свойств программ [13,30-34] . Изучались и сравнивались различные способы точного описания семантики языков программирования [35]. Под влиянием этой методологии была проведена важная работа по математическому обоснованию конструкций языков программирования, начатая с языка Паскаль и получившая дальнейшее развитие в языке Евклид, в котором уже при проектировании были приложены большие усилия для предотвращения различных побочных эффектов. Среди других разработок необходимо отметить создание языка Альфард, оперирующего абстрактны!,ж типами данных, в котором предусмотрена верификация программ перед .тем, как их использовать.
Были реализованы практические системы верификации программ методом индуктивных высказываний. Первая из них [36] ориентировалась на класс арифметических программ с массива!,ж
- Київ+380960830922