Значение заголовка программы и точки.

ИСЧИСЛЕНИЕ ПОСЛЕДОВАТЕЛЬНЫХ ПРОГРАММ.

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

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

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

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

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

Значение частей программы.

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

Новые идеи: Состояния выполнения, композиция отношений и функций, обратная функция, транспонирование, значение блоков и объявлений.

Целью программного исчисления является вычисление P для любой программы CF Pascal P в терминах компонентов P. Разбиение программы на части производится в соответствии с ее синтаксисом.

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

Состояния выполнения.

В таблице выполнения кроме INPUT и OUTPUT могут присутствовать другие переменные программы для описания действий Паскаль-машины, таких как объявление переменных, присваивание им значений и т.д. Строки в INPUT и OUTPUT и значения переменных программы образуют ее рабочие данные.

Допустим, что частично задана следующая программа.

PROGRAM Copy1 (INPUT, OUTPUT);

VAR

Ch1: CHAR;

Ch2: CHAR;

F1: TEXT;

BEGIN

REWRITE(F1);

Ch1:= ‘B’;

READ(Ch2);

WRITE(F1, Ch2);

…

END.

Ее таблица выполнения для входа ABC начинается:

	INPUT	OUTPUT	F1	Ch1	Ch2
PROGRAM Copy1 (INPUT, OUTPUT); VAR Ch1: CHAR; Ch2: CHAR; F1: TEXT; BEGIN REWRITE(F1); Ch1:= ‘B’; READ(Ch2); WRITE(F1, Ch2); … END.	ABC/   ABC/	_	?   _     A_	?     B	?     A

Значения переменных INPUT, OUTPUT, F1, Ch1, Ch2 являются основными элементами истории выполнения программы. Основная информация в таблице выполнения – список переменных и их текущих значений (информация одной строки таблицы). Для описания строки таблицы выполнения со значениями переменных наиболее подходит множество пар идентификатор-величина. Например, состояние после выполнения оператора READ может быть представлено в виде 5-множества пар:

s = {<†INPUT†, <†A†, †BC†Ñ/, R>>, <†OUTPUT†, <††, ††, W>>,

<†F1†, <††, ††, W>>, <†Ch1†, B>, <†Ch2†, A>}

Каждому идентификатору сопоставлена величина соответствующего типа. Например, для INPUT – 3-список, имеющий строку прошлого <†A†, строку будущего †BC†Ñ/, и состояние выполнения R.

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

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

Значение части программы (частное значение) – функция или отношение, которое связывает между собой два состояния выполнения соответствующие двум соседним строкам в таблице выполнения. Например, состояние выполнения, следующее за s, будет:

t = {<†INPUT†, <†A†, †BC†Ñ/, R>>, <†OUTPUT†, <††, ††, W>>,

<†F1†, <†A†, ††, W>>, <†Ch1†, B>, <†Ch2†, A>}

Состояние t практически идентично состоянию s да исключением пары <†F1†, <†A†, ††, W>>, изменение которой отражает выполнение оператора WRITE. Программное исчисление предполагает правило для оператора WRITE, которое позволит получать состояние t из s без использования других частей программы, в результате выполнения которых получается s.

Поскольку s и t – функции, мы можем использовать функциональную запись (value-нотация).

s(†INPUT†) = <†A†, †BC†Ñ/, R>

t(†Ch1†) = B

Состояния выполнения для первых строк программы не так очевидны. В заголовке программы F1, Ch1, Ch2 не имеют значений, потому что еще не определены. Поэтому эти переменные не входят в состояние выполнения для данной строки.

u = {<†INPUT†, <††, †ABC†Ñ/, R>>, <†OUTPUT†, <††, ††, W>>}

Состояние выполнения u – функция, область определения которой множество

{<†INPUT†, <†OUTPUT†}

Поскольку в дальнейшем u переходит в s, очевидно, что часть программы может изменить не только значение функции, но и ее область определения. После объявления переменных F1, Ch1 и Ch2 они принимаю неопределенное значение, обозначенное знаком вопроса. Таким образом, объявление переменной Ch1 порождает набор состояний, каждое из которых будет иметь следующую форму

v = {<†INPUT†, <††, †ABC†Ñ/, R>>, <†OUTPUT†, <††, ††, W>>, <Ch1, x>}

где x – любой символ. Значением части программы будет одно из множества состояний, заданных v, но мы не знаем какое именно. Используя функциональную форму записи, мы можем сказать, что v(†Ch1†) равно некоторому неизвестному символьному значению, которое будет удобно обозначать символом знак вопроса, помня при этом, что ? в данном не является символьным литералом.

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

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

При таком подходе состояние s будет записано как:

s = {INPUT·<†A†, BC/, R>, OUTPUT·<††, ††, W>, F1·<††, ††, W>, Ch1·B, Ch2·A}

Значение заголовка программы и точки.

Первая и последняя части программы – заголовок и точка имеют специальную роль в программном исчислении. Они связывают внутренние частные значения (состояния выполнения) программы с внешними значениями программы. Соответствие между внешними и внутренними значениями задается через INPUT и OUTPUT, которые появляются в состояниях выполнения как переменные, но вне программы их содержимое – списки строк.

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

L = <L₁, L₂, …, L_n>

Преобразуется в строку

(L₁Ñ/)&(L₂Ñ/)& …&(L_nÑ/)

которая становится значением строки будущего для INPUT.

Для данного заголовка программы

H = †PROGRAM† & N & †(INPUT, OUTPUT)†

для любого идентификатора N, частное значение H будет:

H = {<<L₁, L₂, …, L_n>, s>: s = {INPUT ·<††, x, R>, OUTPUT ·<††, ††, W>}

где x = (L₁Ñ/)&(L₂Ñ/)& …&(L_nÑ/) }

Если воспользоваться сокращенной формой записи и опустить маркеры строк, то можно записать:

H = PROGRAM N (INPUT, OUTPUT)

где N - идентификатор

PROGRAM Copy1 (INPUT, OUTPUT) (†AB†, †CD†) =

{INPUT ·<††, (†AB†Ñ/)&(†CD†Ñ/) , R>, OUTPUT ·<††, ††, W>}

При завершении выполнения точка преобразует строку прошлого OUTPUT в выход программы, а именно список символьных строк. Разбиение на элементы списка производится с помощью маркеров строки.

Таким образом, значение точки будет

.= {<s, <L₁, L₂, …, L_n>>: s(OUTPUT) = <(L₁Ñ/)&(L₂Ñ/)& …&(L_nÑ/), ††, W>}

Остальные пары в s, кроме той, что содержит OUTPUT, теряются. Например:

.({INPUT ·< ABCÑ/, †† , R>, OUTPUT ·<(ABÑ/)&(CDÑ/), ††, W>}) =

<†AB† ,†CD† >

что будет распечатано как

AB

CD

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