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

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

DO: do B₁ → S₁ П B₂ → S₂ ... П B_n → S_nod,

где n  0, B_i → S_i- охраняемые команды.

Выполняется оператор следующим образом. Пока возможно выбирается охрана B_i со значением истина, и выполняется соответствующий оператор S_i. Как только все охраны будут иметь значение ложь, выполнение DO завершится.

Выбор охраны со значением истина и выполнение соответствующего оператора называется выполнением шага цикла. Если истинными являются несколько охран, то выбирается любая из них.

Следовательно, оператор DO эквивалентен оператору

do BB→ if B₂ → S₁ П B₂ → S₂ ... П B_n → S_nfi od или do BB → IF od,

где BB - дизъюнкция охран, IF - оператор выбора.

Пример 2.5. Алгоритм Евклида.

Вариант 1.

задать (N, M);

if N > 0 AND M > 0 → n, m := N, M;

do n ≠ m → if n > m → n := n – m П m > n → m := m – n fi od;

выдать (n)

fi.

Вариант 2.

задать (N, M);

if N > 0 AND M > 0 → n, m := N, M;

do n > m → n := n – m П m > n → m := m – n od;

выдать (n)

fi.

Дадим формальное определение слабейшего предусловия для оператора цикла DO.

Пусть предикат H₀(R) определяет множество состояний, в которых выполнение DO завершается за 0 шагов (в этом случае все охраны с самого начала ложны, после завершения R имеет значение истина):

H₀(R) = NOT BB AND R.

Другими словами, требуется, чтобы оператор цикла DO завершил работу, не производя выборки охраняемой команды, что гарантируется первым конъюнктивным членом предиката H₀(R): NOT BB = T. При этом истинность R до выполнения DO является необходимым условием для истинности R после выполнения DO.

Определим предикат H_k(R) как множество состояний, в которых выполнение DO заканчивается за k шагов при значении R истина (H_k(R) будет определяться через H_k-1(R)):

H_k(R) = H₀(R) OR wp(IF, H_k-1(R)), k > 0 → wp(DO, R) = ( k: k  0: H_k(R)).

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

Определение DO. Если предикаты H_k(R) задаются в виде

H_k(R) = NOT B AND R, k= 0,

H_k(R) = wp(IF, H_k-1(R)), k > 0, → wp(DO, R)=( k: k  0: H_k(R)).

Основная теорема для оператора цикла. Пусть оператор выбора IF и предикат P таковы, что для всех состояний справедливо

(P AND BB) => wp(IF, R).(2.3)

Тогда для оператора цикла справедливо:

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

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

Поясним смысл теоремы. Условие (2.3) означает, что если предикат P первоначально истинен и одна из охраняемых команд выбирается для выполнения, то после ее выполнения P сохранит значение истинности. После завершения оператора, когда ни одна из охран не является истиной, будем иметь:

P AND NOT BB.

Работа завершится правильно, если условие wp(DO, T) справедливо и до выполнения DO. Так как любое состояние удовлетворяет T, то wp(DO, T) является слабейшим предусловием для начального состояния такого, что запуск оператора цикла DO приведет к правильно завершаемой работе.

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

Из определения DO следует:

H₀(T) = NOT BB AND T, k = 0;

H_k(T) = wp(IF, H_k-1(T)), k > 0, → wp(DO, T) = ( k: k  0: H_k(T));

H₀(P AND NOT BB) = P AND NOT BB;

H_k(P AND NOT BB) = wp(IF, H_k-1(P AND NOT BB), → wp(DO, P AND NOT BB) = = ( k  0: H_k(P AND NOT BB)).

С помощью метода математической индукции можно доказать, что из условия (2.3) следует

(P AND H_k(T)) => H_k(P AND NOT BB), k  0.

Тогда имеем

P AND wp(DO, T) = ( k: k  0: P AND H_k(T)) => ( k: k  0: H_k(P AND NOT BB)) = = wp(DO, P AND NOT BB).

Следовательно, (P AND wp(DO, T)) => wp(DO, P AND NOT BB).

Чтобы использовать аксиоматическую семантику с данным языком программирования для доказательства правильности программ или для описания формальной семантики, для каждого вида операторов языка должны быть определены аксиомы или правила логического вывода. С ними мы познакомимся в п. 2.3 «Верификация программ».

В аксиоматической семантике система (2.1) интерпретируется как набор аксиом в рамках некоторой формальной логической системы, в которой есть правила вывода и/или интерпретации определяемых объектов.

Для интерпретации системы функций (2.1) вводится понятие аксиоматического описания <S, A> - логически связанной пары понятий: S - сигнатура используемых в системе символов функций f₁, f₂, ..., f_m и символов констант (нульместных функциональных символов) c₁, c₂, ..., c_l, а A - набор аксиом, представленный системой. Предполагается, что каждая переменная x_i, i = 1, ..., k, и каждая константа c_i, i = 1, ..., l, используемая в A, принадлежит к какому-либо из типов данных t₁, t₂, ..., t_r, а каждый символ f_j, j = 1, ..., m, представляет функцию, типа: t_i1 t_i2t... _ik t_i0. Такое аксиоматическое описание получит конкретную интерпретацию, если будут заданы конкретные типы данных t_i = t_i', i = 1, ..., r, и конкретные значения констант c_i = c_i', i = 1, ..., l.

К. Хоaр построил аксиоматическое определение набора типов данных, которые потом Н. Вирт использовал при создании языка Паскаль.

Пример 2.6. Рассмотрим систему равенств:

УДАЛИТЬ(ДОБАВИТЬ(m,d)) = m,

ВЕРХ(ДОБАВИТЬ(m,d)) = d,

УДАЛИТЬ(ПУСТ) = ПУСТ,

ВЕРХ(ПУСТ) = ДНО,

где УДАЛИТЬ, ДОБАВИТЬ, ВЕРХ - символы функций, а ПУСТ и ДНО - символы констант, образующие сигнатуру этой системы. Пусть D, D1 и М - некоторые типы данных, такие, что m M, d D, ПУСТ M, ДНО D1, а функциональные символы представляют функции следующих типов:

УДАЛИТЬ: M M,

ДОБАВИТЬ:M, D M,

ВЕРХ:M D1.

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

Зададим интерпретацию символов ее сигнатуры: D - множество значений, которые являются элементами магазина, M - множество состояний магазина, M = {d₁,d₂, ... ,d_n: d_i D, i= 1, ..., n, n 0}, D1=D {ДНО}, ПУСТ={}, а ДНО - особое значение (зависящее от реализации магазина), не принадлежащее D. Тогда указанный набор аксиом определяют свойства магазина.

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

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

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

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

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

<двоичное_число> → 0; | 1; | <двоичное_число>0; | <двоичное_число>1.

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

В нашем примере значащие объекты должны связываться с первыми двумя правилами. Остальные два правила являются, в известном смысле, правилами вычислений, поскольку они объединяют терминальный символ, с которым может ассоциироваться объект, с нетерминальным, который может представлять собой некоторую конструкцию.

Пусть область определения семантических значений объектов представляет собой множество неотрицательных десятичных целых чисел Nat. Это именно те объекты, которые мы хотим связать с двоичными числами. Семантическая функция М_b отображает синтаксические объекты в объекты множества N согласно указанным выше правилам. Сама функция М_bопределяется следующим образом:

М_b('0') = 0, М_b('1')=1;

М_b(<двоичное_число> '0') = 2 × М_b(<двоичное_число>);

М_b(<двоичное_число> ‘1’) = + 2 × М_b(<двоичное_число>) + 1.

Мы заключили синтаксические цифры в апострофы, чтобы отличать их от математических цифр. Отношение между этими категориями подобно отношениям между цифрами в кодировке ASCII и математическими цифрами. Когда программа считывает число как строку, то прежде, чем это число сможет использоваться в программе, оно должно быть преобразовано в математическое число.

Пример 2.7. Описание значения десятичных синтаксических литеральных констант.

<десятичное_число> → 0|1|2|3|4|5|6|7|8|9;

| <десятичное_число> (0|1|2|3|4|5|6|7|8|9).

Денотационные отображения для этих синтаксических правил имеют следующий вид:

M_d(‘0') = 0, M_d('1') = 1, ,..., M_d('9') = 9;

М_d(<десятичное_число> '0') = 10 × М_d(<двоичное_число>);

М_d(<десятичное_число> ‘1’) = 10 × М_d(<десятичное_число>) + 1;

…

М_d(<десятичное_число> '9') = 10 × М_d(<десятичное_число>) + 9.

Денотационную семантику программы можно определить в терминах изменений состояний идеального компьютера. Подобным образом определялись операционные ceмантики, приблизительно так же определяются и денотационные. Правда, для простоты они определяются только в терминах значений всех переменных, объявленных в программе. Операционная и денотационная семантики различаются тем, что изменения состояний в операционной семантике определяются запрограммированными алгоритмами, а в денотационной семантике они определяются строгими математическими функциями. Пусть состояние s программы определяется следующим набором упорядоченных пар: {<i₁, v₁>, <i₂, v₂>, …, <i_n, v_n>}.

Каждый параметр iявляется именем переменной, а соответствующие параметры v являются текущими значениями данных переменных. Любой из параметров v может иметь специальное значение undef, указывающее, что связанная с ним величина в данный момент не определена.

Пусть VARMAP - функция двух параметров, имени переменной и состояния программы. Значение функции VARMAP(i_k, s) равно v_k(значение, соответствующее параметру i_k в состоянииs).

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

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

<выражение> → <десятичное_число>| <переменная>

| <двоичное_выражение>

<двоичное_выражение> → <выражение_слева><оператор>

<выражение_справа>

<оператор> → + | ×

Единственной рассматриваемой нами ошибкой в выражениях является неопределенное значение переменной. Разумеется, могут появляться и другие ошибки, но большинство из них зависят от машины. Пусть Z - набор целых чисел, a error - ошибочное значение. Тогда множество Z {error} является множеством значений, для которых выражение может быть вычислено.

Ниже приведена функция отображения для данного выражения Е и состояния s. Символ  обозначает равенство по определению функции.

M_e(<выражение>, s) 