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

• Автор: Черноброд, Людмила Викторовна
• Шифр специальности: 01.01.10
• Научная степень: Кандидатская
• Год защиты: 1983
• Место защиты: Новосибирск
• Количество страниц: 123 c. : ил

Глава I. Обзор литературы

Глава II. Логика программ

§ I. Система Хоара

§ 2. Полнота системы Хоара

§ 3. Модифицированная система Хоара

Выводы

Глава III. Контроль типов с использованием верификации

программ

§ I. Анализ поведения программы на совокупности

типов данных

§ 2. Система проверки правильности программ относительно структуры объектов

§ 3. Пример построения вывода утверждения о
программе
§ 4. Непротиворечивость системы
Выводы
Глава ІУ.Формализация предметных областей в автоматическом доказательстве
§ I. Упрощающие стратегии
§ 2. Пример формального описания: задача об
"испорченной" шахматной доске
§ 3. Автоматическое доказательство
Выводы
Глава V. Машинный эксперимент
§ I. Общая характеристика системы проверки утверждений о программах СПРУТ

§ 2. Иллюстрация работы системы
§ 3. Примеры верификации программ
Выводы
Заключение
Литература
Приложение I. Таблица соответствия синтаксических конструкций языков программирования
Паскаль, Сетл и Лисп ‘ . 98'
Приложение 2. Распечатки результатов экспериментов по проверке правильности программ на системе СПРУТ

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

этих правил. Случаи правил для пустого оператору, локализации переменных и описания процедуры очевидны. Обозначения:
- предикатная формула; Р , S - логическое выражение.
1) Рассмотрим правило присваивания переменной. Пусть в системе Хоара выводимы его посылки
LR-lAS)Can./*ilACTyP£»l«tl)AaclseC3Cn,/atl‘] } R*,
R,a S Э (ТУРЕ' (зИ2>.
где 1 (.atw6TTa)t(.R S, Л,е) • Тогда из (3.18) шлеем
С^лА &)CXw/=ct3 О с ТУРЕ еСа^/хП-Ч),
следовательно
ФЛА$)D (R/S)Cxa/xtlAai=eÜ«K/5Ci3д (ТУРЕ =-fcL)<
Отсюда и из (3.17) по правилу логического следствия получаем
(.R^aS )С^/х1з л зч-евч/эс.1] ( -1 ] Rt.
Пршленяя к полученному утверждению правило удаления квантора, ввиду l(x^t то ( Jt, Rt)), шлеем
3xn.CCRnAS)Cxw./xl3 а х^Сх^/ос.з ) { Jfr J йг< (3.19)
Используя аксиому присваивания переменной и пршленяя правило композиции, получаем искомое
ßnAS ^x.;=e. ;iH2,
Заметим, что использование в правиле присваивания Т, пе-решленования переменной вместо квантора существования, как в аксиоме присваивания, вызванное необходимостью упростить правило вызова процедуры , приводит к представлению правила в системе Хоара как комбинации нескольких правил вывода.
2) Рассмотрим правило для условного оператора. Пусть в системе Хоара выводимы его посылки