Значение последовательных выражений.

Раздел определяет значение операторов CF Pascal, таких как: присваивание, пустой оператор, оператор BEGIN, WRITE, READ и простых процедур.

Новые идеи: Семантика операторов.

Последовательные программы не имеют операторов IF или WHILE, поэтому поток управления проходит от первого до последнего оператора. Для каждого вида операторов CF Pascal будет определено его частное значение, которое соответствует преобразованиям над состояниями выполнения, выполняемым данным оператором. Мы будем использовать Box-нотацию для обозначения частного значения оператора.

Оператор присвоения.

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

Box-нотация может быть расширена, чтобы обозначать значение выражения в правой части оператора присвоения. Частное значение такого выражения – это значение, взятое для данного состояния выполнения. Если оператор присвоения:

Ch1 := Ch2;

выражение справа – символьное выражение, представленное переменной, и ее значение доступно в данном состоянии выполнения. Рассмотрим значение символьной переменной, используя следующий пример.

В состоянии, содержащем пару Ch2·B, символьная переменнаяCh2 имеет значение B. Таким образом, для идентификатора W, объявленного как CHAR, частным значением выражения W для состояния s является W(s).

W = {<s, s(W)>}

Например:

Ch ({INPUT ·<††, ††, R>, OUTPUT ·<††, ††, W>,Ch·F, V1·C})

= {INPUT ·<††, ††, R>, OUTPUT ·<††, ††, W>,Ch·F, V1·C}(Ch)

= F

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

‘A’ (s) = A

‘B’ (s) = B

и т.д.

Определение частного значения символьного выражения позволяет нам рассмотреть определение частного значения оператора присвоенияс идентификатором V в левой части и выражением E в правой части:

V:= E = {<s, t>: t = (s – {<V, c >: c - символ}) È {<V, E (s)>}}

Разность множеств удаляет старое значение V из состояния выполнения, объединение добавляет соответствующее новое значение.

Для идентификаторов V1 и V2 и символьного выражения, представленного литералом ‘A’, определение будет выглядеть как:

V1 := V2 ={<s, t>: t = t такое же как s за исключением V1 (t) = V2(s)}

V1 := ‘A’ ={<s, t>: t = t такое же как s за исключением V1 (t) = A}

Примеры:

V1 := ‘B’ ({V1·A, …}) = {V1·B, …}

V2 := V1 ({V1·A, V2·B ,…}) = {V1·A, V2·A, …}

V1 := V2 ({V1·?, V2·A ,…}) = {V1·A, V2·A, …}

V1 := V2 ({V1·A, V2·? ,…}) = {V1·?, V2·?, …}

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

Часть программы	Область определения	Область значений
программа	список строк	список строк
заголовок программы	список строк	состояния выполнения
точка	состояния выполнения	список строк
блок	состояния выполнения	состояния выполнения
объявление	состояния выполнения	состояния выполнения
оператор	состояния выполнения	состояния выполнения
символьное выражение	состояния выполнения	символьное значение

Пустой оператор.

Пустой оператор ничего не выполняет, следовательно не изменяет состояние выполнения. Значением для такого поведения является функция эквивалентности I. Таким образом:

= I = {<s, s>}

Оператор BEGIN

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

BEGIN

END

содержит пустое выражение.

Значение оператора BEGIN может быть определено через значения входящих в него операторов. Пусть S будет одиночный оператор, T – последовательность из одного или более операторов, разделенных точкой с .запятой.

BEGIN S END = S

BEGIN S; T END = S ◦ BEGIN T END

Например:

BEGIN V1 := V2; V2 := V3 END

= V1 := V2 ◦ BEGIN V2 := V3 END

и

BEGIN V1 := V2; V2 := V3; V3 := V4 END

= V1 := V2 ◦ BEGIN V2 := V3; V3 := V4 END

= V1 := V2 ◦ V2 := V3 ◦ V3 := V4

Оператор BEGIN может изменять значения нескольких переменных. Например:

BEGIN V1 := ‘A’; V2 := ‘B’ END ({V1·H, V2·K,…})

= V1 := ‘A’ ◦ V2 := ‘B’ ({V1·H, V2·K,…}) (1)

= V2 := ‘B’ (V1 := ‘A’({V1·H, V2·K,…}) ) (2)

= V2 := ‘B’ ({V1·A, V2·K,…}) ) (3)

= {V1·A, V2·B,…} (4)

На шаге 1 частное значение оператора BEGIN представляется как композиция входящих в него операторов. На шаге 2 выражение приводится к функциональной форме записи. На шаге 3 вычисляется значение первого входящего оператора, и на шаге 4 – значение второго входящего оператора.

Оператор BEGIN может изменять значения одной переменной несколько раз. Например:

BEGIN V1 := ‘A’; V1 := ‘B’ END ({V1·H, V2·K,…})

= V1 := ‘A’ ◦ V1 := ‘B’ ({V1·H, V2·K,…})

= V1 := ‘B’ ({V1·A, V2·K,…}) )

= {V1·B, V2·K,…}

Перемещение двухсимвольного окна из V1, V2 в V2, V3 может быть проанализировано следующим образом:

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

BEGIN V1 := V2; V2 := V3; V3 := V1 END ({V1·X, V2·Y, V3·Z, …})

= V1 := V2 ◦ V2 := V3 ◦ V3 := V1 ({V1·X, V2·Y, V3·Z, …})

= V2 := V3 ◦ V3 := V1 ({V1·Y, V2·Y, V3·Z, …})

= V3 := V1 ({V1·Y, V2·Z, V3·Z, …})

= {V1·Y, V2·Z, V3·Y, …}

Оператор WRITE.

Значение файлов описывается 3-спискоми и действие операторов READ и WRITE было описано ранее в разделе 5.2.2. То описание может легко быть трансформировано в формальное значение через влияние операторов на состояния выполнения.

Пусть f будет файловый идентификатор, а c – символьное выражение.

REWRITE(f) = {<s, t>: t = (s – {<f, u>: u –3-список}) È {<f, <††, ††, W>>}}

WRITE(f, e) = {<s, t>: s(f) =< x, ††, W>, где x – строка,

t = (s – {<f, u>: u – 3-список}) È {<f, <xÑe(s), ††, W>>} }

WRITELN(f) = {<s, t>: s(f) =< x, ††, W>, где x – строка,

t = (s – {<f, u>: u – 3-список}) È {<f, <xÑ /, ††, W>>} }

Когда файловый идентификатор отсутствует, OUTPUT является файлом для выражений WRITE и WRITELN. Например:

WRITELN = {<s, t>: s(OUTPUT) =< x, ††, W>, где x – строка,

t = (s – {<OUTPUT, u>: u – 3-список}) È {<OUTPUT, <xÑ /, ††, W>>} }

Например:

REWRITE(F1) ({F1·<AXB, ††, W>, …}) = {F1·<††, ††, W>, …}

WRITE(F1, Ch) ({F1·<AB, ††, W>, Ch·C,…}) = {F1·<†ABC†, ††, W>, Ch·C,…}

WRITELN ({OUTPUT·<Line1, ††, W>, …}) = {OUTPUT·<Line1/, ††, W>, …}

Операторы WRITE, включающие несколько выражений, определяются как комбинации более простых операторов с композицией их значений:

WRITE(Ch, ‘A’) = WRITE(Ch) ◦ WRITE(‘A’)

WRITE(‘AB’) = WRITE(‘A’) ◦ WRITE(‘B’)

WRITELN(F1, Ch) = WRITE(F1, Ch) ◦ WRITELN(F1)

PROGRAM WriteHello (INPUT, OUTPUT);

VAR

LetterL: CHAR;

BEGIN

LetterL := ‘L’;

WRITELN(‘H’, ‘E’, LetterL, LetterL, ‘O’)

END.

Следующие вычисления определяют значение программы для входного 1-списка <†ABC†>

PROGRAM WriteHello … END. (<†ABC†>)

= (PROGRAM ◦ VAR … BEGIN … END. ◦ .)(<†ABC†>)

= VAR … BEGIN … END. ◦ .)({INPUT ·<††, ABC/, R>, OUTPUT ·<††, ††, W>})

= VAR … ◦ BEGIN … END. ◦ VAR …^T ◦ .

({INPUT ·<††, ABC/, R>, OUTPUT ·<††, ††, W>})

= BEGIN … END. ◦ VAR …^T ◦ .

({INPUT ·<††, ABC/, R>, OUTPUT ·<††, ††, W>, Letter·?})

= (LetterL := ‘L’ ◦ WRITELN(‘H’, ‘E’, LetterL, LetterL, ‘O’) ◦ VAR …^T ◦ .)({INPUT ·<††, ABC/, R>, OUTPUT ·<††, ††, W>, Letter·?})

= WRITELN(‘H’, ‘E’, LetterL, LetterL, ‘O’) ◦ VAR …^T ◦ .)

({INPUT ·<††, ABC/, R>, OUTPUT ·<††, ††, W>, Letter·L})

= (VAR …^T ◦ .)({INPUT ·<††, ABC/, R>, OUTPUT ·<†HELLO†, ††, W>, Letter·L})

= (.)({INPUT ·<††, ABC/, R>, OUTPUT ·<†HELLO†, ††, W>})

= <†HELLO†>

Таким образом, мы нашли значение программы для данного входа

PROGRAM WriteHello … END. (<†ABC†>)= <†HELLO†>

Оператор READ

Действия, выполняемые оператором READ, которые мы рассмотрели в разделе 5.2.2 также могут быть рассмотрены с точки зрения изменения состояний выполнения. Пусть f – файловый идентификатор, а c – символьная переменная, тогда:

RESET(f) = {<s, t>: s(f) = <x, y, R>, где x и y – строки,

t = (s – {<f, u>: u –3-список}) È {<f, <††, x&y, R>>}}

READ(f, c) = {<s, t>: s(f) = <x, y, R>, где x и y – строки, y ¹ ††

t = ((s – {<f, u>: u – 3-список}) – {<c, v>: v – символьное значение})

È {<f, <xÑ( Θ y), Λ y, R>>}

È {<c, Θ y >: Θ y ¹ /} È {<c, □>: Θ y = /}}

READLN(f) = {<s, t>: s(f) = <x, y, R>, где x и y – строки, y ¹ ††

y = (j Ñ / & k, / не подстрока j,

t = (s – {<f, u>: u – 3-список}) È {<f, <x & (j Ñ / ), k, R>>}}

Когда файловый идентификатор отсутствует, INPUT является файлом для выражений READ и READLN. Например:

READ(c) = {<s, t>: s(INPUT) = <x, y, R>, где x и y – строки, y ¹ ††

t = ((s – {<INPUT, u>: u – 3-список}) – {<c, v>: v – символьное значение})

È {<INPUT, <xÑ( Θ y), Λ y, R>>}

È {<c, Θ y >: Θ y ¹ /} È {<c, □>: Θ y = /}}

Примеры:

RESET(F1) ({F1·<AB,CD/,R>,…}) = {F1·<ABCD/,††, R>, …}

READ(F1, Ch) ({F1·<AB,CD/,R>, Ch·Q,…}) = {F1·<ABC, D/,R>, Ch·C,…}

READLN ({INPUT·<AB,CD/,R>,…}) = {INPUT·<ABCD/, ††,R>,…}

Значение более сложных операторов READ определяется через композицию более простых:

READ (Ch1, Ch2) = READ (Ch1) ◦ READ (Ch2)

READLN(Ch) = READ (Ch) ◦ READLN

В качестве примера рассмотрим программу:

PROGRAM Change2 (INPUT, OUTPUT);

VAR

C2:CHAR;

BEGIN

READ(C2);

WRITE(C2);

READ(C2);

WRITELN(‘2’);

END.

При вычислении PROGRAM Change2 END. (<†ABC†>) первые шаги аналогичны тем, которые предпринимались при вычислении значения WriteHello в предыдущем разделе.

PROGRAM Change2 END. (<†ABC†>) =

(PROGRAM Change2 ◦ VAR … ◦ BEGIN … END ◦ VAR …^T ◦ .) (<†ABC†>)

…

= ( BEGIN … END ◦ VAR …^T ◦ .)

({INPUT·<††, ABC/, R>, OUTPUT·<††, ††, W>, C2·?)

= ( READ(C2) ◦ WRITE(C2) ◦ READ(C2) ◦ WRITELN(‘2’) ◦ VAR …^T ◦ .)

({INPUT·<††, ABC/, R>, OUTPUT·<††, ††, W>, C2·?)

= ( WRITE(C2) ◦ READ(C2) ◦ WRITELN(‘2’) ◦ VAR …^T ◦ .)

({INPUT·<†A†, BC/, R>, OUTPUT·<††, ††, W>, C2·A)

= ( READ(C2) ◦ WRITELN(‘2’) ◦ VAR …^T ◦ .)

({INPUT·<†A†, BC/, R>, OUTPUT·<†A†, ††, W>, C2·A)

= ( WRITELN(‘2’) ◦ VAR …^T ◦ .)

({INPUT·<†AB†, C/, R>, OUTPUT·<†A†, ††, W>, C2·B)

= ( VAR …^T ◦ .) ({INPUT·<†AB†, C/, R>, OUTPUT·<†A2†, ††, W>, C2·B)

= . ({INPUT·<†AB†, C/, R>, OUTPUT·<†A2†, ††, W>)

= <†A2†>

Таким образом, PROGRAM Change2 END. (<†ABC†>) = <†A2†>

Простые процедуры.

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

PROGRAM SimpleProc (INPUT, OUTPUT);

PROCEDURE Demo;

BEGIN

WRITELN(‘Invoked’);

END;

BEGIN

Demo;

END.

Объявление процедуры добавляет пару <†Demo†, †BEGIN WRITELN(‘Invoked’) END†> к состоянию выполнения. Значение процедурного оператора будет:

Demo = BEGIN WRITELN(‘Invoked’) END

Формальное описание частного значения процедуры соответствует вышесказанному. Пусть N – идентификатор процедуры, тогда:

N = {s, s(N)(s)}