6.1.5. Значение блоков.

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

BEGIN

END

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

BEGIN END = I

Когда блок содержит объявления, пары идентификатор-значение добавляются к исходному состоянию выполнения до того как выполнится оператор BEGIN, а после его выполнения удаляются из состояния выполнения. Например, если частным значением VAR … добавлены переменные, тогда нам необходимо VAR …^T чтобы удалить эти значения из состояния выполнения.

Простой блок

VAR

Ch: CHAR;

BEGIN

END

с частным значением:

VAR Ch: CHAR; BEGIN END = VAR Ch: CHAR ◦ BEGIN END ◦ VAR Ch: CHAR ^T

а именно, композицией, которая сначала добавляет Ch? к состоянию выполнения, потом выполняет эквивалентные преобразования, потом удаляет Ch и значение из состояния выполнения. Начинаясь с состояния выполнения:

{INPUT <††,  /R>, OUTPUT <††, ††W>}

композиция имеет следующее значение:

(VAR Ch: CHAR ◦ BEGIN END ◦ VAR Ch: CHAR ^T )

({INPUT <††,  /R>, OUTPUT <††, ††W>})

= (BEGIN END ◦ VAR Ch: CHAR ^T )

({INPUT <††,  /R>, OUTPUT <††, ††W>, Ch?})

= (VAR Ch: CHAR ^T ) ({INPUT <††,  /R>, OUTPUT <††, ††W>, Ch?})

= {INPUT <††,  /R>, OUTPUT <††, ††W>}

То есть как и ожидалось, VAR Ch: CHAR содержит все пары из

<s, s  {Chc}>, для любого символьного значения c

которое мы сокращенно записали добавив Ch? К состоянию выполнения.

BEGIN END не изменяет состояние выполнения, а VAR Ch: CHAR ^T удаляет пару сокращенно обозначенную как Ch?

Общий случай для частного значения блока следует аналогичен вышеописанному. Когда объявления отсутствуют, значение блока – это просто значение выражения BEGIN. Когда присутствуют объявления процедур или переменных F, за которыми следует оператор BEGIN B, значение блока будет

F; B = F ◦ B ◦ F ^T

Блок с объявлением одной переменно и одной процедуры может быть проанализирован примерно следующим образом:

VAR … ; PROCEDURE … ; BEGIN … END

= VAR … ; ◦ PROCEDURE … ; BEGIN … END ◦ VAR … ; ^T

= VAR … ; ◦ PROCEDURE … ; ◦ BEGIN … END ◦ VAR … ; ^T

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

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

PROGRAM CopyChar (INPUT, OUTPUT);

VAR

Ch: CHAR;

BEGIN

READ(Ch);

WRITELN(Ch)

END.

Значение программы Q может быть вычислено для 1-списка <†ABC†>

Q (<†ABC†>) = PROGRAM … END. (<†ABC†>)

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

= VAR … END ◦ . ({INPUT <††, ABC/R>, OUTPUT <††, ††W>}) (2)

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

({INPUT <††, ABC/R>, OUTPUT <††, ††W>}) (3)

= BEGIN … END ◦ VAR … ^T ◦ .

({INPUT <††, ABC/R>, OUTPUT <††, ††W>, Ch?}) (4)

= VAR … ^T ◦ .({INPUT <†A†, BC/R>, OUTPUT <†A/†, ††W>, ChA}) (5)

= .({INPUT <†A†, BC/R>, OUTPUT <†A/†, ††W> }) (6)

= <†A†>

Шаг (1) детализирует значение программы Q через композицию заголовка блока и точки. Шаг (2) применяет композицию оставшихся компонентов к значению заголовка. Шаг (3) расширяет значение блока до композиции объявлений, оператора BEGIN и транспозиции объявления. Шаг (4) применяет композицию оставшихся компонентов к значению программы после выполнения деклараций. Шаг (5) применяет композицию оставшихся компонентов к значению программы после выполнения оператора BEGIN. Шаг (6) показывает значение программы после применения к предыдущему значению транспозиции объявлений. Шаг (7) фиксирует значение программы после выполнения финальной точки.

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

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