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

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

= I = {<s, s>}

6.2.3. Оператор 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, …}

6.2.4. Оператор 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†>