Информационные технологии

(2) fR (t) = ,

если вычисление по R для входного слова t не заканчивается.

Тогда мы говорим: алгоритм R вычисляет функцию fp .

Обратим внимание, что для слов t, для которых выполнение СТЗ не завершается, отображение fR дает результат . Символ , таким образом, обозначает (псевдо)результат незавершающегося вычисления. С помощью введения этого символа обходят явную работу с частичными отображениями.

Если слова t V* понимать как представления определенных информации из множества А, т. е. существует функция интерпретации такая, что (А, V*, I) образует информационную систему, и если функция fR , индуцируемая алгоритмом R, согласована с интерпретацией, то R индуцирует также функцию между информациями, т. е. R индуцирует отображение интерпретаций.

Вычислительные структуры

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

Семейства функций и множеств как вычислительные структуры

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

Определение (вычислительная структура). Пусть S и F - множества обозначений; вычислительная структура А состоит из семейства {sА: s S} носителей sА и семейства {fА: f F} отображений fА между этими носителями. Мы пишем:

А=({sА: s S}, {fА: f F}).

Элементы s S есть обозначения для носителей и называются типами. Элементы f F есть обозначения для отображений и называются символами функции или знаками операций. Для каждого f F существует 1 одно n N такое, что имеет место: fА есть n-местная функция, и существуют типы s1…. sn+1 S такие, что

Может также быть и n = 0, т. e. допускаются и "нульместные" отображения. Это такие отображения, которые (с пустым списком аргументов) получают в точности один элемент из области значений.

Для устранения частичных отображений снова используется специальный элемент ("дно") для представления неопределенного значения функции. Пусть М - множество, не содержащее . Множество M1 определяется как

M'=M U {}.

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

Отображение

f:M1 x...x Mn Mn+1

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

Пример

(1) Вычислительная структура BOOL булевских значений Множество S типов вычислительной структуры BOOL задано так:

S = {Ьоо1}. Множество F символов функций структуры BOOL задано так:

F = {true, false, -, v, ^}.

Множество носителей В1 сопоставлено типу Ьоо1, т. e. имеет место

boo|BOOL=B'= {L, О, }.

Символы из F обозначают следующие функции:

trueBOOL: . B',

faiseBOOL: B',

-bool : B' B' (бесскобочный префикс),

^ ВооL: B' х В' В' (инфикс),

v BOOL: B' х В' В' (инфикс).

Причем для a, b В имеет место

trueBOOL = L,

falseBOOL =o,

- bool b = not(b),

a vBOOL b = or(a, b),

а ^BOOL b = and(a, b).

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

Сигнатуры

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

Определение (сигнатура). Сигнатура - это пара (S, F) множеств S и F, причем

S обозначает множество типов, т. е. имен для носителей;

F обозначает множество символов (имен) функций;

для каждого символа функции f F пусть задана ее функциональное

fct f S+.

В дальнейшем для улучшения читаемости при задании функциональности для f мы будем писать

fct f=(S1,..., Sn)Sn+l,

чтобы выразить, что fА в вычислительной структуре А с соответствующей сигнатурой используется для обозначения отображения

Пример (сигнатуры). Сигнатура вычислительной структуры BOOL булевских значении и натуральных чисел из вышеприведенного примера дает пример сигнатуры.

smat = (bool,),

fbool = {true, false, -i, v, ^},

fct true = bool,

fct false = bool,

fct ~ = (bool) bool (бесскобочный префикс),

fct v = (bool, bool) bool (инфикс),

fct ^ = (bool, bool) bool (инфикс),

Рис.2.3. Диаграмма сигнатуры

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

Задания одной только сигнатуры, конечно, недостаточно для того, чтобы однозначно охарактеризовать вычислительную структуру. Имеется много различных вычислительных структур с одной и той же сигнатурой.

Вычислительные структуры указывают на структурные свойств информационных систем. В частности, имеет место:

({sА : s S}, S, T)

образует снова информационную систему с

Т: S {sА : s S, причем T[s] = sА

Также

({fА: f F}, F, I) с I: F {fА: f F},

причем I[f] = fА являет информационной системой.

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

Основные термы

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

(i) каждый нульместиый символ функции f F с fct f = s образует основной терм типа s;

(ii) каждая последовательность символов

f(t1, ..., tn) с f F и fct f= (S1, ..., Sn) s

есть основной терм типа s, если для всех i, 1 <= i <= n, ti есть основной терм типа si.

Множество всех основных термов сигнатуры обозначим через W, a множество основных термов типа s - через Ws. Если не существует нульместных символов функций, то множество W пусто.

Если имеется вычислительная структура А с сигнатурой , то основные термы в А допускают интерпретацию. Переход от основного терма (представления) типа s к соответствующему элементу а из множества А называют интерпретацией t в А. Интерпретация IA поэтому означает отображение

IA: W {а sA; s S}.

Для каждого основного терма t запись IA[t] обозначает интерпретацию I в А. Пишут также tA вместо IA[t]. Интерпретация получается заменой в основном терме символов функций на соответствующие функции:

IA[f(t1,...,tn)]=fA (IA[t1] ,.., IA[tn]).

В классической математике часто заданная интерпретация опускается и вместо tA просто записывается t; разницей между основным термом и его интерпретацией там сознательно пренебрегают.

Для каждой вычислительной структуры А сигнатуры основные термы типа s S могут использоваться как представления элементов из множества sA, которые связаны с типом s в А. Если для каждого элемента а (<>) носителей из А имеется представление терма, т. е. для каждого s и каждого а sA (<>) существует основной терм типа s с tA = а, то А называется термопроизводимой, это равносильно требованию, что в соответствующей информационной системе отображение интерпретаций является сюръективным.

Интерпретация ("значение") основного терма допускает соответственно вычисление терма. Один из простых способов организации такого вычисления представляют собой схемы.

Вычисления основных термов: схемы

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

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

Примеры (схемы).

(1) Основному терму ((1 + 2) * 3) - 4 с интерпретацией в N соответствует схема, показанная на рис. 2.4.



Рис. 2.4. Вычислительная схема

(2) Основному тepмy (true ^ false) v (false v ((~false ^ true)) с интерпретацией в BOOL соответствует схема, приведенная на рис. 2.5.

true

false

false

false

true

Рис. 2.5. Вычислительная схема

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

Термы с (свободными) идентификаторами

Идентификатор ("обозначатель", "переменная", "неизвестное") - это держатель места ("имя") для терма (или элемента), который (позднее) может быть подставлен на это место. Идентификаторы могут пониматься как имена термов или элементов, которые будут конкретизированы только позднее.

Пусть = (S, F) - сигнатура, и Х = {Xs: s S} - семейство множеств идентификаторов. Пусть множества Xs идентификаторов попарно не пересекаются и отличны от символов функций в F. W(X) обозначает алгебру термов, распространенную на X, т. е.

WI с I = (S, F u {х Xs: s S}) и fct x = s

для х Хs, где Xs обозначает множество идентификаторов (держателей мест, обозначений) типа s.

Примеры (термы с идентификаторами).

Уравнения с "неизвестными" в математике - это уравнения между термами с идентификаторами, например ax2 + bx + с = 0.

(2) Часто термы снабжаются свободными идентификаторами,чтобы определять функции. Функция f может быть определена через:

f: N N с f(x) = 2х+ 1

Термы со свободными идентификаторами называются также полиномами. Вместо идентификаторов в термы могут подставляться другие термы. Соответствующее отображение называется подстановкой в термы с (свободными) идентификаторами.

Пусть t - терм с идентификаторами, х - идентификатор типа s и г -терм типа s; через t [г/х] обозначается терм, который получается, когда идентификатор х заменяется на г. Этот процесс называется подстановкой.

Подстановки описываются формально, аналогично построению термов, с помощью следующих уравнении:

x [t/x] = t,

у [t/x] = у, если х и у - различные идентификаторы,

f(tl,...,tn)[t/x]=f(t1[t/x],...,tn[t/x]), где f F с fct f= (S1, .... Sn) Sn+1

и термы ti имеют типы si;.

Через t [t1|/X], ..., tn/Xn] обозначается терм, который возникает из терма t при одновременной подстановке ti вместо (попарно различных) идентификаторов Xi.

Пусть t - терм с (свободными) идентификаторами. Терм г назовем экземпляром t, если г получается из t путем замены (подстановки) в нем определенных (свободных) идентификаторов.

Интерпретация термов с (свободными) идентификаторами

Пусть А - вычислительная структура с сигнатурой

= (S, F), а Х

- семейство множеств идентификаторов. Отображение

b: {х Xs: s S} {а sA : s S},

которое каждому идентификатору х в X типа s ставит в соответствие элемент а sA структуры данных sA типа s, называется конкретизацией Х (в А).

Для каждой конкретизации b определяется интерпретация IAb терма t со свободными идентификаторами из Х с помощью следующих равенств:

IAb[x]=b(x), IAb [f(t1,…,tn)]=fA(IAb [t1],…, IAb [tn])

лтя n = 0 получается IAb [f] = fA .

Термы с (свободными) идентификаторами как схемы

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

Пример (из геометрии). Площадь S кольца s с внутренним радиусом г и внешним радиусом R получается по формуле

S = (R2 - r').

Терму в правой части формулы соответствует схема, приведенная на рис. 2.7.

Pw. 2.7. Вычислительная схема

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

Если в терме определенные идентификаторы встречаются многократно, то вместо схем типа дерева получают "Наsse"-диаграммь1 (т. е. ациклические ориентированные графы).

Пример (схема с многократно применяемым промежуточным результатом). Терм (х - у) * (х + у) обладает схемой, показанной на рис. 2.8.

Рис.2.8. Вычислительная схема

Термы могут использоваться в системах замены термов для представления алгоритмов.

Алгоритмы как системы подстановки термов

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

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

Правила подстановки термов

Для заданной сигнатуры и заданного семейства Х множеств идентификаторов пара (t, r) термов t, r одинакового типа с (свободными) идентификаторами из Х называется подстановкой термов (правилом подстановки термов - ППТ) или также схемой подстановки термов. Правило записывается в виде t г.

В большинстве случаев для ППТ требуется, чтобы все идентификаторы, встречающиеся в г, также входили в t. Если в t и г заменяют определенные идентификаторы Х1, ..., Xn на термы t1, ..., tn подходящих типов, то получают экземпляр (частный, конкретный случаи) правила. Соответственно

t [ t1/X1, ..., tn/Xn ] r [ t1/X1, .... tn/Xn]

называется экземпляром правила t г. Если t и г - основные термы, то экземпляр называется полным.

Пример (экземпляры правил подстановок термов). Для правила

pred (succ (x)) х примерами экземпляров являются:

pred (succ (zero)) zero, pred (succ (succ (у))) succ (у).

Из правила получаются шаги подстановки термов благодаря тому, что правило применяется к любому подтерму имеющегося терма.

Пусть t --> г есть экземпляр правила. Пусть задан терм с, в котором встречается свободный идентификатор х; тогда

С [t/Х] С [r/Х]

называется (безусловным) применением правила (к. терму c[t/x]). Tepм t называется редексом, а вхождение х в с - местом применения.

Пример (применение правила замены термов). К терму

succ (succ (pred (succ (zero)))) может быть применено правило предыдущего примера. Это дает:

succ (succ (pred (succ (zero)))) --> succ (succ (zero)).

Аналогом алгоритмов в виде подстановки текстов являются алгоритмы в виде систем подстановки термов (алгоритмы подстановки термов - АПТ).

Система подстановки термов

Множество (в общем случае конечное) R правил подстановки термов на сигнатуре называется системой подстановки термов (СПТ) над . Если для последовательности термов ti (0 <= i <= n) справедливо для i=0,...,n-l:

(*). ti, --> ti+1 есть применение правила из системы подстановки термов R, то последовательность термов является вычислением в R для to.

Терм t называется терминальнымдлясистемыR,еслине существует герма г такого, что t г есть применение правила из R.

Если в вычислении, заданном с помощью термов ti 0 <= i <= n, терм tn является терминальным, то вычисление называется терминированным (завершающимся), a tn -результатом или выходом вычисления для входа to.

Бесконечная последовательность (ti)iN термов, удовлетворяющих приведенному выше условию (*), называется нетерминированным (незавершающимся) вычислением R для to. Система R называется в общем случае терминированной, если не существует незавершающихся вычислений.

Терминальные основные термы определяют нормальную форму. Они часто также называются термами в нормальной форме относительно R. Над системой R мы можем терму t поставить в соответствие терминальный терм г в качестве нормальной формы, если г есть результат вычислений с входом t. Как правило, система нормальных форм, индуцированных через СПТ, не является ни однозначной, ни полной. Термы, для которых существуют только бесконечные вычисления, не имеют нормальных форм. Для определенных термов могут существовать вычисления с различными результатами.

Пример (СПТ для вычислительной структуры BOOL). Ниже символы

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

(~true) false, (~false) true, (false v x) x, (x v false) x, (true v true) true

Эта СПТ редуцирует каждый основной терм типа bool к терму true или false.

Снова повторное применение ППТ из заданного множества правил мы можсм трактовать как алгоритм, который работает с термами в качестве входа и выхода.

Алгоритмы подстановки термов

Пусть задана система подстановок R; R определяет алгоритм в силу следующего предписания (алгоритм получает в качестве входного слова основной терм t):

(1) Если R содержит правило подстановки с применением t г, то далее алгоритм продолжается с использованием г вместо t.

(2) Если R не содержит правила подстановки с применением t г, то алгоритм закашивается с г в качестве результата.

Алгоритм подстановки термов (АПТ) тем самым выполняет вычисление в R для каждого основного терма t. Часто вычисление состоит в решении задачи преобразовать заданный основной терм в определенную заранее заданную нормальную форму.

Если АПТ начинает работать с заданным основным термом t, то t называют также входом для алгоритма; если алгоритм завершается основным термом г, то г называется также выходом или результатом.

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

Основные композиции действий и их правила вывода. Соотношения для корректности программ

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

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



Рис. 1. Алгоритм для нахождения q и r-, удовлетворяющих условиям x=q*y+r и 0 <= г < y. Таким образом, на выходе q = х div y и r=х mod y.

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

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

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

Рассмотрим рис. 1, который воспроизводит алгоритм для определения х div у и х mod у. Заметим, что состояние вычислений, связанное с точкой входа, определяется значениями входных переменных х и у; но после выполнения первых двух операторов состояние вычислений расширяется, включая значения четырех переменных: х, у, q и г. (Значения х и у могут быть различными



в зависимости от применения алгоритма, но остаются постоянными в течение одного применения). Ясно, что следующая за проверкой r >= у передача управления будет зависеть от текущего состояния вычислений.

Фундаментальное свойство всех видов композиции, которые мы будем рассматривать, заключается в том, что они дают возможность объединить в одну сложную структурную схему с одним входом и одним выходом одну или более схем также с одним входом и одним выходом. Как показано на рис. 1, наша процедура проектирования объединяет с этими точками некоторые соотношения, которые описывают существенные аспекты состояний вычислений в этих точках. Каждая такая структурная схема имеет вид, приведенный на рис. 2А, где S может быть отдельным действием ЭВМ или сложной схемой. Чтобы выразить ее в более краткой форме, используем нотацию:

{Р} S {Q}. (1)

Это - спецификация программы со следующим смыслом: если соотношение Р истинно перед выполнением S, то Q будет истинно после завершения выполнения S. Другими словами, если Р истинно при входе, то Q будет истинно при выходе.

Если S -- программа, чью корректность мы хотим установить, то нотация (1) в том смысле, как мы ее определили, -- это то, что мы хотим доказать, причем Р -- соотношение, которому должны удовлетворять начальные значения переменных, а Q -- соотношение, которому должны удовлетворять конечные значения переменных. Например, если S - алгоритм, изображенный на рис. 1, то соотношение, которое мы хотим доказать, таково:

{(х >= 0)^(y > 0)} S {(х = q *у + r)^(0<= r < у)}, (2)

где знак ^ используется в качестве формальной нотации для "и".

Как уже отмечалось, соотношение {Р} S {Q} означает, что если P истинно перед выполнением S, то Q должно быть истинно при завершении S. Это означает, что {Р} S {Q} тождественно истинно, если S не завершается, т. е. если на рис. 2А точка выхода никогда не достигается. Другими словами, (1) определяет только частичную корректность S. Частично корректной является такая программа, в которой гарантируется получение требуемого результата при условии ее завершения. Но завершается ли программа действительно для некоторых исходных значений -- это другой вопрос. Если дополнительно можно показать, что программа завершается для всех исходных значений, удовлетворяющих соотношению Р, то говорим, что программа полностью корректна. Чтобы доказать завершение программы, получаемой применением правил композиции, введенных ранее, необходим анализ циклов, т.е. операторов итерации.

Можно подвести итог нашему подходу к проектированию программ.

1. Проектирование должно начинаться со спецификации {Р} S {Q}, которой должна удовлетворять проектируемая нами программа. Мы начинаем, таким образом, .с ясного и недвусмысленного определения того, когда программа должна использоваться (предусловие Р), и результата ее использования при этом (постусловие Q).

2. Процесс проектирования сверху вниз определяет спецификации [Рi} Si {Qi} для компонентов Si, из которых строится программа.

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

Правила вывода для простых операторов

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

Два простейших правила вывода формулируются в (2.27) и (2.30). Первое утверждает, что если выполнение программы S обеспечивает истинность утверждения R, то оно также обеспечивает истинность каждого утверждения, которое следует из R, т. е.

[P}S{R}, R Q

{P}S{Q}

Например, из

{(х > 0)^(у > 0)} S{(z+u *у = х *у)^(и = 0)}, (2.28)

(z+u*y=x*y)^(u=0)(z=x*y) (2.29)

заключаем, используя (2.27), что

{(х > 0) ^ (у > Q)} S {z = х * у].

Второе правило утверждает, что если R - известное предусловие программы S, приводящей к результату Q после завершения своего выполнения, то это же относится к любому другому утверждению, из которого следует R:

PR, [R}S{Q}

{P}S{Q}

Правила (2.27) и (2.30) называются правилами консеквенции.

Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор -- тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода

{Р}{Р}. (2.32)

Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р

{PXe}x:=e{P}. (2.33)

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

Составные и условные операторы

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

Составные операторы

Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состоящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)

и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).

Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:

{Р} S, [R], {R} S, {Q}

{Р}begin Si;S, end {Q} (2-36)

Правило вывода (2.36) обобщается следующим очевидным образом:

{Рi-1}S1{Pi} дпя i=1,....n

{P0} begin S1;. ..Sn. end {Pn}

Условные операторы.

Если S1 и S2 - операторы, а В -- Булево выражение (т.е. выражение, имеющее значение Булевого типа), то

if В then S1 else S2 (2.38)

есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае -- действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).



Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность

[Р] if В then S1 else S2 {Q},

то необходимо доказать два утверждения.

1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.

2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^ ~В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^~b}s2{q].

Если мы доказали как [Р^В] S1 {Q}, так и{Р^ ~В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода:

{P^B}S1{Q},{P^~B}S2{Q}

{Р} if В then S1 else S2 {Q}

Теперь рассмотрим два варианта условного оператора и обеспечим для каждого правила вывода. Первый вариант получается, когда мы замечаем, что в if B then S1 else S2 S2 может быть любым и, в частности, пустым оператором. Пустой оператор определяет тождественную операцию, т. е. операцию, не воздействующую на значения переменных. Если S2 -- пустой оператор, то (2.38) запишется так:

if B then S. (2.41)

Действие, которое определяется этим оператором, вначале состоит в вычислении В. Если В истинно, то должно быть выполнено действие, определяемое S, иначе должна быть выполнена тождественная операция. Выражение (2.41) можно представить рис. 2Д.

Теперь определим соответствующее правило вывода. Если мы хотим доказать {P} if B then S{Q}, то необходимо обеспечить два условия. Первое из них заключается в том, что если S выполняется, то Q справедливо после его завершения. Так как при условии истинности В для выполнения выбирается S, то выводим, что Р /\В справедливо перед выполнением S, если Р справедливо перед выполнением (2.41). Итак, требуется доказать {p^b}s{q}. Второй случай имеет место, когда S не выполняется, т.е. когда после вычисления В получается значение ложь. Итак, в этой точке справедливо Р ^ ~В, и если Q справедливо после выполнения (2.41), то необходимо доказать, что Р ^ ~В Q. Альтернативой получения правила вывода является рассмотрение (2.41) в эквивалентной форме:

if B then S else. (2.42)

В (2.42) после else идет пустой оператор. Но в любом случае правило вывода формулируется следующим образом:

{P^B}S{Q},P^~BQ

{Р} if В them S {Q}

Операторы итерации

Теперь обратимся к структурам, которые приводят к циклам. Сначала изучим конструкцию while-do, а затем repeat-until.

Операторы while-do

Если В -- Булево выражение и S -- оператор, то

while В do S (2.47)

обозначает итерационное выполнение оператора S, пока В истинно. Если В ложно с самого начала, то S не будет выполняться совсем. Процесс итерационного выполнения S оканчивается, когда В становится ложным. Эта ситуация изображена на рис. 2Ж.

Задав любое начальное неотрицательное целое значение п, можно воспользоваться этим оператором для вычисления суммы I2 + 22 + ... +п2, получаемой как конечное значение h в следующей программе:

begin h := 0;

while n > 0 do begin h: = h + n *n; n: = п - 1 end

Теперь необходимо изучить утверждение {Р} while В do S {Q}, для чего рассмотрим рис. 2Ж более подробно, т. е. перейдем к рис. 23. Если Р справедливо, когда мы впервые входим в рис. 23, то ясно, что Р^В будет справедливо, если мы достигнем точки С Тогда если мы хотим быть уверенными, что Р снова выполняется при возврате в точку А, нам необходимо обеспечить истинность для S утверждения {Р ^ В} S {Р}.

В этом случае ясно, что Р будет выполняться не только тогда, когда точка А на рис. 23 достигается первый или второй раз, но и после произвольного числа итераций. Аналогично Р ^ В выполняется всякий раз, когда достигается точка С. Когда достигается точка выхода D (см. рис. 23), то справедливо не только Р, но и ~В. Итак, получаем следующее правило вывода:

{p^b}s{p}

{Р} while В do S {Р ^ ~В}

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

Операторы repeat-until

Другая форма оператора итерации:

repeat S until В, (2.50)

где S -- последовательность операторов и В -- Булево выражение. Оператор (2.50) определяет, что S выполняется перед вычислением B. Затем, если В ложно, процесс итерационного выполнения S продолжается, в противном случае он завершается. Структура оператора итерации (2.50) представлена на рис. 2И.

Сравнивая рис. 2Ж и 2И, замечаем, что на рис. 2И S должен быть выполнен по меньшей мере один раз, в то время как на рис. 2Ж он может не выполняться совсем.

Пример оператора repeat-until дан в программе (2.51), которая вычисляет сумму h=12+22+...+n2 для заранее заданного значения п:

begin h:=0;

repeat h: = h + n * п;

п := п -- 1

until n= 0 (2.51) end

Предположим, что допускаются отрицательные значения п. Тогда можно использовать (2.48) и (2.51) для иллюстрации фундаментальной проблемы, связанной с итерационной композицией, когда мы заинтересованы в полной, а не в частичной корректности. Если n<=0, то (2.51) является бесконечным циклом. С другой стороны, программа (2.48) завершается, даже если n<=0. Таким образом, видим, что неправильно спроектированный оператор итерации может фактически описывать бесконечное вычисление.

Чтобы установить правило вывода для repeat S until В, рассмотрим рис. 2К. Предположим, доказано, что

{Р} S {Q} и Q ^~B Р.

Тогда если Р истинно в точке входа, то Q будет истинно, когда точка С достигается в первый раз.

Если В ложно, то истинно Q ^ ~В, и при прохождении через цикл вновь достигается точка А. Так как Q/\~В .Р, то, следовательно, Р удовлетворится при достижении точки А во второй раз (если это вообще происходит). Но тогда вновь на основании [Р] S {Q} будет удовлетворяться Q, когда точка С достигается во второй раз, и т.д. Итак, видно, что при сделанных предположениях Р будет истинно всякий раз, когда достигается точка А, и Q будет истинно всякий раз, когда достигается точка С, независимо от числа повторений цикла. Когда итерационный процесс заканчивается, т.е. когда достигается точка выхода D на рис. 2К, то должно быть истинно утверждение Q^B. Это рассуждение приводит к следующему правилу вывода:

{P}S{Q},Q^~BP

{Р} repeat S until B{Q^B]