Денотационная семантика языка с окружениями.

47. Денотационная семантика языка с окружениями.
Абстрактный синтаксис языка с окружениями
Синтаксические категории:
P  э(принадлежит)  Program
B  э  Block
D  э  Declaration
T  э  Type
C  э  Command
E  э  Exp
Be  э  BExp
I   э  Id
x   э  Var
bx  э BVar
op  э  Op
bop  э  Bop
n   э  Num
Определения:
P ::= program I is B
B ::= D begin C end
D ::= ?  | D’; D” |const I = E | var I: T | var I,I+: T | procedure I is B | procedure I (I:T) is B
T ::= integer | boolean
C ::= skip | I := E | C’ ; C” | if Be then C’ else C” | read I | write E | while Be do C’ | declare B | I | I (E)
E ::= …
Be ::= …
Связь с памятью двухступенчатая: переменная связана с адресом, а адрес со значением.
Окружения:
DV = int(Integer) + bool(Boolean) + var(Location) + Procedure
Environment: Identifier -> DV+unbound
emptyEnv I = unbound – пустое окружение
extendEnv: Environment x Identifier x DV -> Environment – расширение окружения
extendEnv (env,I,dval) I1 =  if I=I1 then dval else env(I1)
applyEnv: Environment x Identifier ->  DV+unbound
applyEnv (env,I) = env(I)
Память:
Location = {0,1,2,3…} – область адресов
Store = Location -> (SV + unused + undefined)      SV – хранимое значение
emptySto loc = unused
updateSto: Store x Location x (SV + unused + undefined) -> Store
updateSto(sto,loc,val) loc1 =  if loc=loc1 then val else sto(loc1)
applySto: Store x Identifier -> (SV + unused + undefined)
applySto(sto,loc) = sto(loc)
allocate: Store -> Store x Location  выделяет ячейку памяти
allocate sto = updateSto(sto,loc,undefined),loc)
    where loc = minimum {k|sto(k)=unused}
deallocate: Store x Location -> Store
deallocate (sto,loc) = updateSto(sto,loc,unused)
Семантические области
Integer = {…, -2, -1, 0, 1, 2, …}
Boolean = {true, false}
EV = int (Integer) + bool (Boolean)
SV = int (Integer) + bool (Boolean)
DV = EV + var (Location) + Procedure
Location = Numeral = {0,1,2,3…}
Store = Location -> (SV + unused + undefined)
Environment: Identifier -> DV+unbound
unbound – переменная, для которой нет связи
Procedure = proc0(Store -> Store) + proc1(Location -> Store -> Store)
Семантические функции
Отличие в том, что добавляются переменные, хранящие окружение
meaning : Program -> Store
perform : Block -> Environment -> Store -> Store – формирует функцию, которая отображает память на память
elaborate : Declaration -> Environment -> Store -> Environment x Store  формирует новое окружение исходя из декларации блока, запускается при входе в блок
execute : Command -> Environment -> Store -> Store
evaluate : Expression -> Environment -> Store -> EV
value : Numeral -> EV
Формирование окружения
elaborate [?]env sto = (env, sto)
elaborate [D1 D2 ] env sto = elaborate [D2] env1 sto1
where (env1, sto1) = elaborate [D2] env sto
elaborate [const I = E] env sto =
   extendEnv (env, I, evaluate [E] env sto), sto)
elaborate [var I : T]env sto =
   extendEnv (env, I, var(loc), sto1)
           where (sto1, loc) = allocate sto
elaborate [var I,L : T] env sto = elaborate [var L : T] env1 sto1
  where (env1, sto1) = elaborate [var I : T] env sto
Семантические уравнения:
execute  [S1;S2] env = (execute [S2] env ) ? (execute [S1] env)
Процедуры:
elaborate [procedure I is B] env sto = (env1, sto)
  where
       env1 = extendEnv (env,I,proc0(proc))
       proc = perform [B] env1
Если рекурсия запрещена, то  proc = perform [B] env
execute [I] env sto = proc sto
  where proc0(proc) = applyEnv( env,I)
Процедуры с параметром:
elaborate [procedure I1(I2:T) is B]env sto = (env1, sto)
where
    env1 = extendEnv (env,I1,proc1(proc))
     proc loc = perform [B] extendEnv env1 ,I2, var(loc))
execute [I(E)] env sto =
                 proc loc updateSto(sto1,loc, evaluate [E] env sto)
where proc1(proc) = applyEnv( env,I)
           (sto1,loc) = allocate sto