形式语义-操作语义

1、程序设计语言的形式语义,The Formal Semantics of Programming Languages,操作语义,操作语义（operational semantics）通过描述程序语法构造在机器上的运行效果而定义程序的语义。 以抽象机器为语义解释对象 操作语义关注程序的运行效果是怎样得到的 HOW,操作语义,操作语义概述(1) 1960s，对编译程序所产生的目标程序标准化、形式化的愿望；自动机理论研究的兴旺时期 抽象机。抽象机是操作语义的核心，既是具体机器的抽象化，又是自动机的高级化向着直接反映高级语言语义的方向靠近。 MaCarthy，比较明确的提出用抽象机表达操作语义，并用它描

2、述了ALGOL60的一个子集的语义。 1964年Landin，SECD（Stack,Environment,Control, Dump）;扩充为SM（共享机），描述了ALGOL60完整语义。 1968年，Knuth提出属性文法。,操作语义,操作语义概述(2) 传统的操作语义的顶峰是VDL（维也纳定义语言），IBM的维也纳实验室，形式化定义PL/1语言 与此同时，英国赫斯利实验室对PL/1语言 的形式化被ANSI接受为标准（形式化程度较低，规范的自然语言描述） 操作语义的另一个变种是变换语义。用分而治之的思想降低复杂度（抽象复杂度+翻译复杂度）。德国CIP小组提出的广谱语言。M5，M4，M3，M

3、2，M1 1981，Plotkin提出结构化的操作语义。把公理化方法引入操作语义中，基本思想是：复合成分的操作语义可以归结为其各个组成部分的操作语义。,IMP一种简单的命令式语言,IMP语言的语法范畴： N，数集，包括正整数、负整数和零 带符号位的正负十进制数的集合 T，真值集，T=true, false Loc，存储单元集 字母开头的字母数字串 Aexp，算术表达式集 Bexp，逻辑表达式集 Com，命令集,IMP一种简单的命令式语言,语法成分的元变量（约定）： n，m表示数集N中的元素 x，y 表示存储单元集Loc中的元素 a 表示算术表达式集Aexp中的元素 b 表示逻辑表达式集Bexp

4、中的元素 c 表示命令集Com中的元素 可以加上标或下标,IMP一种简单的命令式语言,算术表达式的抽象语法,IMP一种简单的命令式语言,逻辑表达式的抽象语法,IMP一种简单的命令式语言,命令的抽象语法,四种语句 空语句 赋值语句 分支语句 循环语句 程序命令、程序语句、程序,IMP一种简单的命令式语言,定义2.1： IMP语言的算术表达式、逻辑表达式及命令的抽象语法,IMP一种简单的命令式语言,IMP语言语法扩展：,为了讲课方便扩充了一些运算，非本质的。,IMP一种简单的命令式语言,例2.1 交换程序及其语法树：,IMP一种简单的命令式语言,例2.2 阶乘程序：,变迁系统,操作语义通过描述程序

5、在抽象机器上的运行过程来描述程序的语义。 运行过程用程序状态和当前要执行的命令的变换序列给出。,格局（configuration）,程序的运行过程就是格局的变换序列,变迁系统,状态： 直观模型：存储单元的内容决定了当前的状态 状态集合， ：LocN (x)是状态下存储单元x 的值或内容,程序中所出现的变量,变迁系统,格局： 程序状态是一个特殊的格局 变迁系统（Transition System）（转换系统） 变迁系统是二元组（X, R）,在状态下将要执行c,语句为空，省略尖括号,变迁系统的状态集， 其元素称为状态或格局,RXX 状态之间的变迁关系,变迁系统,可以将IMP程序理解为运行在一个变迁

6、系统上 运行过程是程序状态和下一步要执行的程序语句的变化 变迁关系(c1,1) (c2, 2)：程序（命令）c1在状态1运行后得到状态2且下一步要执行的程序是c2 。 (c1,1) 2：程序（命令）c1在状态1运行后得到状态2且没有后续语句要执行（程序结束） 。,变迁系统,小结：描述IMP语言的操作语义： 格局 程序（命令）c在状态下运行 程序终止的状态 变迁关系 定义IMP语言的操作语义就是定义适当格局之间的变迁关系 通过定义IMP语言的每个命令所引起的变迁来完成,表达式的语义,表达式是IMP语言的最基本的语法成分，包括算术表达式和逻辑表达式 程序执行是对程序状态的变换；而表达式的计算并不改

7、变程序状态，可以看作是对程序状态的某种观察。 状态 ：LocN 定义一个新状态,程序变量x在该状态下的值就是v，而其他变量的值不变（未知或不关心）,表达式的语义,算术表达式的求值,序偶表示状态下表达式a等待求值 求值关系：,状态下表达式a的求值结果为n,表达式的语义,算术表达式的求值,求值规则,积,表达式的语义,逻辑表达式的求值,求值规则（1）,表达式的语义,逻辑表达式的求值,求值规则（2）,表达式的语义,表达式的语义,逻辑表达式的求值,最左顺序计算（短路）,表达式的语义,说明：,规则一般包括前提和结论，后面的条件称为附加条件。 有些规则没有前提部分，前提为空的规则称为公理。（有时在上面加一条

8、实线） 由前提推出结论称为规则的一个应用。 用特定的数、存储单元、表达式以及状态来替代规则的元变量，就得到一个规则实例。 求值过程推导树。,表达式的语义,状态0下表达式(Init+5)+(7+9)的求值， 0(Init)=0,推导树由规则的实例构成，每个实例的前提正好是上一层实例的结论； 公理位于最顶层，公理的上方没有前提部分； 最底层的实例的结论称为整个推导的结论。 如果某个推导存在结论，称该结论是从规则可精确推导的。 匹配的规则可能有多条，必须考虑所有左部与格局匹配的规则；对于符合条件的所有推导必须并行地构造。,表达式的语义,状态下布尔表达式(x*y)z) +(z+x=0)的求值， (x)

9、=3， (y)=5， (z)=7,表达式的语义,算术表达式的等价 逻辑表达式的等价,命令的语义（自然语义）,操作语义定义适当格局之间的变迁关系 程序（命令）通过执行来改变状态,表示在状态下执行完命令c终止于终态。 例如：,命令的语义（自然语义）,命令的规则（1）,原子命令,实例： 初始状态下所有存储单元的值均为0,命令的语义（自然语义）,命令的规则（2）,顺序命令,实例：,命令的语义（自然语义）,命令的规则（3）,条件命令,命令的语义（自然语义）,命令的规则（3）,条件命令实例：,命令的语义（自然语义）,命令的规则（4）,循环命令,命令的语义（自然语义）,命令的规则（4）,循环命令实例,循环体

10、每执行一步的变迁关系,命令的语义（自然语义）,死循环,这种推导是无穷的，因此，实际上不存在状态使得：,语义无定义,命令的语义（自然语义）,命令的规则小结,命令的语义（自然语义）,推导树 例1：交换程序,命令的语义（自然语义）,例2：阶乘程序 0(x)=3， 0(y)=0,命令的语义（自然语义）,小结：自然语义 可以看作如下形式的函数： 对任意的命令c，自然语义函数是从状态集到的部分函数 有定义 无定义 至多存在一个终止状态,等价关系及证明,命令的等价（语义等价）,例：,等价关系及证明,命题2.8（P16）,证明：,对所有的状态，有：,两方面： “” “”,等价关系及证明,（1）“”,等价关系及

11、证明,等价关系及证明,等价关系及证明,（2）“”,等价关系及证明,由于：,所以：,等价关系及证明,自然语义小结,自然语义 至多存在一个终止状态 语义等价关系,自然语义小结,自然语义小结,练习：整除程序的推导树：,自然语义小结,练习：整除程序的推导树：,信息工程学院计算机系,另一种语义（结构化操作语义）,与自然语义比较 自然语义所给出的变迁关系是一步到位的,另一种语义（结构化操作语义） 描述程序执行中每一小步的中间状态,另一种语义（结构化操作语义）,原子命令的结构化操作语义,另一种语义（结构化操作语义）,顺序命令的结构化操作语义,另一种语义（结构化操作语义）,条件命令的结构化操作语义,另一种语义（结构化操作语义）,循环命令的结构化操作语义,另一种语义（结构化操作语义）,规则：,另一种语义（结构化操作语义）,例1：交换程序,推导序列,另一种语义（结构化操作语义）,推导序列,另一种语义（结构化操作语义）,另一种语义（结构化操作语义）,例2：阶乘程序,另一种语义（结构化操作语义）,例2：阶乘程序,另一种语义（结构化操作语义）,例2：阶乘程序,另一种语义（结构化操作语义）,例2：阶乘程序,另一种语义（结构化操作语义）,例2：阶乘程序,另一种语