Курсовая работа по «Теории вычислительных процессов»

федеральное агенство связи уральский государственный  институт связи и информаТИКИ гоу впо «сибгути»

 

 

 

 

 

 

 

 

 

Курсовая работа

по дисциплине

«Теория вычислительных процессов»

 

 

 

 

 

 

 

 

 

Г. ЕКАТЕРИНБУРГ, 2013 ГОД

Содержание

     1. Теоретический материал 5

2. Практические задания 6

    Литература 19

 

Современные исследования, связанные с доказательством  правильности программ

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

1. Методы доказательства (частичной) правильности или конечности.

2. Проблемы разработок программ и создания языков программирования.

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

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

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

В наших учебных пособиях (и в курсе теории вычислительных процессов) мы сконцентрировали внимание на двух основных методах: методе индуктивных  утверждений и структурной индукции. Метод индуктивных утверждений  впервые был предложен Флойдом и Науром. Барстелл в 1969 г. предложил метод структурной индукции. В главе 2 очень кратко рассмотрены понятия, относящиеся к правилам верификации и аксиомам для доказательства частичной правильности. Этот метод, впервые предложил Хоар.

Существуют и другие методы доказательства правильности программ. Различные методы доказательства полной правильности итеративных программ приводятся в работах Базу, Бурсталла, Дейкстры, Манны и др. В работе Бурсталла рассмотрен алгебраический подход к доказательству правильности. В работах Бурсталла и Вегбрейта обсуждаются методы доказательства правильности программ, использующих сложные структуры или модифицирующие структуру данных. В работах Манны показано, как можно использовать метод индуктивных утверждений для доказательства правильности недетерминированных программ. В работах Ашкрофта, Келлера, Липтона рассматриваются методы доказательства правильности параллельных программ.

Такой метод доказательства, как метод индуктивных утверждений, где речь идет лишь о доказательстве частичной правильности, требует  отдельного доказательства конечности итеративных программ. Флойд и Манна использовали вполне упорядоченные (или частично упорядоченные) множества для доказательства конечности. В работе Манны проведено сравнение различных методов доказательства конечности. В работе Сайтеса описаны методы доказательства «чистого» окончания программ.

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

В работе Манны «Математическая  теория вычислений» дается некоторый  формальный подход ко многим известным  методам доказательства правильности программ. Рассмотрены методы доказательства правильности и конечности для итеративных  и рекурсивных программ.

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

Желание создавать программы, для которых было бы легко удостовериться в их правильности, привлекло внимание к проблеме конструирования программ и разработки языков программирования. Работа «Конструктивный подход к  проблеме правильности программ» была одной из первых работ, относящихся  к проблемам конструирования  программ и доказательству их правильности. Другая его работа «Программирование  без Goto» также была одной из первых, где вопросы разработки языка связывались с проблемами правильности (речь шла об исключении операторов перехода). Эти же проблемы обсуждались и в других его работах.

Большинство последних работ, где проблемы построения программ связываются  с проблемами их правильности, посвящены  структурному программированию. Основное внимание в них уделяется таким  методам создания программ, которые  позволяли бы программисту следить (неформально убеждаться) за правильностью  программы на всех этапах процесса программирования. Этой теме посвящены  работы Дейкстры и Хоара «структурное программирование», а также работа Макхована и Келли «Стратегии структурного программирования «сверху вниз» и «снизу вверх». Вирт в книге «Системное программирование: введение» написал введение в программирование, где он так же рассматривает структурное программирование и проблемы доказательства правильности. В работе Хоара «Доказательство правильности структурированных программ» приводится детальное доказательство правильности для одной структурированной программы. Миллс («Новые пути компьютерного программирования» и «Как написать правильную программу и доказать это») и Бакер («Структурное программирование в создании программного обеспечения») рекомендуют использовать структурное программирование при создании программного обеспечения. Проблемы структурного программирования и использования оператора перехода рассматриваются и в работе Кнута «Структурное программирование с оператором go to».

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

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

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

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

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

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

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

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

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

 

2. Практические задания

1. Доказать с помощью простой индукции, что для любого положительного n

 

2 + 4 + 6 + … + (2n – 2) + 2n =  n(n + 1)

Используя простую  индукцию, мы должны:

1. Доказать, что 2 = 1(1 + 1). Это  очевидно, т.к. 2 = 1*2.

2. Доказать, что  если для всех положительных  n справедлива формула

2 + 4 + 6 + … + (2n – 2) + 2n =  n(n + 1)

то справедлива и формула

2 + 4 + 6 + … + (2n – 2) + 2n + 2(n + 1) =  (n+1)((n + 1) + 1)

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

2+4+6+…+(2n–2)+2n+2(n+1)= (2+4+6+…+(2n–2)+2n)+2(n+1)=

n(n+1)+2(n+1)=(n+1)(n+2)=(n+1)((n+1)+1)

(по гипотезе

индукции)

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

2 + 4 + 6 + … + (2n – 2) + 2n =  n(n + 1)

Считается справедливой для любого положительного n.

 

 

2. Доказать  правильность блок-схемы программы,  вычисляющей 2ⁿ

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

Сначала необходимо доказать, что при попадании в  точку 2 J = 2^I .

1. При первом  попадании в точку 2 при переходе  из точки 1имеем I = 0 и J = 1. Таким образом, утверждение J = 2^I = 2⁰ = 1справедливо.

2. Предположим, мы попали в точку 2 и утверждение J = 2^I справедливо. Пусть I и J в этой точке принимают значения I_n и J_n, т.е. J_n = 2^In. Если I ¹ N ложно, то это уже обеспечивает конечный результат. Предположим, что мы прошли по циклу, что возможно только при выполнении условия I ¹ N. При возвращении в точку 2 I и J принимают новые значения I_n+1 и J_n+1, которые можно представить следующим образом:

 

 

I_n+1 = I_n + 1,

J _n+1 = 2 * J_n = 2 * 2^In = 2^In+1 =

                                            (так как J_n = 2^In)

Следовательно, при очередном попадании в  точку 2 высказывание

J = 2^I вновь справедливо, что и требовалось доказать, т.е. при любом попадании в точку 2 справедливо высказывание J = 2^I.

Теперь  необходимо доказать, что в конце концов попадем в точку 2 со значением I = N. При первом попадании в точку 2 имеем I = 0. При последующих попаданиях, если таковые есть, I каждый раз увеличивается на 1. Так как значение N нигде в программе не изменяется, и мы предположили, что N ³ 0, то очевидно, что в какой-то момент I станет равным N.

Если мы попадем  в точку 2 при I = N, то будет верно и J = 2^I = 2^N. Отношение I ¹ N в этот момент ложно, и мы попадаем по стрелке с пометкой F (FALSE – ложь) в точку 3 с J = 2^N. На этом доказательство правильности программы заканчивается.