第五部分操作语义2010.pptVIP

程序设计形式语义学 3 操作语义 通过规定程序设计语言在抽象机器上的执行过程来描述程序设计语言的含义。 本章中举例：由规则规定求值和执行关系，是语法制导的。 3.1 IMP程序设计语言 IMP是一种带while程序的小型语言，其程序在运行时要依靠一连串的显式命令进行状态转换，因此IMP被称为是一种命令式语言。 从形式上看，IMP的行为由一组规则来描述，规则规定了表达式如何计算和命令如何执行。 IMP的操作语义也由规则来确定。 3.1 IMP程序设计语言的语法集合 数集N，它是正整数、负整数和零的集合。 真值集T={true, false}。 存储单元集Loc。 算术表达式集Aexp。 布尔表达式集Bexp。 命令集Com。 3.1 IMP程序设计语言的语法集合 数集N：带符号位的正负十进制数集合。 真值集T={true, false}。 存储单元集Loc：非空字母或后跟数字的非空字符串的集合。 算术表达式集Aexp。 布尔表达式集Bexp。 命令集Com。 3.1 IMP程序设计语言的语法集合 描述IMP语法时对某些特定字母的约定： n,m表示数集N中的元素。 X,Y表示存储单元集Loc中的元素。 a表示算术表达式集Aexp中的元素。 b表示布尔表达式集Bexp中的元素。 c表示命令集Com中的元素。 上述特殊字母还可以加撇和下标进行表示。 3.1 IMP程序设计语言的语法集合 Aexp、Bexp和Com的构造规则： Aexp a::=n|X|a0+a1|a0-a1|a0×a1 Bexp b::=true|flase|a0=a1|a0≤a1|﹁b|b0∧b1|b0∨b1 Com c::=skip|X:=a|c0;c1|if b then c0 else c1|while b do c 3.2 IMP编写的程序的状态 对IMP语言编写的程序进行理解时，易形成一个思维模式：存储单元的内容决定了状态。 对于每个状态，算术表达式的求值结果都是一个整数，布尔表达式的求值结果都是一个布尔值。求值的结果影响命令的执行，从而引起状态的变化。 因此，对IMP编写程序的行为的形式化描述也体现上述思想。首先定义程序运行的状态，然后定义算术表达式和布尔表达式的求值，最后定义命令的执行。 3.2 IMP编写的程序的状态 状态集合∑由存储单元集到数集的函数δ:Loc→N组成。 δ(X)表示状态δ下存储单元X的值或内容。 a,δ →n表示在状态δ下表达式a的求值结果是n。 3.3 算术表达式的求值规则 整数求值： n,δ →n，任一整数的求值结果就是本身。 存储单元求值： X,δ →δ(X)，在一个状态下存储单元的求值结果就是它的内容。 加法求值： a0, δ →n0 a1, δ →n1 ，其中n是n0与n1的和 a0+a1,δ →n 减法求值： a0, δ →n0 a1, δ →n1 ，其中n是n0与n1的差 a0-a1,δ →n 乘积求值： a0, δ →n0 a1, δ →n1 ，其中n是n0与n1的积 a0×a1,δ →n 算术表达式求值的规则实例 用特定的数、存储单元、表达式以及状态来替代规则的元变量，就得到一个规则实例。 2, δ0 →2 3, δ0 →3 2×3,δ0 →6 算术表达式求值的推导 状态δ0下的表达式a≡(Init + 5) + (7 + 9)的求值，其中已知Init是状态δ0下δ0(Init)=0的存储单元。 求值过程如下： Init, δ0→0 5, δ0→5 7, δ0→7 9, δ0→9 Init+5, δ0→5 7+9, δ0→16 (Init + 5) + (7 + 9), δ0→21 称这样的结构为推导树，简称推导。推导树由规则的实例构成，每个实例的前提正好是上一层实例的结论；公理位于最顶层，并且公理的上方没有前提部分。最底层的实例的结论称为整个推导的结论。 算术表达式求值的推导 在这种方式下，规则提供了基于查找推导树计算算术表达式的一个算法。因为它易于直接实现，所以这些规则以操作的方式规定了算术表示式的语义，此时就说这组规则给出了表达式的操作语义。 3.4 布尔表达式的求值规则 布尔表达式的求值为真值(true，false)的规则如下： 1. true,δ→true 2. false,δ→false 3. a0,δ →n a1,δ →m，如果n等于m a0 = a1,δ →true 4. a0,δ →n a1,δ →m，如果n不等于m a0