ТЕОРИЯ ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ. Теория вычислительных процессов

• Название: Теория вычислительных процессов
• Анкор: ТЕОРИЯ ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ.doc
• Дата: 01.04.2018
• Размер: 2.17 Mb.
• Имя файла: ТЕОРИЯ ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ.doc
• Тип: Документы; #17485
• страница: 11 из 20

Использование высказываний в программах
Высказывания используются для доказательства правильности программ. Тогда высказывания необходимо формулировать в некоторой формальной логической системе. Обычно используется исчисление предикатов первого порядка.

Исчисление - это метод или процесс рассуждений посредством вычислений над символами. В исчислении предикатов высказывания являются логическими переменными или выражениями, имеющими значение T - истина илиF - ложь. Наша цель - при написании программы некоторым способом доказать истинность высказывания (2.2) - триады Хоара {Q} S {R}. Для этого нужно уметь записывать его в исчислении предикатов и формально доказывать его истинность.

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

Пример 2.8. Пусть надо определить приближенное значение квадратного корня: s = sqrt(n), где n, s Nat. Определим постусловие в виде:

R: s×s n < (s+1)×(s+1).

Пример 2.9. Даны целочисленные n > 0 и массив a[1,...,n]. Отсортировать массив, т.е. установить

R: ( i: 1 i < n: a[i] a[i+1]).

Пример 2.10. Определить x как максимальное значение массива a[1,...,n]. Определим постусловие:

R: {x = max({y | y a})}.

Для построения программы следует определить математическое понятие max. Тогда

R: {( i: 1 i n: x = a[i]) AND ( i: 1 i n: a[i] = x)}.

Пример 2.11. Пусть имеем программу S обмена значениями двух целых переменных a и b. Сформулируем входное и выходное высказывания программы и представим программу S в виде предиката:

{a = A AND b = B} S {a = B AND b = A},(2.4)

где A, B - конкретные значения переменных a, b.

Программа вместе с высказываниями между каждой парой соседних операторов называется наброском доказательства. Последовательно, для каждого оператора программы формулируя предикат (2.4), можно доказать, что программа удовлетворяет своим спецификациям. Представим набросок доказательства для программы S:

{a = A AND b = B};

r := a; {r = a AND a = A AND b = B};

a := b; {r = a AND a = B AND b = B};

b := r; {a = B AND b = A}.

Не обязательно набросок доказательства должен быть настолько полным. Для документирования программы нужно вставить достаточно высказываний, чтобы программа стала понимаемой.

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

Правила верификации К. Хоара
Сформулируем правила (аксиомы) К.Хоара, которые определяют предусловия как достаточные предусловия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желаемым постусловиям.

A1. Аксиома присваивания: {R_o} x := Е {R}

Неформальное объяснение аксиомы: так как x после выполнения будет содержать значение Е, то R будет истинно после выполнения, если результат подстановки Е вместо x в R истинен перед выполнением. Таким образом, R_o = R(x) при x = E. Для R_o вводится обозначение: R_o = R^x_Е (у Вирта) или R_x→Е (у Дейкстры), что означает, что x заменяется на Е.

Аксиома присваивания будет иметь вид:{R^x_Е} x := Е {R}.

Сформулируем два очевидных правила монотонности.

A2. Если известно: {Q} S {P} и {P} => {R}, то {Q} S {R}.

A3. Если известно: {Q} S {P} и {R} => {Q}, то {R} S {P}.

Пусть S - это последовательность из двух операторов S1; S2 (составной оператор).

A4. Если известно:{Q} S1 {P1} и {P1} S2 {R}, то {Q} S {R}.

Это правило можно сформулировать для последовательности, состоящей из n операторов.

Сформулируем правило для условного оператора (краткая форма).

A5. Если известно:

{Q AND B} S1 {R} и {Q NOT B} => {R}, то {Q} if B then S1 {R}.

Правило A5 соответствует интерпретации условного оператора в языке программирования.

Сформулируем правило для альтернативного оператора (полная форма условного оператора).

A6. Если известно:

{Q AND B} S1 {R} и {Q NOT B} S2 {R}, то {Q} if B then S1 else S2 {R}.

Сформулируем правила для операторов цикла.

Предусловия и постусловия цикла until удовлетворяют правилу:

A7. Если известно:

{Q AND NOT B} S1 {Q}, то {Q} repeat S1 until B {Q AND NOT B}.

Правило отражает инвариантность цикла. В данном случае единственная операция - это выполнение шага цикла при условии истинности Q вначале.

Предусловия и постусловия цикла while удовлетворяют правилу:

A8. Если известно:

{Q AND B} S1 {Q} , то {Q} while B do S1 {Q AND NOT B}.

Правила A1 - A8 можно использовать для проверки согласованности передачи данных от оператора к оператору, для анализа структурных свойств текстов программ, для установления условий окончания цикла и для анализа результатов выполнения программы.

Пример 2.12. Пусть надо определить частное q и остаток r от деления x на y.

Входные данные x, y и выходные данные q, r Nat, причем y > 0.

Задать(x,y); /* x,y получают конкретные значения X,Y */

r := x; q := 0;

while y r do

begin

r := r - y; q := q + 1

end;

выдать(q,r);

Сформулируем постусловие R: (r < y) AND (x = y*q + r).

Нужно доказать, что {y > 0 AND x/y} S {(r < y) AND (x = y*q + r)}.

Доказательство.

1.Очевидно, что Q => x = x + y*0.

2.Применим аксиому A1 к оператору r := x, тогда получим

{x = x + y*0 } r := x {x = r + y*0}.

3.Аналогично, применяя A1 к оператору q := 0, получим:

{x = r + y*0} q := 0 {x = r + y*q}.

4.Применяя правило A3 к результатам пунктов 1 и 2, получим

{Q} r := x {x = r + y*0}.

5.Применяя правило A4 к результатам пунктов 4 и 3, получим

{Q} r := x; q := 0 {x = r + y*q}.

6.Выполним равносильное преобразование

x = r + y*q AND y r => q = (r - y) + y*(q + 1).

7.Применяя правило A1 к оператору r:= r - y, получим

{x = (r - y) + y*(q + 1)} r:= r - y {x = r+ y*(q+1)}.

8.Для оператора q := q + 1 аналогично получим

{x = r + y*(q + 1)} q := q + 1 {x = r + y*q}.

9.Применяя правило A4 к результатам пунктов 7 и 8, получим

{x = (r - y) + y*(q + 1)} r := r - y; q := q + 1 {x = r + y*q}.

10.Применяя правило A2 к результатам пунктов 6 и 9, получим

{x = r + y*q AND y r} r := r - y; q := q + 1 {x = r + y*q}.

11.Применяя правило A8 к результату пункта 10, получим

{x = r + y*q} while y r do begin r := r - y; q := q + 1 end

{NOT (y <= r) AND (x = r + y*q)}.

Высказывание x = r + y*q является инвариантом цикла, так как значение его остается истинным до цикла и после выполнения каждого шага цикла.

12.Применяя правило A4 к результатам пунктов 5 и 11, получаем то, что требовалось доказать: {Q} S {NOT (y r) AND (x = r + y*q)}.

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

Доказывать будем от противного, т.е. предположим, что программа не заканчивается. Тогда должна существовать бесконечная последовательность значений r и q, удовлетворяющая условиям

1) y r;

2) r, q Nat.

Но значение r на каждом шаге цикла уменьшается на положительную величину: r := r - y (y > 0). Значит, последовательность значений r и q является конечной, т.е. найдется такое значение r, для которого не будет выполняться условие y r и циклический процесс завершится.
Основные выводы и результаты

 Операционная семантика, сводится к описанию смысла программы посредством выполнения ее операторов на реальной или виртуальной машине.

 Операционная семантика является эффективной до тех пор, пока описание языка остается простым и неформальным. Она зависит от алгоритмов, а не от математики.

 В аксиоматической семантике для каждой синтаксической конструкции языка определен набор аксиом, который используют для вывода результатов выполнения этой конструкции. Чтобы понять смысл всей программы эти аксиомы используются так же, как при доказательстве обычных математических теорем.

 Аксиоматическое определение семантики оператора дается в виде правила, описывающего, как для любого заданного постусловия R можно вывести соответствующее слабейшее предусловие wp(S, R).

 Если для каждого оператора языка по заданным постусловиям можно вычислить слабейшее предусловие, то для программ на данном языке может быть построено корректное доказательство.

 Основная теорема инвариантности для цикла:

(P AND wp(DO, T)) => wp(DO, P AND NOT BB).

 Аксиоматическая семантика является мощным инструментом для исследований в области доказательств правильности и анализа программ. Однако ее полезность при описании содержания языков программирования весьма ограничена. Трудно построить «множество основных аксиом, достаточно ограниченное для того, чтобы избежать противоречий, но достаточно богатое для того, чтобы служить отправной точкой для доказательства высказываний о программах» (Э. Дейкстра).

 Денотационная семантика, опирающаяся на теорию рекурсивных функций, основной концепцией имеет определение для каждой сущности языка некоего математического объекта и некоей функции, отображающей экземпляры этой сущности в экземпляры этого математического объекта. Поскольку объекты определены строго, то они представляют собой точный смысл соответствующих сущностей.

 Денотационную семантику программы можно определить в терминах изменений состояний идеального компьютера. Изменения состояний в денотационной семантике определяются строгими математическими функциями, а не запрограммированными алгоритмами, как в операционной семантике.

 Денотационные описания достаточно сложны, но они дают великолепный метод краткого описания языка.

 Декларативная семантика применяется в языках логического программирования, в которых программы состоят из объявлений, а не из операторов. Эти объявления являются высказываниями (операторами в символьной логике).

 Декларативная семантика значительно проще, чем семантика императивных языков. Она не требует для проверки отдельного оператора рассмотрения его контекста, локальных объявлений или последовательности выполнения программы.

 Существуют подкрепленные соответствующими стандартами как универсальные, так и специализированные языки формальных спецификаций, используемые как средство проектирования и анализа программного обеспечения, а также генерации тестов.

 Верификация программ позволяет при помощи строгих средств устанавливать их правильность. При этом используются свойства программы, а не свойства ее отдельных процессов, как при тестировании.

 Процесс доказательства на основе метода индуктивных высказываний Флойда и Наура настолько формализуем, что может выполняться на вычислительной машине.

 Метод верификации Хоара и Дейкстры основан на формальном выводе программ из математической постановки задачи на основе исчисления предикатов первого порядка.

 Правила верификации Хоара определяют достаточные предусловия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желаемым постусловиям.
ТЕОРЕТИЧЕСКИЕ МОДЕЛИ ВЫЧИСЛИТЕЛЬНЫХ ПРОЦЕССОВ
Взаимодействующие последовательные процессы

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

Такой подход обладает целым рядом преимуществ. Во-первых, он позволяет избежать многих традиционных для параллельного программирования проблем, таких, как взаимное влияние и взаимное исключение, прерывания, семафоры, многопоточная обработка и т. д.

Во-вторых, он включает в себя в виде частных случаев модели структурного программирования: мониторы, классы, модули, пакеты, критические участки, конверты, формы и даже подпрограммы.

В-третьих, он является надежной основой для избежания таких ошибок, как расходимость, тупики, зацикливание.
Определения
Неформально, процесс можно представить себе как группу ячеек памяти, содержимое которых меняется по определенным правилам. В ЭВМ эти правила описываются программой, которую интерпретирует процессор. Синоним термина «Процесс», – «задача», «программа».

«Задача – основная единица, подчиняющаяся управляющей программе в мультипрограммном режиме»; «Процесс – это программа, выполняемая псевдопроцессором»; «Процесс – это то, что происходит при выполнении программы на ЭВМ».

Хорнинг и Ренделл (1973) построили формальное определение понятие процесса. Основные термины модели:

набор переменных состояния;

состояние;

пространство состояний;

действия;

работа;

функция действия;

процесс;

начальное состояние.

В модели ВПП понятие процесс используется для обозначения поведения объекта. Для формального описания поведения объекта в ВПП необходимо сначала выделить в таком поведении наиболее важные события или действия, и выбрать для каждого из них подходящее название, или имя.

В случае простого автомата, торгующего шоколадками, существуют два вида событий:

мон -опускание монеты в щель автомата,

шок -появление шоколадки из выдающего устройства.

Заметим, что имя каждого события обозначает целый класс событий; отдельные вхождения события внутри одного класса разделены во времени. Множество имен событий, выбранных для конкретного описания объекта, называется его алфавитом.

Считается, что конкретное событие в жизни объекта происходит мгновенно, т. е. является элементарным действием, не имеющим протяженности во времени. Протяженное, т. е. требующее времени, действие следует рассматривать как пару событий, первое из которых отмечает начало действия, а второе — его завершение. Два протяженных действия перекрываются по времени, если начало каждого из них предшествует завершению другого. Когда совместность событий существенна (например, при синхронизации), такие события сводятся в одно событие, или же совместные события происходят в любом относительно друг друга порядке.

Введем следующие соглашения:

1.Имена событий будем обозначать словами, составленными из строчных букв, например, шок, а также буквами а,b,с...

2. Имена процессов будем обозначать словами, составленными из прописных букв, например, ТАП—простой торговый автомат, а буквамиР,Q,R будем обозначать произвольные процессы.

3.Буквы х,у,z используются для переменных, обозначающих события.

4.Буквы А, В, Сиспользуются для обозначения множества событий.

5.Буквы X, У используются для переменных, обозначающих процессы.

6.Алфавит процесса Р обозначается Р, например, ТАП= {мон,шок}.

7.Процесс с алфавитом V, такой, что в нем не происходит ни одно событие из V, назовем СТОП_Vэтот процесс описывает поведение сломанного объекта. Определим систему обозначений для описания поведения объектов.

Префиксы

Пусть х — событие, а Р — процесс. Тогда (х Р) (читается как «Р за х») описывает объект, который вначале участвует в событии х, а затем ведет себя в точности как Р, где

(х Р) = Р, x Р.

Пример 3.1. Простой торговый автомат, который благополучно обслуживает двух покупателей и затем ломается:

(мон (шок (мон (шок СТОП_ТАП)))).

В дальнейшем скобки будут опускаться в случае линейной последовательности событий. Условимся, что операция → ассоциативна справа.

Рекурсия

Префиксную запись можно использовать для полного описания поведения процесса, который рано или поздно останавливается. Было бы желательно, чтобы этот способ был компактным и не требовал знать заранее срок жизни объекта.

Рассмотрим простой долговечный объект — часы, функционирование которых состоит в том, чтобы тикать.

ЧАСЫ = {тик}.

Теперь рассмотрим объект, который вначале издает единственный «тик», а затем ведет себя в точности как ЧАСЫ

(тикЧАСЫ).

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

ЧАСЫ = (тикЧАСЫ).

Это уравнение можно развертывать простой заменой в правой части уравнения члена ЧАСЫ на равное ему выражение (тикЧАСЫ) столько раз, сколько нужно, при этом возможность для дальнейшего развертывания сохраняется. Мы эффективно описали потенциально бесконечное поведение объекта ЧАСЫ, как

тик тик тик …

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

Утверждение 3.1. Если F(Х) —предваренное выражение, содержащее имя процесса X, а V— алфавит X, то уравнение Х =F(Х) имеет единственное решение в алфавите V.

Иногда обозначают это решение выражением

Х:V.F(Х).

Пример 3.2. Простой торговый автомат, полностью удовлетворяющий спрос на шоколадки:

ТАП= (мон (шок ТАП)).

Решение этого уравнения может быть записано в виде:

ТАП= Х: {мон, шок}.(мон (шок X)).

Утверждение о том, что предваренное уравнение имеет решение, и это решение единственное, можно неформально доказать методом подстановки. Всякий раз, когда в правую часть уравнения производится подстановка на место каждого вхождения имени процесса, выражение, определяющее поведение процесса, становится длиннее, а значит, описывает больший начальный отрезок этого поведения. Таким путем можно определить любой конечный отрезок поведения процесса. А так как два объекта, ведущие себя одинаково вплоть до любого момента времени, ведут себя одинаково всегда, то они представляют собой один и тот же процесс.

Выбор

Используя префиксы и рекурсию, можно описывать объекты, обладающие только одной возможной линией поведения. Однако поведение многих объектов зависит от окружающей их обстановки. Например, торговый автомат может иметь различные щели для 1- и 2-пенсовых монет; выбор одного из двух событий в этом случае предоставлен покупателю.

Если х и y - различные события, то (х P у Q) описывает объект, который сначала участвует в одном из событий x, у, где (х P уQ) = P,x,y Р и Р= Q. Последующее же поведение объекта описывается процессом Р, если первым произошло событие х, или Q, если первым произошло событие y.

Пример 3.3. Процесс копирования состоит из следующих событий:

вв.0—считывание нуля из входного канала,

вв.1— считывание единицы из входного канала,

выв.0—запись нуля в выходной канал,

выв.1 — запись единицы в выходной канал.

Поведение процесса состоит из повторяющихся пар событий. На каждом такте он считывает, а затем записывает один бит.

КОПИБИТ=Х: (вв.0 выв.0 X вв.1 выв.1 X).

Определение выбора легко обобщить на случай более чем двух альтернатив. В общем случае если В - некоторое множество событий, а Р(х) - выражение, определяющее процесс для всех различных х из В, то запись (х: В Р(х)) определяет процесс, который сначала предлагает на выбор любое событие у из В, а затем ведет себя как Р(у).

Взаимная рекурсия

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

Пример 3.4. Автомат с газированной водой имеет рукоятку с двумя возможными положениями — ЛИМОН и АПЕЛЬСИН.Действия по установке рукоятки в соответствующее положение назовем устлимон и устапельсин, а действия автомата по наливанию напитка — лимон иапельсин. Вначале рукоятка занимает некоторое нейтральное положение, к которому затем уже не возвращается. Ниже приводятся уравнения, определяющие алфавит и поведение трех процессов:

АГАЗ= G= W= {устлимон, устапельсин, мон, лимон, апельсин}.

АГАЗ= (устлимон G  устапельсин W),

G= (мон лимон G  устапельсин W),

W= (мон апельсин W  устлимон G).