Доказательство правильности программ (стр. 8 )

После знаменитого письма Дейкстры об операторе перехода (GO ТО) появились работы, где прослеживается влияние проблемы доказательства правильности на разработку языка программирования. Среди языков, в которых проявилось влияние вопросов доказательства правильности, следует отметить такие языки, как Паскаль, А1рharh, Сlu, Nucleus. В работе Хоара «Процедуры и параметры: аксиоматический подход» обсуждаются возможные ограничения на процедуры и параметры, которые могли бы облегчить доказательство правильности. Морисс «Верификационно-ориентированные языки программирования» рассматривает язык, ориентированный на верификацию. Кларк в своей работе обсуждает конструкции языка программирования, для которых невозможно получить хорошую систему аксиом, подобную введенной Хоаром. Он показывает, что в языке могут присутствовать некоторые такие общие свойства, при которых будет невозможно построить логичную и полную систему аксиом, как это было сделано Хоаром. Кларк предлагает такие свойства либо как-то видоизменить, либо вообще исключить из языка для облегчения доказательства правильности.

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

5.3. Механизация процесса доказательства правильности

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

Если мы хотим использовать механическую систему верификации при проведении доказательства правильности, то нужно каким-то образом формализовать и индуктивные утверждения, и сами доказательства. Чаще всего для формализации используется исчисление предикатов первого порядка, хотя такой способ не всегда пригоден для выражения некоторых утверждений и для доказательств. В работах Бурсталла и Манны есть примеры формализованных доказательств правильности на основе нотации исчисления предикатов первого порядка. В работе Лискова и Зиллеса «Программирование с абстрактными типами данных» исследуются различные методы спецификации, которые можно было бы использовать для формальной записи индуктивных утверждений.

Большинство уже построенных систем механической верификации основывается на методе индуктивных утверждений. Такие системы в качестве входных данных рассматривают исходную программу, которую нужно верифицировать, и вместе с ней сформулированные программистом индуктивные утверждения. Основываясь на «заложенных в ней знаниях» синтаксиса и семантики языка программирования, система прослеживает все пути, по которым может идти выполнение программы, и формирует множество условий верификации, которые должны обеспечить верификацию всей программы. В главе 2 мы уже показали, как можно формировать такие формализованные условия верификации: для этого используются программы алгебраических и логических упрощений и «доказыватель» (программа) теорем исчисления предикатов первого порядка. Из-за того что программа, доказывающая механически теоремы, скорее всего будет при некоторых доказательствах обнаруживать ошибки, системы обычно делаются интерактивными и позволяют пользователю вмешиваться в те части доказательств, где обнаруживаются неточности. Системы механической верификации такого типа описываются в работах Гуда, Кинга, Судзуки и др. Системы механической верификации обсуждаются также в работах Куппера, Лондона, Игараши, Левитта, Вандингера.

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

Во всех системах механической верификации, использующих метод индуктивных утверждений, требуется, чтобы индуктивные утверждения задавал пользователь. Было бы очень удобно, если бы система могла сама «задавать» (создавать) некоторые или даже все индуктивные утверждения. В работах Каплейна, Грефа и Вандингера, Германна и Вебгрейта, Манны описываются некоторые эвристические методы, цель которых – механическое формирование индуктивных утверждений. Хотя ни один их этих методов не пригоден для любых программ, но некоторые комбинации таких методов могли бы быть полезными при формировании многих из индуктивных утверждений.

Некоторые идеи и методы систем механической верификации используются в более ограниченных системах, которые создаются для того, чтобы помочь программисту систематически тестировать и отлаживать свою программу. Реализации таких систем описываются в работах Кинга («Корректное доказательство правильности программ», «Подход к программному тестированию»), Элсписа Левитта и Валдингера («Интерактивная система для верификации компьютерных программ».

Литература

1. оказательство правильности программ. – М.: Мир, 1982.

2. Веретельникова правильности программ: Метод индуктивных утверждений. Конспект лекций. – Новосибирск, Изд-во НГТУ, 2004.

3. Информатика. Теория и практика структурного программирования: Методическая разработка. – Новосибирск, изд-во НГТУ, 1999.

4. еория и практика структурного программирования. /Пер. с англ., М.: Мир, 1982.

5. Хопкрофт Дж., Нильман Дж. Введение в теорию автоматов, языков и вычислений, 2-е изд. – М.: Изд. дом «Вильямс», 2002.

6. Метод индуктивных утверждений для доказательства правильности программ: Учебное пособие. – Новосибирск, 2002. – В электронном виде.

7. атематическая логика. – М.: Мир, 1973.

8. зык логики. – М.: Наука, 1969.

ОГЛАВЛЕНИЕ

Глава 1. РАЗЛИЧНЫЕ ВЕРСИИ МАТЕМАТИЧЕСКОЙ ИНДУКЦИИ        3

1.1. Строгая математическая индукции        4

  Принцип строгой индукции        4

1.2. Обобщенная индукция        6

  Принцип обобщенной индукции        8

Глава 2. ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА правильности
С ПОМОЩЬЮ ИДУКТИВНЫХ УТВЕРЖДЕНИЙ        9

Глава 3. АКСИОМАТИЧЕСКИЙ ПОДХОД К ДОКАЗАТЕЛЬСТВУ ЧАСТИЧНОЙ ПРАВИЛЬНОСТИ        14

Глава 4. ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ РЕКУРСИВНЫХ ПРОГРАММ        21

4.1. Упрощенный язык программирования для иллюстрации
понятия рекурсии        21

4.2. Структурная индукция        28

4.3. Структурная индукция для нерекурсивных программ        34

Глава 5. СОВРЕМЕННЫЕ ИССЛЕДОВАНИЯ, СВЯЗАННЫЕ
С ДОКАЗАТЕЛЬСТВОМ ПРАВИЛЬНОСТИ ПРОГРАММ        37

5.1. Методы доказательства        38

5.2. Конструирование программ и языков        39

5.3. Механизация процесса доказательства правильности        40

Литература        42