Деннотационная семантика языка While. | MetodPro.ru

Реклама на сайте

Деннотационная семантика языка While.


45) Денотационная семантика языка While.

Семантические области
• Integer = {…, -2, -1, 0, 1, 2, …}
• Boolean = {true, false}
• Store = Identifier -> (SV + undefined)
• SV = int (Integer) + bool (Boolean)
• EV = int (Integer) + bool (Boolean)

Семантические функции
• evaluate : Expression -> Store -> EV
• execute : Command -> Store -> Store
• meaning : Program -> Store

Вспомогательные функции
• Арифметические операции: plus, minus, times, div, lesseq, greater, equal …
Пример
equal : Integer -> Integer -> Boolean
• Операции с памятью:
emptySto::Store
emptySto i = undefined
updateSto::Store->Identifier->SV->Store
updateSto sto i val = i1 -> if i=i1 then val else sto i1
applySto::Store->Identifier->(SV+undefined)
applaySto sto i = sto i

Семантические уравнения для языка While
meaning [[C]]= execute [[C]]emptyStore
execute [[S1;S2]]= execute[[S2]]? execute[[S1]]
execute [[skip]]s = s или
execute [[skip]]= id
execute [[x:=a]]s = updateSto s x (evaluate[[a]])
execute [[ if b then S1 else S2]]s =
if bv then execute [[S1]]s
else execute [[S2]] s
where bool(bv) = evaluate[[b]]s

С командой while дело обстоит сложнее.
Определение
execute [[ while b do S]]s =
if bv then
(execute [[ while b do S ]]  ? execute [[S2]]) s
else id
where bool(bv) = evaluate[[b]]s
- не композиционно.

Представим смысл команды while рекурсивной функцией:
execute [[ while b do S]] = loop
  where loop sto = if bv
then loop execute [[ S ]]sto)
else sto
where bool(bv) = evaluate[[b]]s

Семантические уравнения для выражений
evaluate[[x]]sto = if val == undefined then error else val
where
val = applyStore  sto x
evaluate[[n]]sto = int (value[[n]])
evaluate[[true]]sto = bool (true)
evaluate[[false]]sto = bool (false)
evaluate[[e1+e2]]sto = int (plus m n)
where            int (m) = evaluate[[e1]]sto
        int (n) = evaluate[[e2]]sto
evaluate[[e1/e2]]sto = if n == 0 then error else int (div m n)
where            int (m) = evaluate[[e1]]sto
        int (n) = evaluate[[e2]]sto

evaluate[[e1 < e2]]sto = if less m n then bool (true)
else bool (false)
where
int (m) = evaluate[[e1]]sto
        int (n) = evaluate[[e2]]sto
evaluate[[e1 and e2]]sto = if p then bool (q)
else bool (false)
where
        bool(p) = evaluate[[e1]]sto
        bool(q) = evaluate[[e2]]sto
evaluate[[- e]]sto = int (minus 0 m)
         where
        int (m) = evaluate[[e]]sto
evaluate[[not e]]sto = if p then bool (false)
         else bool (true)
         where                bool(p) = evaluate[[e]]sto

Семантическая эквивалентность
Для любой команды S,  S ? S;skip.
execute [[S;skip]]s =
(execute[[skip]]? execute[[S]]) s =
execute[[skip]](execute[[S]] s) =
(execute[[S]] s)



Методические пособия

  • Системы автоматизированного проектирования
  • Социология молодёжи
  • Общая социология
  • Криптография
  • Проектирование трансляторов
  • Компьютерная графика
  • Моделирование систем
  • Информационная безопасность
  • Теория вычислительных процессов
  • Логические основы искусственного интелекта
  • Проектирование распределённых информационных систем