形式语义-操作语义.ppt

《形式语义-操作语义.ppt》由会员上传分享，免费在线阅读，更多相关内容在PPT专区-天天文库。

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

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

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

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

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

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

7、态的某种观察。状态：Loc→N定义一个新状态程序变量x在该状态下的值就是v，而其他变量的值不变（未知或不关心）表达式的语义算术表达式的求值序偶表示状态下表达式a等待求值求值关系：状态下表达式a的求值结果为n表达式的语义算术表达式的求值求值规则积表达式的语义逻辑表达式的求值求值规则（1）表达式的语义逻辑表达式的求值求值规则（2）当t0为true且t1为true时t为true，否则为false当t0为true或t1为true时t为true，否则为false表达式的语义逻辑表达式的