形式语义-操作语义

1、程序设计语言的形式语义The Formal Semantics of Programming Languages操作语义操作语义 操作语义操作语义（operational semantics）通过描述程序语法通过描述程序语法构造在机器上的运行效果而定义程序的语义。构造在机器上的运行效果而定义程序的语义。以抽象机器为语义解释对象以抽象机器为语义解释对象操作语义关注程序的运行效果是怎样得到的操作语义关注程序的运行效果是怎样得到的HOW操作语义操作语义v 操作语义概述操作语义概述(1) 19601960ss，对编译程序所产生的目标程序标准化、形式化的对编译程序所产生的目标程序标准化、形式化的愿望；自

2、动机理论研究的兴旺时期愿望；自动机理论研究的兴旺时期 抽象机。抽象机是操作语义的核心，既是具体机器的抽象抽象机。抽象机是操作语义的核心，既是具体机器的抽象化，又是自动机的高级化化，又是自动机的高级化向着直接反映高级语言语义向着直接反映高级语言语义的方向靠近。的方向靠近。 MaCarthyMaCarthy，比较明确的提出用抽象机表达操作语义，并用比较明确的提出用抽象机表达操作语义，并用它描述了它描述了ALGOL60ALGOL60的一个子集的语义。的一个子集的语义。 19641964年年LandinLandin，SECDSECD（Stack,Environment,Control, DumpSta

3、ck,Environment,Control, Dump）; ;扩充为扩充为SMSM（共享机），描述了共享机），描述了ALGOL60ALGOL60完整语义。完整语义。 19681968年，年，KnuthKnuth提出属性文法。提出属性文法。操作语义操作语义v 操作语义概述操作语义概述(2) 传统的操作语义的顶峰是传统的操作语义的顶峰是VDLVDL（维也纳定义语言），维也纳定义语言），IBMIBM的维也纳实验室，形式化定义的维也纳实验室，形式化定义PL/1PL/1语言语言 与此同时，英国赫斯利实验室对与此同时，英国赫斯利实验室对PL/1PL/1语言语言 的形式化被的形式化被ANSIANSI接受为

4、标准（形式化程度较低，规范的自然语言描述）接受为标准（形式化程度较低，规范的自然语言描述） 操作语义的另一个变种是变换语义。用分而治之的思想降操作语义的另一个变种是变换语义。用分而治之的思想降低复杂度（抽象复杂度低复杂度（抽象复杂度+ +翻译复杂度）。德国翻译复杂度）。德国CIPCIP小组提出小组提出的广谱语言。的广谱语言。M5M5，M4M4，M3M3，M2M2，M1M1 19811981，PlotkinPlotkin提出结构化的操作语义。把公理化方法引入提出结构化的操作语义。把公理化方法引入操作语义中，基本思想是：复合成分的操作语义可以归结操作语义中，基本思想是：复合成分的操作语义可以归结为

5、其各个组成部分的操作语义。为其各个组成部分的操作语义。IMP一种简单的命令式语言一种简单的命令式语言vIMP语言的语法范畴： N，数集，包括正整数、负整数和零带符号位的正负十进制数的集合带符号位的正负十进制数的集合 T，真值集，T=true, false Loc，存储单元集字母开头的字母数字串字母开头的字母数字串 Aexp，算术表达式集 Bexp，逻辑表达式集 Com，命令集IMP一种简单的命令式语言一种简单的命令式语言v语法成分的元变量（约定）： n，m表示数集表示数集N中的元素中的元素 x，y 表示存储单元集表示存储单元集Loc中的元素中的元素 a 表示算术表达式集表示算术表达式集Aexp

6、中的元素中的元素 b 表示逻辑表达式集表示逻辑表达式集Bexp中的元素中的元素 c 表示命令集表示命令集Com中的元素中的元素可以加上标或下标可以加上标或下标IMP一种简单的命令式语言一种简单的命令式语言v 算术表达式的抽象语法算术表达式的抽象语法010101A exp : : :| |anx aaaaaaIMP一种简单的命令式语言一种简单的命令式语言v 逻辑表达式的抽象语法逻辑表达式的抽象语法01010101B exp : : :|baaaab bbbbtruefal setruefal seIMP一种简单的命令式语言一种简单的命令式语言v 命令的抽象语法命令的抽象语法 0101C om :

7、 : :| :| ;| | cxa c cbccbcs sk ki ip pi if ft th he en ne el l s se ew w h hi il l e ed do o 四种语句四种语句空语句空语句赋值语句赋值语句分支语句分支语句循环语句循环语句 程序命令、程序语句、程序程序命令、程序语句、程序IMP一种简单的命令式语言一种简单的命令式语言定义定义2.1：IMP语言的算术表达式、逻辑表达式及命令的抽象语法语言的算术表达式、逻辑表达式及命令的抽象语法010101010101010101A exp : :|B exp : :|C om : :|:|;| | anxaaaaaabaa

8、aabbbbbcxaccbccbc t tr ru u e ef fa al ls se es sk ki ip pi if ft th he en ne el ls se ew w h hi il le ed do oIMP一种简单的命令式语言一种简单的命令式语言IMP语言语法扩展：语言语法扩展：为了讲课方便扩充了一些运算，非本质的。为了讲课方便扩充了一些运算，非本质的。IMP一种简单的命令式语言一种简单的命令式语言例2.1 交换程序及其语法树：IMP一种简单的命令式语言一种简单的命令式语言例2.2 阶乘程序：变迁系统变迁系统v操作语义通过描述程序在抽象机器上的运行过程操作语义通过描述程序在

9、抽象机器上的运行过程来描述程序的语义。来描述程序的语义。v运行过程用运行过程用程序状态和当前要执行的命令程序状态和当前要执行的命令的变换的变换序列给出。序列给出。 格局（configuration）程序的运行过程就是格局的变换序列变迁系统变迁系统v状态：状态： 直观模型：存储单元的内容决定了当前的状态直观模型：存储单元的内容决定了当前的状态 状态集合状态集合， ：LocN (x)是状态是状态 下存储单元下存储单元x 的值或内容的值或内容程序中所出现的变量05,7,0 xyz:; :;:zx xy yz05/ ,7/ ,0/ xyz变迁系统变迁系统v格局：格局： 程序状态程序状态 是一个是一个特

10、殊的格局特殊的格局v变迁系统（变迁系统（Transition System）（转换系统）（转换系统） 变迁系统是二元组（变迁系统是二元组（X, R）在状态 下将要执行c语句为空，省略尖括号变迁系统的状态集，变迁系统的状态集，其元素称为状态或格局其元素称为状态或格局R XX状态之间的变迁关系状态之间的变迁关系变迁系统变迁系统v可以将可以将IMPIMP程序理解为运行在一个程序理解为运行在一个变迁系统变迁系统上上 运行过程是程序状态和下一步要执行的程序语运行过程是程序状态和下一步要执行的程序语句的变化句的变化 变迁关系变迁关系(c (c1 1, , 1 1) (c) (c2 2, , 2 2) )：

11、程序（命令）：程序（命令）c c1 1在状在状态态 1 1运行后得到状态运行后得到状态 2 2且下一步要执行的程序且下一步要执行的程序是是c c2 2 。 (c (c1 1, , 1 1) ) 2 2：程序（命令）：程序（命令）c c1 1在状态在状态 1 1运行后得运行后得到状态到状态 2 2且没有后续语句要执行（程序结束）且没有后续语句要执行（程序结束） 。变迁系统变迁系统v小结：描述小结：描述IMP语言的操作语义：语言的操作语义： 格局格局 程序（命令）程序（命令）c在状态下在状态下 运行运行 程序终止的状态程序终止的状态 变迁关系变迁关系 定义定义IMPIMP语言的操作语义就是定义适当

12、格局之间的变迁关语言的操作语义就是定义适当格局之间的变迁关系系 通过定义通过定义IMPIMP语言的每个命令所引起的变迁来完成语言的每个命令所引起的变迁来完成表达式的语义表达式的语义v 表达式是表达式是IMPIMP语言的最基本的语法成分，包括算术表达式和语言的最基本的语法成分，包括算术表达式和逻辑表达式逻辑表达式v 程序执行是对程序状态的变换；而表达式的计算并不改变程程序执行是对程序状态的变换；而表达式的计算并不改变程序状态，可以看作是对程序序状态，可以看作是对程序状态状态的某种的某种观察观察。 状态状态 ：LocNLocN 定义一个新状态定义一个新状态 xv ( / )( )( ) vyxv

13、xyyyx 程序变量程序变量x x在该状态下的值就是在该状态下的值就是v v，而其他变量的，而其他变量的值不变（未知或不关心）值不变（未知或不关心） / v x表达式的语义表达式的语义算术表达式的求值算术表达式的求值010101A exp : :|anxaaaaaav 序偶序偶a, 表示状态表示状态 下表达式下表达式a a等待求值等待求值v 求值关系：求值关系：:,anA状态下表达式a的求值结果为n表达式的语义表达式的语义算术表达式的求值算术表达式的求值v 求值规则求值规则001101010011010100110101,( ),nnn,nnn,nnn,nnxxananaanananaanan

14、anaan其中 是与 的和其中 是与 的差其中 是与 的积表达式的语义表达式的语义逻辑表达式的求值逻辑表达式的求值v 求值规则（求值规则（1 1）00110101001101010011010100110101,(,truetruefalsefalseanannnaatrueanannnaafalseanannnaatrueanannnaafalse如 果等 于如 果不 等 于如 果小 于 等 于如 果大 于表达式的语义表达式的语义逻辑表达式的求值逻辑表达式的求值v 求值规则（求值规则（2 2）001101001101, , ,btruebfalsebfalsebtruebtbtbbtbtbt

15、bbt 当t0为true且t1为true时t为true，否则为false当t0为true或t1为true时t为true，否则为false表达式的语义表达式的语义逻辑表达式的求值规则逻辑表达式的求值规则00110101001101010011010100110101,(,truetruefalsefalseanannnaatrueanannnaafalseanannnaatrueanannnaafalsebt如果等于如果不等于如果小于等于如果大于001101001101, , ,ruebfalsebfalsebtruebtbtbbtbtbtbbt 当t0为true且t1为true时t为true，

16、否则为false当t0为true或t1为true时t为true，否则为false表达式的语义表达式的语义逻辑表达式的求值逻辑表达式的求值v 最左顺序计算（短路）最左顺序计算（短路）00101010101, ,bfalsebbfalsebtruebfalsebbfalsebtruebtruebbtrue表达式的语义表达式的语义说明：说明：v 规则规则一般包括前提和结论，后面的条件称为附加条件。一般包括前提和结论，后面的条件称为附加条件。v 有些规则没有前提部分，前提为空的规则称为公理。（有时有些规则没有前提部分，前提为空的规则称为公理。（有时在上面加一条实线）在上面加一条实线）v 由前提推出结论

17、称为规则的一个应用。由前提推出结论称为规则的一个应用。v 用特定的数、存储单元、表达式以及状态来替代规则的元变用特定的数、存储单元、表达式以及状态来替代规则的元变量，就得到一个量，就得到一个规则实例规则实例。v 求值过程求值过程推导树。推导树。表达式的语义表达式的语义v 状态状态 0 0下表达式下表达式(Init+5)+(7+9)(Init+5)+(7+9)的求值，的求值， 0 0(Init)=0(Init)=00000000,05,5 7,79,9 (5),5(7 9),16(5) (7 9),21InitInitInit0,0Init00,05,5Init000,05,5 (5),5Ini

18、tInit000000,05,5 7,79,9 (5),5(7 9),16InitInit 推导树由规则的实例构成，每个实例的前提正好是上一层实例的推导树由规则的实例构成，每个实例的前提正好是上一层实例的结论；结论； 公理位于最顶层，公理的上方没有前提部分；公理位于最顶层，公理的上方没有前提部分； 最底层的实例的结论称为整个推导的结论。最底层的实例的结论称为整个推导的结论。 如果某个推导存在结论，称该结论是从规则可如果某个推导存在结论，称该结论是从规则可精确推导精确推导的。的。 匹配的规则可能有多条，必须考虑所有左部与格局匹配的规则；匹配的规则可能有多条，必须考虑所有左部与格局匹配的规则；对于

19、符合条件的所有推导必须并行地构造。对于符合条件的所有推导必须并行地构造。表达式的语义表达式的语义v状态状态 下布尔表达式下布尔表达式(x(x* *y)z) y)z) +(z+x=0)+(z+x=0)的求值，的求值， (x)=3(x)=3， (y)=5(y)=5， (z)=7(z)=7,3,5 ,7,3 ,70,0(),15(),10(),() 0,()() 0,xyzxzx yz xx yzfalsez xfalsex yzz xfalse =表达式的语义表达式的语义v 算术表达式的等价算术表达式的等价 v 逻辑表达式的等价逻辑表达式的等价0101(.,)aaiffnNanan 0101(.,

20、)bbifftbtbt 命令的语义（自然语义）命令的语义（自然语义）v 操作语义定义适当格局之间的变迁关系操作语义定义适当格局之间的变迁关系v 程序（命令）通过执行来改变状态程序（命令）通过执行来改变状态,cv 表示在状态表示在状态 下执行完命令下执行完命令c c终止于终态终止于终态 。v 例如：例如：: 5,x: 5,5/ xx命令的语义（自然语义）命令的语义（自然语义）命令的规则（命令的规则（1 1） , :,/ skipamxam xv 原子命令原子命令实例：实例： 初始状态下所有存储单元的值均为初始状态下所有存储单元的值均为0 000 :1,1/ xxx命令的语义（自然语义）命令的语义

21、（自然语义）命令的规则（命令的规则（2 2）0101, ;,ccc cv 顺序命令顺序命令实例：实例：000000:1,1/ :1,1/ 1/ 2/ :1;:1,1/ 2/ xxxyxxxyxxyxxy命令的语义（自然语义）命令的语义（自然语义）命令的规则（命令的规则（3 3）001, ,btruecif b then c else cv 条件命令条件命令101, ,bfalsecif bthen c else c命令的语义（自然语义）命令的语义（自然语义）命令的规则（命令的规则（3 3）条件命令实例：条件命令实例：000000, (0):1,xtrueskipifxthen skip els

22、e xx0( )0 x111110,:1,2/ (0):1,2/ xfalsexxxifxthen skip else xxx1( )1x命令的语义（自然语义）命令的语义（自然语义）命令的规则（命令的规则（4 4）, , ,falsewhiledotruewhiledowhiledobbcbcbcbcv 循环命令循环命令命令的语义（自然语义）命令的语义（自然语义）命令的规则（命令的规则（4 4）000(1),1/ (1):1,1/ 1/ falsewhixxxxxxxledov 循环命令实例循环命令实例0000000(1),:1,1/ (1):1,1/ 1/ (1):1,1/ xxxxtrue

23、whiledowhilexxxxxxxdxxo循环体每执行一步的变迁关系命令的语义（自然语义）命令的语义（自然语义）:1 whiledotruexxv 死循环死循环0000:1,1/ :1,1/ ? :1,?xxxwhiledtruexowhilxxtruexxedo0000:1,1/ 2/ :1,2/ ? :1,1/ ?xxxxtruexxxtruwhiledowhiledexoxx这种推导是无穷的，因此，实际上不存在状态这种推导是无穷的，因此，实际上不存在状态 使得：使得：0:1, truexwxhiledo语义无定义语义无定义命令的语义（自然语义）命令的语义（自然语义）命令的规则小结命令

24、的规则小结0101001101 , :,/ , ;, , , , skiptrueifthenamxam xccc cbcbc elsefalseifthenelsefalsewhilecbcbdcbocbcb , ,truewhicbcbcledowhiledo命令的语义（自然语义）命令的语义（自然语义）v 推导树推导树 例1：交换程序命令的语义（自然语义）命令的语义（自然语义） 例2：阶乘程序 0(x)=3， 0(y)=0命令的语义（自然语义）命令的语义（自然语义）v小结：自然语义小结：自然语义 c, 可以看作如下形式的函数： 对任意的命令c，自然语义函数是从状态集到的部分函数有定义无定义

25、 至多存在一个终止状态:()nsCom Sn等价关系及证明等价关系及证明v命令的等价（语义等价）命令的等价（语义等价） 0101,.,)cciffcc 例： wwhileb do c;if b then c welse skip等价关系及证明等价关系及证明v命题命题2.82.8（P16P16） ; wif bthen c welse skipv证明：证明： ,;,wiffif b then c w else skip对所有的状态，有： 两方面： “” “” 等价关系及证明等价关系及证明,;,wiffif b then c w else skip（1）“”, (1),bfalsew,(2),bt

26、ruecww等价关系及证明等价关系及证明, (1),bfalsew.,bfalsew.,;,bfalseskipif bthen c welse skip等价关系及证明等价关系及证明,(2),btruecww.,btruecww.,; ,cwc w.,; ,;,cwbtruec wif b then c w else skip,;,wif b then c w else skip等价关系及证明等价关系及证明,;,wiffif b then c w else skip（2）“”., (1);,bfalseskipif bthen c welse skip.,; , (2);,btruec wif

27、 b then c welse skip等价关系及证明等价关系及证明., , (1);,bfalseif bthen c welse skispkip,skip由于：所以：.,bfalsew.,bfalsew等价关系及证明等价关系及证明., .;(,2)btrueif b then c welse skipc w.,;,cwc w.,btruecww,;,wif b then c w else skip,;,wif b then c w else skip自然语义小结自然语义小结v自然语义自然语义 c, 至多存在一个终止状态语义等价关系0101,.,)cciffcc ; wif bthen c

28、 welse skip自然语义小结自然语义小结0101001101 , :,/ , ;, , , , skiptrueifthenamxam xccc cbcbc elsefalseifthenelsefalsewhilecbcbdcbocbcb , ,truewhicbcbcledowhiledo自然语义小结自然语义小结练习：整除程序的推导树：练习：整除程序的推导树：:;: 0;():;:1sumyzwhile sumx do sumsumy zz04,2,0,0 xyzsum自然语义小结自然语义小结练习：整除程序的推导树：练习：整除程序的推导树：0:;: 0;():;:14,2,0,0su

29、my zwhile sumx do sumsumy zzxyzsum信息工程学院计算机系信息工程学院计算机系另一种语义（结构化操作语义）另一种语义（结构化操作语义）v 与自然语义比较与自然语义比较 自然语义所给出的变迁关系是一步到位的 另一种语义（结构化操作语义） 描述程序执行中每一小步的中间状态 , anbt , c1 , cc : 5;: 7,xy1 : 5;: 7,: 7, 5/ xyyx 11 : 5;: 7,: 7, 5/ 5/ 7/ xyyxxy 另一种语义（结构化操作语义）另一种语义（结构化操作语义） , :,/ amxskiaxpm原子命令的结构化操作语义原子命令的结构化操作语

30、义另一种语义（结构化操作语义）另一种语义（结构化操作语义）0011000101, ;, ;,;, cc ccccc ccc顺序命令的结构化操作语义顺序命令的结构化操作语义另一种语义（结构化操作语义）另一种语义（结构化操作语义）010011, , , trueifthenelsefalseifthenelsebbcccbbccc条件命令的结构化操作语义条件命令的结构化操作语义另一种语义（结构化操作语义）另一种语义（结构化操作语义） , , ,;,bbcbfalsewhiledotruewhibledo cc whileb do c循环命令的结构化操作语义循环命令的结构化操作语义另一种语义（结构化

31、操作语义）另一种语义（结构化操作语义）0011000101010011 , :,/, ;, ;,;, , , skiptrueifthenelsamxamxcccccefalsccccceifthenelsebbcccbbcccbfals , ,;,ewhiledotruewhiledobcbbcc while b do c 规则：另一种语义（结构化操作语义）另一种语义（结构化操作语义）例例1 1：交换程序：交换程序 推导序列推导序列0000:; :;:,:;:,5/ :,5/ 7/ 5/ 7/ 5/ zx xy yzxy yzzyzzxzxy另一种语义（结构化操作语义）另一种语义（结构化操作

32、语义）推导序列推导序列另一种语义（结构化操作语义）另一种语义（结构化操作语义）另一种语义（结构化操作语义）另一种语义（结构化操作语义）例例2 2：阶乘程序：阶乘程序03,0: 1;(1) :;:1xyywhile xdo yyx xx0000(1) :;:1,1/ :;:1;(1) :;:1,1/ :1;(1): :;:1,3/ (11;(1) :;:1,) :;:1while xdo yyx xxyyyx xxwhile xdo yyx xxyxxwhile xdo yyx xxywhile xdo yyywhile xdo yyxxxxxx 00000,3/ 2/ :;:1;(1) :;:

33、1,3/ 2/ :1;(1) :;:1,6/ 2/ (1) :;:1,6/ 1/ 6/ 1/ yxyyx xxwhile xdo yyx xxyxxxwhile xdo yyx xxyxwhile xdo yyx xxyxyx 另一种语义（结构化操作语义）另一种语义（结构化操作语义）例例2 2：阶乘程序：阶乘程序03,0: 1;(1) :;:1xyywhile xdo yyx xx0000:;:1;(1) :;:1,1/: 1;(1) :;:1,(1):1;(1) :;:1,3/ (1) :;:1:;:1,1/ yyx xxywhile xdo yyx xxwhile xdwhile xdo

34、yyx xxyxxwhile xdo yyx xxywhio yyx xxyle xdo yyx xx 00000,3/ 2/ :;:1;(1) :;:1,3/ 2/ :1;(1) :;:1,6/ 2/ (1) :;:1,6/ 1/ 6/ 1/ yxyyx xxwhile xdo yyx xxyxxxwhile xdo yyx xxyxwhile xdo yyx xxyxyx 另一种语义（结构化操作语义）另一种语义（结构化操作语义）例例2 2：阶乘程序：阶乘程序03,0: 1;(1) :;:1xyywhile xdo yyx xx0000: 1;(1) :;:1,(1) :;:1,1/ :;:

35、1;(1) :;:1,1:1;(1) :;:1,3/ (1) :;:1/ ywhxxwhile xdo yyx xxywhile xdo yyxile xdo yyx xxwhile xdo yyx xxyyyx xxwhile xdo yyx xxxxy 00000,3/ 2/ :;:1;(1) :;:1,3/ 2/ :1;(1) :;:1,6/ 2/ (1) :;:1,6/ 1/ 6/ 1/ yxyyx xxwhile xdo yyx xxyxxxwhile xdo yyx xxyxwhile xdo yyx xxyxyx 另一种语义（结构化操作语义）另一种语义（结构化操作语义）例例2 2

36、：阶乘程序：阶乘程序03,0: 1;(1) :;:1xyywhile xdo yyx xx0000: 1;(1) :;:1,(1) :;:1,1/ :;:1;(1) :;:1,1/ :1;(1) :;:11) :;:1,3/ ywhwhile xdoile xdo yyx xxwyyhile xdo yyx xxyyyx xxwhile xdo yyx xxyxxwhile xdo yyx xxxxyx 00000,3/ 2/ :;:1;(1) :;:1,3/ 2/ :1;(1) :;:1,6/ 2/ (1) :;:1,6/ 1/ 6/ 1/ yxyyx xxwhile xdo yyx xxy

37、xxxwhile xdo yyx xxyxwhile xdo yyx xxyxyx 另一种语义（结构化操作语义）另一种语义（结构化操作语义）例例2 2：阶乘程序：阶乘程序03,0: 1;(1) :;:1xyywhile xdo yyx xx0000: 1;(1) :;:1,(1) :;:1,1/ :;:1;(1) :;:1,1/ :1;(1) :;:1,3/ (1) :;:1ywhile xdo yyx xxwhile xdo yyx xxyyyx xxwhile xdo yyx xxyxxwhile xdo yyx xxywhile xdo yyx xx 00000:;:1;(1) :;:1

38、,3/ 2/ :1;(1,3/ ) :;:1,6/ 2/ (1) :;:1,6/ 1/ 6/ 2/ 1/ yyx xxwhile xdo yyx xxyxxxwhile xdo yyx xxyxwhile xdo yyxyxxxyxyx 另一种语义（结构化操作语义）另一种语义（结构化操作语义）例例2 2：阶乘程序：阶乘程序03,0: 1;(1) :;:1xyywhile xdo yyx xx0000: 1;(1) :;:1,(1) :;:1,1/ :;:1;(1) :;:1,1/ :1;(1) :;:1,3/ (1) :;:1ywhile xdo yyx xxwhile xdo yyx xxyyyx xxwhile xdo yyx xxyxxwhile xdo yyx xxywhile xdo yyx xx 00000:1;(1,3/ 2/ :;:1;(1) :;:1,3/ 2/) :;:1,6/ 2/ (1) :;:1,6/ 1/ 6/ 1/xxwhile xdo yyx xxyxwhile xdo yyx xyxyyx xxwhile xdo yyx xxyxxyxyx 另一种语义（结构化操作语义）另一种语义（结构化操作语义）例例2 2：阶乘程序：阶乘程序03,0: 1;(1) :;:1