Объявление элемента
Пусть х - любой идентификатор, s - тип, а Е - выражение этого типа; тогда s х: Е называется объявлением элемента или согласованием элемента с идентификатором х. Через объявление элемента идентификатор х связывается со значением выражения Е. С помощью такого объявления принимается соглашение о том, что с этого момента х стоит в качестве этого значения.
Область связанности, порождаемая объявлением ограничивается блоком, в начале которого и помещаются объявления. Пусть G -объявление, а ЕО - выражение. Тогда
[О; EO]
есть блок. Угловые скобки называют скобками блока. Они ограничивают область действия объявления G,
т.е. область связанности идентификатора, порождаемую объявлением G. Это значит, соглашение о том, что объявленный в G идентификатор стоит в качестве соответствующего значения, действительно только внутри скобок блока.
Синтаксис объявления элемента описывается следующим БНФ-правилом:
<объявление_элемента>:: =<тип><идентификатор>=<выражение>
Пусть для объявления элемента справедливы следующие дополнительные условия:
·
тип выражения Е есть s;
· х не входит свободно в Е.
Второе условие указывает на то, что в модельном языке не допускаются рекурсивные объявления элементов.
Пример (объявление элемента). С помощью объявления
nat х = 3 + 4
принимается соглашение о том, что х имеет значение 7. Это объявление может использоваться в каком-либо блоке. Блок
[nat x =3+4;x*x]
имеет тогда значение 49. Внутри блока х стоит в качестве значения 7.
В ЯП вместо угловых скобок часто записываются также begin и end. Тогда блок будет записываться в виде
begin s х = El; E2 end
Скобки блока begin (соответствующая [) и end (соответствующая ]) ограничивают область действия описания для идентификатора х. Внутри этой области могут приниматься другие, вложенные соглашения, и тогда исходное соглашение на время теряет свою силу (становится "невидимым"). Так, значение блока
[nat х= 1; [nat х =2; х ] + х ] идентично блоку
[nаt х = 1; [nat у = 2; у ] + х ].
Систематическое переименование идентификаторов в локальных объявлениях в блоке (аналог
-редукции) не меняет значения блока.
В программном выражении какой- либо идентификатор может объявляться повторно - тем самым принимаются различные соглашения относительно его связывания, и тогда один и тот же идентификатор в разных местах выражения будет иметь различные значения. Впрочем, все эти области связанности должны быть вложенными. Поэтому при наличии объявлений необходимо делать различие между областью действия объявления и длительностью жизни связывания идентификатора. В разделе
[s x=- El; E2]
соглашение о связывании идентификатора х со значением Е1 имеет силу во всей области, находящейся между угловыми скобками, в частности и в E2, причем действие этого соглашения прерывается с помощью соглашений, принимаемых (через соответствующие объявления) в E2. Это проясняет различие между длительностью жизни и областью видимости связывания. Длительность жизни, т.е. область связанности, охватывает всю область между угловыми скобками (т.е., в частности, и полностью E2). А область видимости соответствует длительности жизни за вычетом внутренних блоков с новыми связываниями для х.
С помощью объявления элемента устанавливаются конкретизации для соответствующего идентификатора. Область действия такой конкретизации ограничивается угловыми скобками. Внутри угловых скобок х стоит в качестве значения выражения Е1. Семантически это означает, что E2 интерпретируется с соответствующим изменением конкретизации для х. Значение I[G] объявления G можно понимать как "точечное" (локальное) изменение подстановки и тем самым как отображение между конкретизациями.
Caмo объявление не обладает никаким простым элементом данных в качестве значения, поэтому оно не вычисляется непосредственно с помощью правил подстановки термов. В дальнейшем будет даваться исключительно правило для вычисления значения выражения, в котором встречается объявление.
Все сказанное относительно связывания, видимости, длительности жизни и свободности или связанности идентификаторов для абстракции функций справедливо и для объявлений.
Содержание раздела