第四章 程序语言的性质

语言的形式化模型 BNF为描述程序设计语言的属性提供了一种很好的手段，但并不是充分的手段。BNF回答了程序看起来象什么，但没有回答程序是做什么的。 形式化模型采用精确的数学模型来刻画研究对象，为研究、分析和操纵研究对象提供严谨的数学工具和手段。 本章将介绍下列形式化模型： 形式文法：乔姆斯基文法分级 语言的语义：属性文法、指称语义 程序的验证

4.1 语言的形式化性质 乔姆斯基分级文法 语言的能力

乔姆斯基分级文法 文法 文法的类别 由非终结符、终结符、开始（非终结）符、及产生式构成 3型文法：正则文法，定义词法的模型 2型文法：BNF文法，上下文无关文法 1型文法：上下文有关文法 0型文法：

3型文法：正则文法 为词法分析器提供模型。 这类文法的大多数性质都是可判定的 正则文法可以产生形如an的串，其中a为有限字符序列 如，能产生什么样的串、给定串是否属于文法规定的语言、语言中的串是否有限等 正则文法可以产生形如an的串，其中a为有限字符序列 正则文法只能计数有限数 常用于关键字或单词扫描

2型文法—上下文无关文法 产生式的形式为：X  , 其中可以是终结符和非终结符的任意序列 同样，这类文法的大多数性质都是可判定的 如，能产生什么样的串、给定串是否属于文法规定的语言、语言是否为空等 可用来计数和比较两个项，产生形如ancbn的串 可以用堆栈来实现 可用来自动产生程序的语法分析树 2型和3型文法的相关问题都已基本上得到解决

1型文法—上下文有关文法 产生式的形式为：  , 其中任意非终结符串， 是终结符和非终结符的任意序列，但中的符号个数应不多于的符号个数 从开始符开始导出的串的长度是递增的 在生成串时，需要使用固定数量的存储空间，例如识别上下文无关文法无法识别的串ancnbn 上下文有关文法太复杂，很难用于程序设计语言 人们对上下文有关文法的很多特征还不太清楚

0型文法—非限定型文法 对产生式的形式  没有任何限制 可用来识别任意可计算的函数 其大多数性质都是不可判定的 返回

不可判定性 不同类型的文法越来越复杂，产生的语言也越来越复杂，但是否说明计算机解决问题的能力可以越来越强，没有限制？ 例如：能否编写一个C语言程序来判断另一个C语言程序能否结束？ 但这基本上是不可能的，这不是编程人员的问题，而是因为计算机所基于的数学模型本身的局限性而导致的。

图灵机 一般来说，用一种语言编写的程序也可以用其他另一种语言来实现。 那么是否存在某个程序，只能用某种语言来实现，而用其他语言就无法实现？ 如果没有，那么有哪些程序是其它程序设计语言无法表示的，为什么还需要那么多种不同的语言？ 如果我们将能够表示所有计算的语言都称为通用语言，那么是不是所有语言都是通用语言？如果是，是否存在更简单的通用语言？

图灵机的结构 图灵机是一种用来定义可计算函数的抽象计算机 图灵机只有一个单一的数据结构，即一个称为“带子”的可变长线性数组 带子被分为很多格，每格上只包含一个字符 图灵机还有一个指针变量，称为“读出头”，它总是指向带子上的某个格。

图灵机的操作 图灵机只提供几个简单的操作： 读出头所指定位置的字符可以被读出或被修改。程序可以根据读出的值进行转移。 读出头可以左右移动。如果读出头移动到带子的最末端，则自动在带子上加上一格，并赋予一个空字符作为初始值。

图灵机的运行 图灵机开始运行时，带子上存放输入数据，读出头指向输入数据的最左端的字符； 图灵机根据预先编好的操作序列读写带子上的数据、或移动读出头； 如果最终能够停机，则带子上的内容就是最后的输出结果。

图灵机的能力 任意可计算函数都可以用图灵机计算出来（Church论题） 图灵机等价于0型文法 确定型图灵机等价于非确定型图灵机。

停机问题 是否存在某个通用的算法，它能够断定任意给定的图灵机在任意的输入下能否停机？ 任意一个不可判断的问题，都等价于停机问题。 结论： 停机问题是不可判断的，即不存在这样的通用算法。 任意一个不可判断的问题，都等价于停机问题。 结论： 任何一种程序设计语言都可能代替其它语言 程序设计语言不存在质的区别，只有量的区别，如是否优美、易用、高效等 任何一种程序设计语言都有它存在的理由 返回

4.2 语言的语义 程序设计语言基本上都是以上下文无关文法(特别是 LR(k) 文法)的核心设计的。 但语法分析已经不再是人们感兴趣的研究问题了。 现在的问题是如何确定程序的含义（即语义）。

语言的语义 语言的手册必须定义语言中每个结构的含义，包括单独结构的含义以及和其他结构组合时的含义。 语言提供了不同结构，用户（为了写正确的程序，预测语句的执行效果）和实现者（正确地实现语言）需要这些结构的精确定义。 大多数语言中，形式文法用于定义语法，一段文字或例子用于定义语义，但定义是不精确的，有二义性，不同作者可能有不同理解。 语义定义问题还是理论研究的目标，但至今没有令人满意的解答。 已有各种形式方法用于语义定义。

语义建模（1）—文法模型 对定义语言的BNF文法进行扩展，给出程序的语法分析树，从树中抽取出附加信息。属性文法便是抽取附加信息的一种方式。

语义建模（2）—命令或操作模型 定义程序如何在某虚拟机上执行。通常描述为一自动机，但比语法用的简单自动机远为复杂。 自动机有内部状态——对应程序执行时的内部状态，包括所有变量的值、执行程序本身、以及各种系统定义的数据结构。

语义建模（2）—命令或操作模型 一组形式定义的操作用于刻划自动机内部状态如何改变。此外还需定义程序文本如何翻译成自动机的初始状态。 语言的操作定义对语言如何实际执行给出了相当直接的抽象。 也可能提出一个更抽象的模型，作为语言的软件解释的基础。 70年代的VDL（Vienna Definition Language）是一个操作方法。 它扩展语法分析树已包含机器解释器。 计算的状态是程序树加上描述机器中所有数据的树。 每条语句的执行使树的状态发生变化。

语义建模（3）—作用型模型 试图直接构造每个程序的函数的定义，采用层次式的构造方式。 程序中每个基本的或程序员定义的操作代表一个数学函数。 语言的程序控制结构用于将这些函数复合为更大的序列，代表表达式和语言。 语句序列和条件分叉表示为个体函数构造而成的函数。 循环通常表示为递归函数。 最终，为整个程序导出一个完整的函数模型，指称语义归于此类。

语义建模（4）—公理模型 使用谓词演算，每个语法结构的语义被描述为公理或推导规则，用于导出结构的执行效果。 从一个初始假设开始， 假设输入变量满足一定的约束， 在程序语句执行后，使用公理和推导规则来推导其他变量值需满足的限制， 最终，程序的结果被证明满足希望的约束（描述了它们的值和输入值的关系）。 如Hoare的公理语义。

语义建模（5）—规约模型 描述实现程序的各个函数的关系，只要我们可以证明一个实现符合了所有的函数间的关系，则称实现相对于规约是正确的。 代数数据类型是形式规约的一种形式。 例如：实现栈的程序，S表示栈，则有公理， pop(push(S,x))=S 任何一个实现如果能保持这种关系，则称是栈的正确实现。

语义模型—小结 上述各种形式语义模型各有优点，但均不能称为完全实用的和适用的，各有其适合范围。 操作语义为语言的实现提供了一种形式模型，但对用户来说太细节 公理语义易于理解，但很难用来定义复杂的程序设计语言，且缺乏对语言实现的支持 返回

语义建模—属性文法 这是最早的开发语义模型的工作之一。 其思想是对分析树中的每个结点关联一个函数，从而给出结点的语义内容。 属性文法的创建过程是为文法中的每一条规则都定义相关的语义函数。 继承属性是一个函数，它将树中非终结符值和树中更高层的非终结符值相关联。换言之，任何规则右端的非终结符的函数值是左端非终结符的函数。 综合属性是一个函数，它将左端非终结符和右端非终结符的值相关联，这些属性在树中向上传递信息，即从树中下层信息进行“综合”。

属性文法 例：考虑算术表达式的简单文法。 其语义通过文法中非终结符间的关系集合定义。如：下面函数生成该文法生成的任意表达式的值： E→T|E+T T→P|T×P P→I|(E) 其语义通过文法中非终结符间的关系集合定义。如：下面函数生成该文法生成的任意表达式的值： 产生式 属性 E→E+T Value(E1)=V(E2)+V(T) E→T V(E)=V(T) T→T×P V(T1)=V(T2)×V(P) T→P V(T)=V(P) P→I V(P)=数I的值 P→(E) V（P）=V（E）

属性文法 下图是一个属性树，它给出了表达式2+4×(1+2)值

属性文法 属性文法可用于在语法树中传递语义信息。例如，声明信息可以通过语言的声明产生式收集。沿树向下传的符号表信息可用于生成表达式代码。 下面属性可加到非终结符<decl>和<declaration>来创建一个程序中声明的名字集合。 产生式 属性 <declaration>::=<decl><declaration> decl_set(declaration1)=declaname(decl) ∪decl_set(declaration2) <declaration>::=<decl> decl_set(declaration)=decl-name(decl) <decl>::=declare x decl-name(decl)=x (decl)::=declare y decl-name(decl)=y (decl)::=declare z decl-name(decl)=z 这是综合属性，包含程序中声明的名字集合。该属性可以沿树向下传递，成为继承属性，用于正确地生成数据的代码。

属性文法的使用 首先创建语法分析树。属性文法假设你已经知道表达式是如何推导出来的，它并不关心是如何分析推导出来的。 定义属性的函数可以是任意给定的，因此定义属性的过程完全是手工完成的。 如果只有综合属性，并且文法是 LR(k)，那么，属性文法可以用来在语法分析时自动产程中间代码。 这就是 YACC 如何工作的，它利用属性文法来计算所有非终结符的值。 在构造分析树时，非终结符的信息逐层向上传递给分析树上层的非终结符。 语法分析完毕，所有属性的值将计算出来。 返回

指称语义 指称语义是一种用来描述程序设计语言的语义的作用型语义模型 指称语义基于-演算

-演算 -演算是一种和图灵机的计算能力相当的理论计算模型 -演算可以作为程序设计语言的函数调用的模型 Algol和Lisp都采用来-演算的函数调用语义 指称语义是对-演算的扩充，它将-演算扩充为一种通用的数据类型理论

-演算的表达式 -表达式可以递归地定义如下： 形式语法： 变量名为-表达式 如果M为一个-表达式，则x.M也是一个-表达式 如果F和A都是-表达式，则(F A)也是-表达式，其中F为操作符，A为操作数。 形式语法： -expr ::= id | id.-expr | (-expr -expr) x相当于申明参数变量x，没有申明的变量为自由变量，否则为约束变量。 x.M相当于函数申明，其中x相当于M的参数。 例如： x x.x x.(xy) x.y (x.x y.y)

-表达式的操作 -表达式只有一种操作：约简 (F A)约简相当于将A作为实际参数，替换F的形式参数的所有出现 例如： (x.M A)  M’，相当于用A替换M中x的所有自由出现。 例如： (x.x y)  y (x.(xy) x.x)  x.x y  y 注意：约简并不一定能简化原来的表达式 (x.(xx) x.(xx))  (x.(xx) x.(xx))  ……

指称语义 指称语义的基本思想是定义一个语义函数（指称函数），把程序的意义映射到某种意义清晰的数学对象（就像用中文解释英文） 作为被指的数学对象可以根据需要选择 对于简单的程序语言，一种很自然的选择是把程序的语义定义为（指称为）从状态到状态的函数。定义语义就是定义好每个程序对应的函数。 程序的状态由标识符到值的映射集合构成 S = { id | value, … }

指称语义 表达式的语义 [e]  S  val 语句的语义 [s]  S  S 程序的语义 [m]  val  val

指称语义 设为程序的当前状态 语句的语义 程序的语义 表达式的语义 赋值语句：[x = e] =   {x | [e]} 常数：[n] = n 变量：[x] = (x) 算术表达式：[e1 + e2] = [e1] + [e2] 语句的语义 赋值语句：[x = e] =   {x | [e]} 复合语句：[s1; s2] = [s2]([s1]) 条件语句：[if b then s1 else s2] = if [b] then [s1] else [s2] 程序的语义 [m]  val  val 返回

程序验证 在编程时，人们越来越关心程序的正确性和可靠性。人们在设计程序设计语言时，也希望通过增加新的特征来增强程序的正确性和可靠性。 我们可以用程序语义，按以下方式来探讨程序的正确性问题： 给定程序P，其含义是什么？即，它的规范描述S是什么？ 给定规范描述S，开发实现了该规范描述的程序P 规范描述S和程序P是否完成了相同的功能（执行了相同的函数）？ 相当于语义建模问题 软件工程的核心问题 程序验证的核心问题

程序验证 测试不能保证程序的正确性 如果能找到不依赖于测试的保证程序正确性的方法，产生的程序就能更加可靠： 程序计算了一个函数 如果能给出该函数的规范描述，并且能够根据程序知道它到底计算了一个什么样的函数，那么，如果能够证明程序所计算的函数与给定的函数等价或相同，就能证明程序的正确性，而不需再测试。

形式化的规范描述 任一程序都可以表示成流程图 基调：函数名：定义域  值域 fun1: S1 and P1  S3 fun2: S1 and not(P1)  S3 fun3: S3 and not(P3)  S4 fun4: S3 and P3  S4 S2 and P2 = S4 S2 and not(P2) = S3 P1 P2 P3 Fcn1 Fcn4 Fcn3 Fcn2 S1 S2 S3 S4

形式化的规范描述（续） 这样，程序可以看成是一个定义在其基本成分上的复杂函数： C(fun1, fun2, fun3, fun4, p1, p2, p3): S1  S4 如果我们能够形式化地推导出上述关系，那么我们就能够从数学上证明，给定S1, 程序将终止于状态 S4。 但是：证明非常困难。 另外，在证明时，我们总是想证明程序和某个给定的形式化规范等价，但问题是，如果没有给出规范描述，“程序是否正确？”可能就没有了意义。

公理化验证 用谓词逻辑公式来刻画程序的语义、用谓词演算来验证程序的正确性。 Tony Hoare 在1969年提出的。 每个程序都遵循某种形式化的公理定义。 实证（Validation）: 通过一系列测试数据的测试，展示程序满足了其规范描述。 验证（Verification）: 根据程序结构，通过形式化的讨论，展示程序满足了其规范描述。 Validation一般认为需要执行程序，而 verification不需要。

谓词逻辑公理 {P1}S{P2} 表示如果 P1 为真，则在 S 执行并终止后，P2 将为真。 如果 A 为真，则 B 也为真。 逻辑公理： 组合 顺序1 顺序2 {P}S1{Q},{Q}S2{R} [组合语句] {P}S1;S2{R} {P}S{R}, RQ [增加后置条件] {P}S{Q} PR, {R}S{Q} [增加前置条件] {P}S{Q}

语句类型的公理 条件语句1 条件语句2 While循环语句 赋值语句 {P^B}S{Q}, P^not(B)Q {P}if B then S{Q} 条件语句1 条件语句2 While循环语句 赋值语句 {P^B}S1{Q},{P^not(B)}S2{Q} {P}if B then S1 else S2{Q} {P^B}S{P} {P}while B do S{P ^ not(B)}，其中 P 为不变式 {P(e)}x:=e{P(x)}，P(x) 为 x 的谓词。

公理化的程序证明 给定程序：s1; s2; s3; s4; … sn 及其规约：P 和 Q 通过证明下列的谓词来证明 {P}s1;…sn{Q}： {P}s1{p1} {p1}s2{p2} … {pn-1}sn{Q} 反复运用组合公理，产生： {P}s1; …; sn{Q}

例子 {B>=0} 1 X:=B 2 Y:=0 3 while X>0 do 4 begin 5 Y:= Y+A 6 X:= X-1 7 end {Y=AB} 即，给定非负的 B，证明当程序终止时， Y=A*B.

证明过程概要 一般通过回溯来进行。 首先，找到循环的不变式： 可以试着用 (Y+X*A=A*B and X>=0)作为不变式

证明 赋值语句公理(6): {(Y+(X-1)A=A*B and X-1>=0)} X:=X-1 {(Y+X*A=A*B and X>=0)} 赋值语句公理(5): {((Y+A)+(X-1)A=A*B and X-1>=0)} Y:=Y+A {(Y+(X-1)*A=A*B and X-1>=0)} 组合公理 (5,6): {(Y+A)+(X-1)*A=A*B and X-1>=0)} Y:=Y+A; X:=X-1 {(Y+X*A=A*B and X>=0)} 数学定理: Y+X*A=A*B and X>0  ((Y+A)+(X-1)*A=A*B and X-1>=0) 顺序语句公理: {Y+X*A=A*B and X>0} Y:=Y+A; X:=X-1 {(Y+X*A=A*B and X>=0)} 数学定理: (Y+X*A=A*B and X>=0) and (X>0)  Y+X*A=A*B and X>0 顺序语句公理: {(Y+X*A=A*B and X>=0)and (X>0)} Y:=Y+A; X:=X-1 {(Y+X*A=A*B and X>=0)} [用 ** 来代替] While循环语句公理: ** {Y+X*A=A*B and X>=0}while X>0 do Y:=Y+A; X:=X-1 {(Y+X*A=A*B and X>=0) and not(X>0)}

证明 (续) 数学定理: (Y+X*A=A*B and X>=0) and not(X>0) (Y+X*A=A*B and X=0) Y=AB 顺序语句公理: {Y+X*A=A*B and X>=0}while X>0 do Y:=Y+A; X:=X-1 {Y+A*B} 赋值语句公理: {0+X*A=A*B and X>=0} Y:=0 {Y+X*A=A*B and X>=0} 赋值语句公理: {0+B*A=A*B and B>=0} X:=B {0+X*A=A*B and X>=0)} 组合公理: {0+B*A=A*B and B>=0} X:=B; Y:=0 {Y+X*A=A*B and X>=0)} 数学定理: (B>=0)  0+B*A=A*B and B>=0 顺序语句公理: {B>=0} X:=B; Y:=0{Y+X*A=A*B and X>=0)} 组合公理: {B>=0} program {Y=A*B}

公理化验证—小结 需要为语言的所有特征建立公理，能否也为简单数组、过程调用、参数等建立公理？ 即使是要证明小程序也很困难，要证明大型程序就更困难了。 还不能很好地处理非数学方面的问题，处理起来极端困难。 很难自动化，而手工又会导致大量错误。 但是 准确，能够清楚地区别“程序是什么”以及“程序是如何解决问题” 它是大多数其他验证方法的基础，包括半形式化的规范表示法。 对于关键应用，付出的代价还是值得的。

程序验证 只有程序正确性的验证过程能够自动化，程序验证才有实际意义 但要证明那些没有结构化的程序、以及那些具有复杂结构的程序的正确性，非常困难，基本上是不可能的。 程序验证工作的研究成果通常用来指导程序设计语言的设计 例如，在C++中加断言等。

ML 概述 ML (元语言) 是一种函数式语言，其程序的形式与 C 或 Pascal 相似。 ML 由 Robin Milner 于1970年代中期开发，是一种机器辅助形式化证明的机制。 ML 也可以作为一种通用符号操纵语言。 1983，该语言中加入了模块等概念，并经过重新设计，形成了现在的标准ML。 ML 是一种具有静态类型、强类型、和函数式执行的语言，但类型不必由程序员来指定。 ML 程序由若干个函数定义构成。每个函数的类型是静态的，函数可以返回任意类型的值。因为是函数型的语言，变量的存储与C或Fortran语言的很不相同。 ML 可以通过其类型系统支持多态，还支持数据抽象。

ML 程序例子 1 fun digit(c:string):int = ord(c)-ord("0"); 2 (* Store values as a list of characters *) 3 fun SumNext(V) = if V=[ ] then (print("\n Sum="); 0) 4 else (print(hd(V)); 5 SumNext(tl(V))+digit(hd(V))); 6 fun SumValues(x:string):int= SumNext(explode(x)); 7 fun ProcessData() = 8 (let val infile = open_in("data.sml"); 9 val count = digit(input(infile,1)) 10 in 11 print(SumValues(input(infile,count))) 12 end; 13 print("\n"));

把一个列表颠倒过来的函数 datatype list [a, b, c, d, e] hd(x)：列表的头，或第一个元素 tl(x)：列表的尾，或除第一个元素外的元素 x::y 表示头为 x，尾为 y 的列表 x@y 表示连接列表 x 和 y fun reverse(L) = if L = nil then nil else reverse(tl(L)) @ [hd(L)]; 目标：将颠倒列表变成一个更简单的函数： 列表要么是空的，否则，对表头和表尾进行处理 将表尾颠倒，然后把表头连到后头。

ML 模式匹配 上面的函数也可以写成： fun reverse(x::y) = reverse(y) @ [x] 在这个格式中，模式匹配就是寻找可以运用的函数定义： 如果列表不为空，则匹配 x::y； 否则，匹配 [ ]。

ML 的类型 列表 Lists: [a, b, c, d, e]  所有的元素具有相同的类型 元组 Tuples: (“a”, 1, 2.3)  简化的静态记录 记录 Records: {1=“a”, 2=1, 3=2.3}  给出了选择子的名字 构造动态的任意结构： datatype money = penny | nickel | dime; val x = penny;  为常量设定值 零钱的记录： datatype change = coins of money * int; coins(penny,3)  类型为 change 的对象 构造函数处理零钱： fun NumPennies(coins(penny,x)) = x; val x = coins(penny, 5); NumPennies(x); val it = 5: int;

ML 的结构 硬币袋（Bags of coins）: datatype coinbag = bag of coinbag * coinbag | item of change | empty; fun Valuechange(coins(penny,X)) = X | Valuechange(coins(nickel,X)) = 5* X | Valuechange(coins(dime,X)) = 10* X; fun Countchange(bag(X,Y)) = Countchange(X)+Countchange(Y) | Countchange(item(X)) = Valuechange(X) | Countchange(Empty) = 0; 函数的使用： val x=bag(item(coins(dime,3)),item(coins(nickel,7))); Countchange(x); val it = 65 : int