形式语义-操作语义

程序设计语言的形式语义TheFormalSemanticsofProgrammingLanguages操作语义操作语义（operationalsemantics）通过描述程序语法构造在机器上的运行效果而定义程序的语义。−以抽象机器为语义解释对象−操作语义关注程序的运行效果是怎样得到的−HOW操作语义操作语义概述(1)1960s’，对编译程序所产生的目标程序标准化、形式化的愿望；自动机理论研究的兴旺时期抽象机。抽象机是操作语义的核心，既是具体机器的抽象化，又是自动机的高级化——向着直接反映高级语言语义的方向靠近。MaCarthy，比较明确的提出用抽象机表达操作语义，并用它描述了ALGOL60的一个子集的语义。1964年Landin，SECD（Stack,Environment,Control,Dump）;扩充为SM（共享机），描述了ALGOL60完整语义。1968年，Knuth提出属性文法。操作语义操作语义概述(2)传统的操作语义的顶峰是VDL（维也纳定义语言），IBM的维也纳实验室，形式化定义PL/1语言与此同时，英国赫斯利实验室对PL/1语言的形式化被ANSI接受为标准（形式化程度较低，规范的自然语言描述）操作语义的另一个变种是变换语义。用分而治之的思想降低复杂度（抽象复杂度+翻译复杂度）。德国CIP小组提出的广谱语言。M5，M4，M3，M2，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中的元素c表示命令集Com中的元素−可以加上标或下标IMP——一种简单的命令式语言算术表达式的抽象语法010101Aexp:::||||anxaaaaaaIMP——一种简单的命令式语言逻辑表达式的抽象语法01010101Bexp:::||||||baaaabbbbbtruefalseIMP——一种简单的命令式语言命令的抽象语法0101Com:::|:|;||cxaccbccbcskipifthenelsewhiledo四种语句−空语句−赋值语句−分支语句−循环语句程序命令、程序语句、程序IMP——一种简单的命令式语言定义2.1：IMP语言的算术表达式、逻辑表达式及命令的抽象语法010101010101010101Aexp:::||||Bexp:::||||||Com:::|:|;||anxaaaaaabaaaabbbbbcxaccbccbctruefalseskipifthenelsewhiledoIMP——一种简单的命令式语言IMP语言语法扩展：为了讲课方便扩充了一些运算，非本质的。IMP——一种简单的命令式语言例2.1交换程序及其语法树：IMP——一种简单的命令式语言例2.2阶乘程序：变迁系统操作语义通过描述程序在抽象机器上的运行过程来描述程序的语义。运行过程用程序状态和当前要执行的命令的变换序列给出。格局（configuration）程序的运行过程就是格局的变换序列变迁系统状态：直观模型：存储单元的内容决定了当前的状态状态集合∑，∈∑：Loc→N(x)是状态下存储单元x的值或内容程序中所出现的变量0[5,7,0]xyz:;:;:zxxyyz0[5/,7/,0/]xyz变迁系统格局：c,程序状态是一个特殊的格局变迁系统（TransitionSystem）（转换系统）变迁系统是二元组（X,R）在状态下将要执行c语句为空，省略尖括号变迁系统的状态集，其元素称为状态或格局RX×X状态之间的变迁关系变迁系统可以将IMP程序理解为运行在一个变迁系统上运行过程是程序状态和下一步要执行的程序语句的变化变迁关系(c1,1)→(c2,2)：程序（命令）c1在状态1运行后得到状态2且下一步要执行的程序是c2。(c1,1)→2：程序（命令）c1在状态1运行后得到状态2且没有后续语句要执行（程序结束）。变迁系统小结：描述IMP语言的操作语义：格局•c,程序（命令）c在状态下运行•程序终止的状态变迁关系•定义IMP语言的操作语义就是定义适当格局之间的变迁关系•通过定义IMP语言的每个命令所引起的变迁来完成表达式的语义表达式是IMP语言的最基本的语法成分，包括算术表达式和逻辑表达式程序执行是对程序状态的变换；而表达式的计算并不改变程序状态，可以看作是对程序状态的某种观察。状态：Loc→N定义一个新状态[]xv([/])()()vyxvxyyyx程序变量x在该状态下的值就是v，而其他变量的值不变（未知或不关心）[/]vx表达式的语义算术表达式的求值010101Aexp:::||||anxaaaaaa序偶a,表示状态下表达式a等待求值求值关系：:,anA状态下表达式a的求值结果为n表达式的语义算术表达式的求值求值规则001101010011010100110101,,(),,nnn,,,nnn,,,nnn,nnxxananaanananaanananaan其中是与的和其中是与的差其中是与的积表达式的语义逻辑表达式的求值求值规则（1）00110101001101010011010100110101,,,,,,,,,(,,,,,truetruefalsefalseanannnaatrueanannnaafalseanannnaatrueanannnaafalse如果等于如果不等于如果小于等于如果大于表达式的语义逻辑表达式的求值求值规则（2）001101001101,,,,,,,,,,btruebfalsebfalsebtruebtbtbbtbtbtbbt当t0为true且t1为true时t为true，否则为false当t0为true或t1为true时t为true，否则为false表达式的语义逻辑表达式的求值规则00110101001101010011010100110101,,,,,,,,,(,,,,,,truetruefalsefalseanannnaatrueanannnaafalseanannnaatrueanannnaafalsebt如果等于如果不等于如果小于等于如果大于001101001101,,,,,,,,,ruebfalsebfalsebtruebtbtbbtbtbtbbt当t0为true且t1为true时t为true，否则为false当t0为true或t1为true时t为true，否则为false表达式的语义逻辑表达式的求值最左顺序计算（短路）00101010101,,,,,,,,bfalsebbfalsebtruebfalsebbfalsebtruebtruebbtrue表达式的语义说明：规则一般包括前提和结论，后面的条件称为附加条件。有些规则没有前提部分，前提为空的规则称为公理。（有时在上面加一条实线）由前提推出结论称为规则的一个应用。用特定的数、存储单元、表达式以及状态来替代规则的元变量，就得到一个规则实例。求值过程——推导树。表达式的语义状态0下表达式(Init+5)+(7+9)的求值，0(Init)=00000000,05,57,79,9(5),5(79),16(5)(79),21InitInitInit0,0Init00,05,5Init000,05,5(5),5InitInit000000,05,57,79,9(5),5(79),16InitInit推导树由规则的实例构成，每个实例的前提正好是上一层实例的结论；公理位于最顶层，公理的上方没有前提部分；最底层的实例的结论称为整个推导的结论。如果某个推导存在结论，称该结论是从规则可精确推导的。匹配的规则可能有多条，必须考虑所有左部与格局匹配的规则；对于符合条件的所有推导必须并行地构造。表达式的语义状态下布尔表达式((x*y)z)∧+(z+x=0)的求值，(x)=3，(y)=5，(z)=7,3,5,7,3,70,0(),15(),10(),()0,()()0,xyzxzxyzxxyzfalsezxfalsexyzzxfalse==表达式的语义算术表达式的等价逻辑表达式的等价0101(.,,)aaiffnNanan0101(.,,)bbifftbtbt命令的语义（自然语义）操作语义定义适当格局之间的变迁关系程序（命令）通过执行来改变状态,'c表示在状态下执行完命令c终止于终态’。例如：:5,'x:5,[5/]xx命令的语义（自然语义）命令的规则（1）,,:,[/]skipamxamx原子命令实例：初始状态下所有存储单元的值均为000:1,[1/]xxx命令的语义（自然语义）命令的规则（2）0101,'',''';,'cccc顺序命令实例：000000:1,[1/]:1,[1/][1/][2/]:1;:1,[1/][2/]xxxyxxxyxxyxxy命令的语义（自然语义）命令的规则（3）001,,','btruecifbthencelsec条件命令101,,','bfalsecifbthencelsec命令的语义（自然语义）命令的规则（3）条件命令实例：000000,,(0):1,xtrueskipifxthenskipelsexx0()0x111110,:1,[2/](0):1,[2/]xfalsexxxifxthenskipelsexxx1()1x命令的语义（自然语义）命令的规则（4）,,,,'',''','falsewhiledotruewhiledowhiledobbcbcbcbc循环命令命令的语义（自然语义）命令的规则（4）000(1),[1/](1):1,[1/][1/]falsewhixxxxxxxledo循环命令实例0000000(1),:1,[1/](1)