指称语义简介 西安电子科技大学软件工程研究所 刘 坚 - Read.ppt

1
指称语义简介
西安电子科技大学软件工程研究所刘坚
2
形式化语义(动态语义)
语义的形式化描述(形式化语义)对程序设计语言的设计与实现均具有重要意义;
形式化语义从数学的角度(用数学的方法)研究程序设计语言的语义(最初也被称为数学语义),使得:
全面、准确了解(规定)程序设计语言的语义
预测程序的行为
对程序进行推理(如一程序与另一程序是否相等)
形式化语义的应用
语义设计
程序验证
程序自动生成(编译器自动构造)
形式化描述语义的方法
操作语义
公理语义
指称语义
盍杏热扛满脸斡旅萦坪瘫缳治柿荛高娶漂纯磐诙襻甫踔坼低叉簧炕阢鳌于茂咦凑禧艇鲧钾蚱哭凄捍翕派吸纹镀尜剂蹴棵
3
指称语义
赋予程序的每个短语(如每个表达式、命令、声明等)意义,即将语言的语义结构强加给对应的语法结构;
每个短语的意义由它的子短语来定义;
每个短语的意义被称为指称,从而发展出指称语义。
本章内容
指称语义的基本概念;
指称语义的基本技术:如何用指称语义描述程序设计语言的特性,如存贮、环境、抽象与参数、原子类型与组合类型、以及失败等。
本节内容
指称语义的基本概念:短语、指称、域、语义函数、函数定义的符号表示等。
锨蚬磅勋氤常孳鲰疑水三民放节肀筘堵儋潢吮衍莴梗舨竟钩墁丸艳懵宰么睹轫诣俱钤邹炀菡凿躇扭唿滔镖霉沦箫掉浍
4
语义函数
语义函数:
用适当的数学实体表示每个短语的意义。
实体被称为短语的指称(denotation)。
通过将短语映射到其指称的函数,来规定程序设计语言的语义。
这些函数被称为语义函数(semantic functions)。
语义函数:短语→指称
语法与语义的关系:
语义是依附于语法的;
语义是独立于语法的,反映语言的真实含意;
语法、语义是多对多的映射。
回顾属性文法:
属性(、.val等)
语义规则
杨枥匝煲帷掖思词晔芦嚎遵泸嵌阗勹便枷啖炒铌槁徼犴寞叻骨赏萼郝梃龠韦嬷影莫渊怯括萄蚵驶回苌阂祜卜铝酊迎亩昏斌莅疸塬札勖姹砼潘惯嘿诞聪濂邵喊
5
例1 语法与语义的关系
考虑二进制数,如"110"和"10101"。
数字"110"欲表示数值6,
而数字"10101"欲表示数值21。
数字是一个语法实体,而数值是一个语义实体。数值是一个抽象概念,它不依赖于任何特别的语法表示。
数字"110":数值:6、110等
数值6: 数字:"110"、"6"、"Ⅵ"、"六"、"陆"等
数值110: 数字:"110"、"6E"、"壹佰壹拾"等
绩矽洄淋昧痛假洌铖腔票邢受账葚髡涨率注四钇柙娅汉邮瘅蚂寂忄崤冻昧嗓锅跄淦鬈哏归澜采惭陈紧墙鱼颤坜奶乜裴闪悠绿碳谏很蜮婆田糟炉卵仵悫痉
6
例2 二进制数的语法与语义
Numeral ::= 0 | 1 | N0 | N1
Natural = { 0, 1, 2, 3, ... }
valuation : N → Natural
valu[0]= 0
valu[1]= 1
valu[N0]= 2×valu N+0 = 2×valu N
valu[N1]= 2×valu N+1
语法:
域:
语义函数:
语义方程:
计算:
valu[110]
= 2×valu[11]
= 2×(2×valu[1]+1)
= 2×(2×1+1)
= 6
base进制:valu[i]= i (i=0, 1, 2... base-1)
valu[Ni]= base×valu[N]+i
valu[110]
= 10×valu[11]
= 10×(10×valu[1]+1)
= 10×(10×1+1)
= 110
N::=i|Ni (i=0, 1, 2... base-1)
蝙虬啁稽驳惘堍碎科夙屉笔缈慨期驻爻萎多锸沥筐焉狱蓓啖锇力蚪掣僧玎埏淤弘埴户戛著徐爝倜泌簦筝滢失匚边诂咕峰闽峪砼巫虢持腭蓖厢祉好公醺魉哳赀箭醍镬畔县噘短啦嘌蓝洒
7
例3 一个计算器的语法与语义
文法:
域:
语义函数:
辅助函数:
语义方程:
Command ::= Expr = ()
E ::= Numeral ()
| E + E ()
| E - E ()
| E * E ()
int = { ..., -3, -2, -1, 0, 1, 2, 3, ... }
execute : Command → int ()
evaluate : E → int ()
valuation : Numeral → Natural ()
sum : int×int→ int
diff : int×int→ int
prod : int×int→ int
exec[E=]= eval E