Значение объявлений.

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

Декларация изменяет состояние выполнения, добавляя к нему один или несколько идентификаторов. До выполнения декларации идентификаторы не существуют, после декларации они могут иметь значения. Частное значение декларации изменяет область определения состояния выполнения, добавляя идентификатор. Будет удобно отдельно разделять декларации для типов CHAR, TEXT и PROCEDURE.

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

Для переменной N типа CHAR определим:

VAR N: CHAR = {<s, t>: t = s È {<N, x>} для любого символьного значения x}

Строка N соответствует синтаксису <идентификатора> и строка VAR N: CHAR формально должна быть представлена как:

V = †VAR† & N & †CHAR†

При использовании символа ? для обозначения значения N:

VAR N: CHAR = {<s, t>: t = s È {<N, ?>} }

не так очевидно, что любые символьные значения образуют пары с N. Например, пусть s будет аргументом VAR N: CHAR, тогда s будет:

s È {Ch·A},

s È {Ch·B},

…

для всех возможных символьных значений.

Хотя VAR N: CHAR не является функцией, VAR N: CHAR^T является функцией, потому что ее пары имеют вид:

<s È {N·A}, s>

<s È {N·B}, s>

…

и каждому аргументу соответствует уникальное значение.

Значение декларации файловых переменных аналогично. Пусть N – идентификатор, определим:

VAR N: TEXT = {<s, t>: t = s È {N·<x, y, z>} для некоторых строк x, y и некоторого z Î {R,W}}

Сокращенная форма записи присоединяет 3-список <?,?,?> к вновь созданному идентификатору.

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

Это может быть выражено композицией:

VAR Сh1, Ch2: CHAR = VAR Сh1: CHAR ◦ VAR Ch2: CHAR

= {<s, t>: t = s È {Ch1·?} È {Ch2·?}}

которая включает пары, такие как

<s, s È {Ch1·C} È {Ch2·F}>

и все остальные комбинации двух символьных значений.

Предположим, что

x = {INPUT ·<††, †† , R>, OUTPUT ·<††, ††, W>}

является аргументом отношения VAR Сh: CHAR, тогда x образует пары в отношении для

{INPUT ·<††, †† , R>, OUTPUT ·<††, ††, W>} È {Ch·с}

для всех символьных значений c. Представим это в виде формулы:

VAR Сh: CHAR ({INPUT ·<††, †† , R>, OUTPUT ·<††, ††, W>})

= { INPUT ·<††, †† , R>, OUTPUT ·<††, ††, W>, Ch·?}

Объявление процедур, насколько нам в данный момент известно, не изменяет количество в столбцов в таблице выполнения. Когда позднее идентификатор процедуры используется в в процедурном выражении, вызывается <тело> процедуры. Задача объявления процедуры - записать информацию, которая сделает возможными действия описанные в процедуре. Этот текст присоединяется к идентификатору процедуры подобно значению из таблицы выполнения для переменной.

Для идентификатора процедуры N и тела T, определим:

PROCEDURE N; T = {<s, t>: t = s È {<N, T>}}

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

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

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

Блок может содержать ноль или больше объявлений переменных и процедур, но он должен завершаться оператором 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) фиксирует значение программы после выполнения финальной точки.

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