1、第四章第四章 程序语言的性质程序语言的性质1语言的形式化模型语言的形式化模型nBNF为描述程序设计语言的属性提供了一种很为描述程序设计语言的属性提供了一种很好的手段，但并不是充分的手段。好的手段，但并不是充分的手段。BNF回答了回答了程序看起来象什么，但没有回答程序是做什么程序看起来象什么，但没有回答程序是做什么的。的。n形式化模型采用精确的数学模型来刻画研究对形式化模型采用精确的数学模型来刻画研究对象，为研究、分析和操纵研究对象提供严谨的象，为研究、分析和操纵研究对象提供严谨的数学工具和手段。数学工具和手段。n本章将介绍下列形式化模型：本章将介绍下列形式化模型：n形式文法：乔姆斯基文法分级形
2、式文法：乔姆斯基文法分级n语言的语义语言的语义：属性文法属性文法、指称语义指称语义n程序的验证程序的验证24.1 语言的形式化性质语言的形式化性质n乔姆斯基分级文法乔姆斯基分级文法n语言的能力语言的能力3乔姆斯基分级文法乔姆斯基分级文法n文法文法n由非终结符、终结符、开始（非终结）符、由非终结符、终结符、开始（非终结）符、及产生式构成及产生式构成n文法的类别文法的类别n3型文法：正则文法，定义词法的模型型文法：正则文法，定义词法的模型n2型文法：型文法：BNF文法，上下文无关文法文法，上下文无关文法n1型文法：上下文有关文法型文法：上下文有关文法n0型文法：型文法：43型文法：正则文法型文法：
3、正则文法n为词法分析器提供模型。为词法分析器提供模型。n这类文法的大多数性质都是可判定的这类文法的大多数性质都是可判定的n如，能产生什么样的串、给定串是否属于文法规如，能产生什么样的串、给定串是否属于文法规定的语言、语言中的串是否有限等定的语言、语言中的串是否有限等n正则文法可以产生形如正则文法可以产生形如an的串，其中的串，其中a为有为有限字符序列限字符序列n正则文法只能计数有限数正则文法只能计数有限数n常用于关键字或单词扫描常用于关键字或单词扫描52型文法型文法上下文无关文法上下文无关文法n产生式的形式为：产生式的形式为：X ,其中其中 可以是终结符可以是终结符和非终结符的任意序列和非终结
4、符的任意序列n同样，这类文法的大多数性质都是可判定的同样，这类文法的大多数性质都是可判定的n如，能产生什么样的串、给定串是否属于文法规定的语言、如，能产生什么样的串、给定串是否属于文法规定的语言、语言是否为空等语言是否为空等n可用来计数和比较两个项，产生形如可用来计数和比较两个项，产生形如ancbn的串的串n可以用堆栈来实现可以用堆栈来实现n可用来自动产生程序的语法分析树可用来自动产生程序的语法分析树n2型和型和3型文法的相关问题都已基本上得到解决型文法的相关问题都已基本上得到解决61型文法型文法上下文有关文法上下文有关文法n产生式的形式为：产生式的形式为：,其中其中 任意非终结符任意非终结符
5、串，串，是终结符和非终结符的任意序列，但是终结符和非终结符的任意序列，但 中的符号个数应不多于中的符号个数应不多于 的符号个数的符号个数n从开始符开始导出的串的长度是递增的从开始符开始导出的串的长度是递增的n在生成串时，需要使用固定数量的存储空间，例如在生成串时，需要使用固定数量的存储空间，例如识别上下文无关文法无法识别的串识别上下文无关文法无法识别的串ancnbnn上下文有关文法太复杂，很难用于程序设计语言上下文有关文法太复杂，很难用于程序设计语言n人们对上下文有关文法的很多特征还不太清楚人们对上下文有关文法的很多特征还不太清楚70型文法型文法非限定型文法非限定型文法n对产生式的形式对产生式
6、的形式 没有任何限制没有任何限制n可用来识别任意可计算的函数可用来识别任意可计算的函数n其大多数性质都是不可判定的其大多数性质都是不可判定的返回8不可判定性不可判定性n不同类型的文法越来越复杂，产生的语不同类型的文法越来越复杂，产生的语言也越来越复杂，但是否说明计算机解言也越来越复杂，但是否说明计算机解决问题的能力可以越来越强，没有限制？决问题的能力可以越来越强，没有限制？n例如：能否编写一个例如：能否编写一个C语言程序来判断另一语言程序来判断另一个个C语言程序能否结束？语言程序能否结束？n但这基本上是不可能的，这不是编程人员的但这基本上是不可能的，这不是编程人员的问题，而是因为问题，而是因为
7、计算机所基于的数学模型计算机所基于的数学模型本本身的局限性而导致的。身的局限性而导致的。9图灵机图灵机n一般来说，用一种语言编写的程序也可以用其一般来说，用一种语言编写的程序也可以用其他另一种语言来实现。他另一种语言来实现。n那么是否存在某个程序，只能用某种语言来实那么是否存在某个程序，只能用某种语言来实现，而用其他语言就无法实现？现，而用其他语言就无法实现？n如果没有，那么有哪些程序是其它程序设计语言无如果没有，那么有哪些程序是其它程序设计语言无法表示的，为什么还需要那么多种不同的语言？法表示的，为什么还需要那么多种不同的语言？n如果我们将能够表示所有计算的语言都称为通用语如果我们将能够表示
8、所有计算的语言都称为通用语言，那么是不是所有语言都是通用语言？如果是，言，那么是不是所有语言都是通用语言？如果是，是否存在更简单的通用语言？是否存在更简单的通用语言？10图灵机的结构图灵机的结构n图灵机是一种用来定义可计算函数的抽图灵机是一种用来定义可计算函数的抽象计算机象计算机n图灵机只有一个单一的数据结构，即一个称图灵机只有一个单一的数据结构，即一个称为为“带子带子”的可变长线性数组的可变长线性数组n带子被分为很多格，每格上只包含一个字符带子被分为很多格，每格上只包含一个字符n图灵机还有一个指针变量，称为图灵机还有一个指针变量，称为“读出头读出头”，它总是指向带子上的某个格。它总是指向带子
9、上的某个格。11图灵机的操作图灵机的操作n图灵机只提供几个简单的操作：图灵机只提供几个简单的操作：n读出头所指定位置的字符可以被读出或被修读出头所指定位置的字符可以被读出或被修改。程序可以根据读出的值进行转移。改。程序可以根据读出的值进行转移。n读出头可以左右移动。如果读出头移动到带读出头可以左右移动。如果读出头移动到带子的最末端，则自动在带子上加上一格，并子的最末端，则自动在带子上加上一格，并赋予一个空字符作为初始值。赋予一个空字符作为初始值。12图灵机的运行图灵机的运行n图灵机开始运行时，带子上存放输入数图灵机开始运行时，带子上存放输入数据，读出头指向输入数据的最左端的字据，读出头指向输入
10、数据的最左端的字符；符；n图灵机根据预先编好的操作序列读写带图灵机根据预先编好的操作序列读写带子上的数据、或移动读出头；子上的数据、或移动读出头；n如果最终能够停机，则带子上的内容就如果最终能够停机，则带子上的内容就是最后的输出结果。是最后的输出结果。13图灵机的能力图灵机的能力n任意可计算函数都可以用图灵机计算出任意可计算函数都可以用图灵机计算出来（来（Church论题）论题）n图灵机等价于图灵机等价于0型文法型文法n确定型图灵机等价于非确定型图灵机。确定型图灵机等价于非确定型图灵机。14停机问题停机问题n是否存在某个通用的算法，它能够断定任意给是否存在某个通用的算法，它能够断定任意给定的图
11、灵机在任意的输入下能否停机？定的图灵机在任意的输入下能否停机？n停机问题是不可判断的，即不存在这样的通用算法。停机问题是不可判断的，即不存在这样的通用算法。n任意一个不可判断的问题，都等价于停机问题。任意一个不可判断的问题，都等价于停机问题。n结论：结论：n任何一种程序设计语言都可能代替其它语言任何一种程序设计语言都可能代替其它语言n程序设计语言不存在质的区别，只有量的区别，如程序设计语言不存在质的区别，只有量的区别，如是否优美、易用、高效等是否优美、易用、高效等n任何一种程序设计语言都有它存在的理由任何一种程序设计语言都有它存在的理由返回154.2 语言的语义语言的语义n程序设计语言基本上都
12、是以上下文无关文法(特别是 LR(k)文法)的核心设计的。n但语法分析已经不再是人们感兴趣的研究问题了。n现在的问题是如何确定程序的含义（即语义）。16语言的语义语言的语义n语言的手册必须定义语言中每个结构的含义，包括单语言的手册必须定义语言中每个结构的含义，包括单独结构的含义以及和其他结构组合时的含义。独结构的含义以及和其他结构组合时的含义。n语言提供了不同结构，用户（为了写正确的程序，预语言提供了不同结构，用户（为了写正确的程序，预测语句的执行效果）和实现者（正确地实现语言）需测语句的执行效果）和实现者（正确地实现语言）需要这些结构的精确定义。要这些结构的精确定义。n大多数语言中，形式文法
13、用于定义语法，一段文字或大多数语言中，形式文法用于定义语法，一段文字或例子用于定义语义，但定义是不精确的，有二义性，例子用于定义语义，但定义是不精确的，有二义性，不同作者可能有不同理解。不同作者可能有不同理解。n语义定义问题还是理论研究的目标，但至今没有令人语义定义问题还是理论研究的目标，但至今没有令人满意的解答。满意的解答。n已有各种形式方法用于语义定义。已有各种形式方法用于语义定义。17语义建模（语义建模（1）文法模型文法模型n对定义语言的对定义语言的BNF文法进行扩展，给出文法进行扩展，给出程序的语法分析树，从树中抽取出附加程序的语法分析树，从树中抽取出附加信息。属性文法便是抽取附加信息
14、的一信息。属性文法便是抽取附加信息的一种方式。种方式。18语义建模（语义建模（2）命令或操作模型命令或操作模型n定义程序如何在某虚拟机上执行。通常定义程序如何在某虚拟机上执行。通常描述为一自动机，但比语法用的简单自描述为一自动机，但比语法用的简单自动机远为复杂。动机远为复杂。n自动机有内部状态自动机有内部状态对应程序执行时对应程序执行时的内部状态，包括所有变量的值、执行的内部状态，包括所有变量的值、执行程序本身、以及各种系统定义的数据结程序本身、以及各种系统定义的数据结构。构。19语义建模（语义建模（2）命令或操作模型命令或操作模型n一组形式定义的操作用于刻划自动机内部状态如何改一组形式定义的
15、操作用于刻划自动机内部状态如何改变。此外还需定义程序文本如何翻译成自动机的初始变。此外还需定义程序文本如何翻译成自动机的初始状态。状态。n语言的操作定义对语言如何实际执行给出了相当直接语言的操作定义对语言如何实际执行给出了相当直接的抽象。的抽象。n也可能提出一个更抽象的模型，作为语言的软件解释也可能提出一个更抽象的模型，作为语言的软件解释的基础。的基础。n70年代的年代的VDL（Vienna Definition Language）是是一个操作方法。一个操作方法。n它扩展语法分析树已包含机器解释器。它扩展语法分析树已包含机器解释器。n计算的状态是程序树加上描述机器中所有数据的树。计算的状态是程
16、序树加上描述机器中所有数据的树。n每条语句的执行使树的状态发生变化。每条语句的执行使树的状态发生变化。20语义建模（语义建模（3）作用型模型作用型模型n试图直接构造每个程序的函数的定义，采用层次式的试图直接构造每个程序的函数的定义，采用层次式的构造方式。构造方式。n程序中每个基本的或程序员定义的操作代表一个数学程序中每个基本的或程序员定义的操作代表一个数学函数。函数。n语言的程序控制结构用于将这些函数复合为更大的序语言的程序控制结构用于将这些函数复合为更大的序列，代表表达式和语言。列，代表表达式和语言。n语句序列和条件分叉表示为个体函数构造而成的函数。语句序列和条件分叉表示为个体函数构造而成的
17、函数。n循环通常表示为递归函数。循环通常表示为递归函数。n最终，为整个程序导出一个完整的函数模型，指称语最终，为整个程序导出一个完整的函数模型，指称语义归于此类。义归于此类。21语义建模（语义建模（4）公理模型公理模型n使用谓词演算，每个语法结构的语义被描述为使用谓词演算，每个语法结构的语义被描述为公理或推导规则，用于导出结构的执行效果。公理或推导规则，用于导出结构的执行效果。n从一个初始假设开始，从一个初始假设开始，n假设输入变量满足一定的约束，假设输入变量满足一定的约束，n在程序语句执行后，使用公理和推导规则来推导其在程序语句执行后，使用公理和推导规则来推导其他变量值需满足的限制，他变量值
18、需满足的限制，n最终，程序的结果被证明满足希望的约束（描述了最终，程序的结果被证明满足希望的约束（描述了它们的值和输入值的关系）。它们的值和输入值的关系）。n如如Hoare的公理语义。的公理语义。22语义建模（语义建模（5）规约模型规约模型n描述实现程序的各个函数的关系，只要描述实现程序的各个函数的关系，只要我们可以证明一个实现符合了所有的函我们可以证明一个实现符合了所有的函数间的关系，则称实现相对于规约是正数间的关系，则称实现相对于规约是正确的。确的。n代数数据类型是形式规约的一种形式。代数数据类型是形式规约的一种形式。n例如：实现栈的程序，例如：实现栈的程序，S表示栈，则有公理，表示栈，则
19、有公理，npop(push(S,x)=Sn任何一个实现如果能保持这种关系，则称是任何一个实现如果能保持这种关系，则称是栈的正确实现。栈的正确实现。23语义模型语义模型小结小结n上述各种形式语义模型各有优点，但均上述各种形式语义模型各有优点，但均不能称为完全实用的和适用的，各有其不能称为完全实用的和适用的，各有其适合范围。适合范围。n操作语义为语言的实现提供了一种形式模型，操作语义为语言的实现提供了一种形式模型，但对用户来说太细节但对用户来说太细节n公理语义易于理解，但很难用来定义复杂的公理语义易于理解，但很难用来定义复杂的程序设计语言，且缺乏对语言实现的支持程序设计语言，且缺乏对语言实现的支持
20、返回24语义建模语义建模属性文法属性文法n这是最早的开发语义模型的工作之一。这是最早的开发语义模型的工作之一。n其思想是对分析树中的每个结点关联一个函数，从而其思想是对分析树中的每个结点关联一个函数，从而给出结点的语义内容。给出结点的语义内容。n属性文法的创建过程是为文法中的每一条规则都定义属性文法的创建过程是为文法中的每一条规则都定义相关的语义函数。相关的语义函数。n继承属性继承属性是一个函数，它将树中非终结符值和树中更是一个函数，它将树中非终结符值和树中更高层的非终结符值相关联。换言之，任何规则右端的高层的非终结符值相关联。换言之，任何规则右端的非终结符的函数值是左端非终结符的函数。非终结
21、符的函数值是左端非终结符的函数。n综合属性综合属性是一个函数，它将左端非终结符和右端非终是一个函数，它将左端非终结符和右端非终结符的值相关联，这些属性在树中向上传递信息，即结符的值相关联，这些属性在树中向上传递信息，即从树中下层信息进行从树中下层信息进行“综合综合”。25属性文法属性文法n例：考虑算术表达式的简单文法。例：考虑算术表达式的简单文法。ET|E+TTP|TPPI|(E)n其语义通过文法中非终结符间的关系集合定义。如：其语义通过文法中非终结符间的关系集合定义。如：下面函数生成该文法生成的任意表达式的值：下面函数生成该文法生成的任意表达式的值：产生式产生式属性属性EE+TValue(E
22、1)=V(E2)+V(T)ETV(E)=V(T)TTPV(T1)=V(T2)V(P)TPV(T)=V(P)PIV(P)=数数I的值的值P(E)V（P）=V（E）26属性文法属性文法n下图是一个属下图是一个属性树，它给出性树，它给出了表达式了表达式2+4(1+2)值值 27属性文法属性文法n属性文法可用于在语法树中传递语义信息。例如，声属性文法可用于在语法树中传递语义信息。例如，声明信息可以通过语言的声明产生式收集。沿树向下传明信息可以通过语言的声明产生式收集。沿树向下传的符号表信息可用于生成表达式代码。的符号表信息可用于生成表达式代码。n下面属性可加到非终结符下面属性可加到非终结符和和来创建一
23、个程序中声明的名字集合。来创建一个程序中声明的名字集合。产生式产生式属性属性:=decl_set(declaration1)=declaname(decl)decl_set(declaration2):=decl_set(declaration)=decl-name(decl):=declare xdecl-name(decl)=x(decl):=declare ydecl-name(decl)=y(decl):=declare zdecl-name(decl)=zn这是综合属性，包含程序中声明的名字集合。该属性这是综合属性，包含程序中声明的名字集合。该属性可以沿树向下传递，成为继承属性，用于
24、正确地生成可以沿树向下传递，成为继承属性，用于正确地生成数据的代码。数据的代码。28属性文法的使用属性文法的使用n首先创建语法分析树。属性文法假设你已经知道表达首先创建语法分析树。属性文法假设你已经知道表达式是如何推导出来的，它并不关心是如何分析推导出式是如何推导出来的，它并不关心是如何分析推导出来的。来的。n定义属性的函数可以是任意给定的，因此定义属性的定义属性的函数可以是任意给定的，因此定义属性的过程完全是手工完成的。过程完全是手工完成的。n如果只有综合属性，并且文法是如果只有综合属性，并且文法是 LR(k)，那么，属性，那么，属性文法可以用来在语法分析时自动产程中间代码。文法可以用来在语
25、法分析时自动产程中间代码。n这就是这就是 YACC 如何工作的，它利用属性文法来计算所如何工作的，它利用属性文法来计算所有非终结符的值。有非终结符的值。n在构造分析树时，非终结符的信息逐层向上传递给分析树上在构造分析树时，非终结符的信息逐层向上传递给分析树上层的非终结符。层的非终结符。n语法分析完毕，所有属性的值将计算出来。语法分析完毕，所有属性的值将计算出来。返回返回29指称语义指称语义n指称语义是一种用来描述程序设计语言指称语义是一种用来描述程序设计语言的语义的作用型语义模型的语义的作用型语义模型n指称语义基于指称语义基于-演算演算30-演算演算n-演算是一种和图灵机的计算能力相当演算是一
26、种和图灵机的计算能力相当的理论计算模型的理论计算模型n-演算可以作为程序设计语言的函数调演算可以作为程序设计语言的函数调用的模型用的模型nAlgol和和Lisp都采用来都采用来-演算的函数调用语演算的函数调用语义义n指称语义是对指称语义是对-演算的扩充，它将演算的扩充，它将-演演算扩充为一种通用的数据类型理论算扩充为一种通用的数据类型理论31-演算的表达式演算的表达式n-表达式可以递归地定义如下：表达式可以递归地定义如下：n变量名为变量名为-表达式表达式n如果如果M为一个为一个-表达式，则表达式，则 x.M也是一个也是一个-表达式表达式n如果如果F和和A都是都是-表达式，则表达式，则(F A)
27、也是也是-表达式，表达式，其中其中F为操作符，为操作符，A为操作数。为操作数。n形式语法：形式语法：-expr:=id|id.-expr|(-expr -expr)n x相当于申明参数变量相当于申明参数变量x，没有申明的变量为自由变量，没有申明的变量为自由变量，否则为约束变量。否则为约束变量。n x.M相当于函数申明，其中相当于函数申明，其中x相当于相当于M的参数。的参数。n例如：例如：x x.x x.(xy)x.y (x.x y.y)32-表达式的操作表达式的操作n-表达式只有一种操作：约简表达式只有一种操作：约简n(F A)约简相当于将约简相当于将A作为实际参数，替换作为实际参数，替换F的
28、形式的形式参数的所有出现参数的所有出现n(x.M A)M，相当于用相当于用A替换替换M中中x的所有自由出现。的所有自由出现。n例如：例如：n(x.x y)yn(x.(xy)x.x)x.x y yn注意：约简并不一定能简化原来的注意：约简并不一定能简化原来的 表达式表达式n(x.(xx)x.(xx)(x.(xx)x.(xx)33指称语义指称语义n指称语义的基本思想是定义一个语义函数（指指称语义的基本思想是定义一个语义函数（指称函数），把程序的意义映射到某种意义清晰称函数），把程序的意义映射到某种意义清晰的数学对象（就像用中文解释英文）的数学对象（就像用中文解释英文）n作为被指的数学对象可以根据需
29、要选择作为被指的数学对象可以根据需要选择n对于简单的程序语言，一种很自然的选择是把对于简单的程序语言，一种很自然的选择是把程序的语义定义为（指称为）从状态到状态的程序的语义定义为（指称为）从状态到状态的函数。定义语义就是定义好每个程序对应的函函数。定义语义就是定义好每个程序对应的函数。数。n程序的状态由标识符到值的映射集合构成程序的状态由标识符到值的映射集合构成S=id|value,34指称语义指称语义n表达式的语义表达式的语义ne S valn语句的语义语句的语义ns S Sn程序的语义程序的语义nm val val35指称语义指称语义n设设 为程序的当前状态为程序的当前状态n表达式的语义表
30、达式的语义n常数：常数：n =nn变量：变量：x =(x)n算术表达式：算术表达式：e1+e2 =e1 +e2 n语句的语义语句的语义n赋值语句：赋值语句：x=e =x|e n复合语句：复合语句：s1;s2 =s2(s1)n条件语句：条件语句：if b then s1 else s2 =if b then s1 else s2 n程序的语义程序的语义nm val val返回36程序验证程序验证n在编程时，人们越来越关心程序的正确性和可在编程时，人们越来越关心程序的正确性和可靠性。人们在设计程序设计语言时，也希望通靠性。人们在设计程序设计语言时，也希望通过增加新的特征来增强程序的正确性和可靠性。
31、过增加新的特征来增强程序的正确性和可靠性。n我们可以用程序语义，按以下方式来探讨程序我们可以用程序语义，按以下方式来探讨程序的正确性问题：的正确性问题：n给定程序给定程序P，其含义是什么？即，它的规范描述其含义是什么？即，它的规范描述S是是什么？什么？n给定规范描述给定规范描述S，开发实现了该规范描述的程序开发实现了该规范描述的程序Pn规范描述规范描述S和程序和程序P是否完成了相同的功能（执行了是否完成了相同的功能（执行了相同的函数）？相同的函数）？相当于语义建模问题软件工程的核心问题程序验证的核心问题37程序验证程序验证n测试不能保证程序的正确性测试不能保证程序的正确性n如果能找到不依赖于测
32、试的保证程序正如果能找到不依赖于测试的保证程序正确性的方法，产生的程序就能更加可靠：确性的方法，产生的程序就能更加可靠：n程序计算了一个函数程序计算了一个函数n如果能给出该函数的规范描述，并且能够根如果能给出该函数的规范描述，并且能够根据程序知道它到底计算了一个什么样的函数，据程序知道它到底计算了一个什么样的函数，那么，如果能够证明程序所计算的函数与给那么，如果能够证明程序所计算的函数与给定的函数等价或相同，就能证明程序的正确定的函数等价或相同，就能证明程序的正确性，而不需再测试。性，而不需再测试。38形式化的规范描述形式化的规范描述n任一程序都可以表示成流程图任一程序都可以表示成流程图基调：
33、函数名：定义域基调：函数名：定义域 值域值域n fun1:S1 and P1 S3n fun2:S1 and not(P1)S3n fun3:S3 and not(P3)S4n fun4:S3 and P3 S4n S2 and P2=S4n S2 and not(P2)=S3P1P2P3 Fcn1Fcn4Fcn3Fcn2S1S2S3S439形式化的规范描述（续）形式化的规范描述（续）n这样，程序可以看成是一个定义在其基本成分上的这样，程序可以看成是一个定义在其基本成分上的复杂函数：复杂函数：C(fun1,fun2,fun3,fun4,p1,p2,p3):S1 S4n如果我们能够形式化地推导出
34、上述关系，那么我们如果我们能够形式化地推导出上述关系，那么我们就能够从数学上证明，给定就能够从数学上证明，给定S1,程序将终止于状态程序将终止于状态 S4。n但是：证明非常困难。但是：证明非常困难。n另外，在证明时，我们总是想证明程序和某个给定另外，在证明时，我们总是想证明程序和某个给定的形式化规范等价，但问题是，如果没有给出规范的形式化规范等价，但问题是，如果没有给出规范描述，描述，“程序是否正确？程序是否正确？”可能就没有了意义。可能就没有了意义。40公理化验证公理化验证n用谓词逻辑公式来刻画程序的语义、用谓词演算来用谓词逻辑公式来刻画程序的语义、用谓词演算来验证程序的正确性。验证程序的正
35、确性。nTony Hoare 在在1969年提出的。年提出的。n每个程序都遵循某种形式化的公理定义。每个程序都遵循某种形式化的公理定义。n实证（实证（Validation）:通过一系列测试数据的测试，通过一系列测试数据的测试，展示程序满足了其规范描述。展示程序满足了其规范描述。n验证（验证（Verification）:根据程序结构，通过形式根据程序结构，通过形式化的讨论，展示程序满足了其规范描述。化的讨论，展示程序满足了其规范描述。nValidation一般认为需要执行程序，而一般认为需要执行程序，而 verification不需要。不需要。41谓词逻辑公理nP1SP2 表示如果 P1 为真，
36、则在 S 执行并终止后，P2 将为真。n如果 A 为真，则 B 也为真。n逻辑公理：n组合n顺序1nn顺序2BAPS1Q,QS2R 组合语句PS1;S2RPSR,RQ 增加后置条件PSQPR,RSQ 增加前置条件 PSQ42语句类型的公理n条件语句1n条件语句2nWhile循环语句n赋值语句PBSQ,Pnot(B)Q Pif B then SQPBS1Q,Pnot(B)S2Q Pif B then S1 else S2QPBSPPwhile B do SP not(B)，其中 P 为不变式P(e)x:=eP(x)，P(x)为 x 的谓词。43公理化的程序证明公理化的程序证明n给定程序：给定程序
37、：s1;s2;s3;s4;sn n及其规约：及其规约：P 和和 QnP 为前置条件为前置条件nQ 为后置条件为后置条件n通过证明下列的谓词来证明通过证明下列的谓词来证明 Ps1;snQ：nPs1p1np1s2p2n npn-1snQn反复运用组合公理，产生：反复运用组合公理，产生：nPs1;snQ44例子例子B=01X:=B2Y:=03while X0 do4 begin5 Y:=Y+A6 X:=X-17 endY=AB即，给定非负的即，给定非负的 B，证明当程序终止时，证明当程序终止时，Y=A*B.45证明过程概要证明过程概要n一般通过回溯来进行。一般通过回溯来进行。n首先，找到循环的不变式
38、：首先，找到循环的不变式：nY 为乘积的一部分，为乘积的一部分，X 为剩下的乘数为剩下的乘数n因此，因此，Y 和和 X*A 必须是所需的乘机，即不必须是所需的乘机，即不变式变式nY+X*A=A*B 就是建议的不变式就是建议的不变式n可以试着用可以试着用(Y+X*A=A*B and X=0)作为不变式作为不变式 46证明证明n赋值语句公理赋值语句公理(6):(Y+(X-1)A=A*B and X-1=0)X:=X-1(Y+X*A=A*B and X=0)n赋值语句公理赋值语句公理(5):(Y+A)+(X-1)A=A*B and X-1=0)Y:=Y+A(Y+(X-1)*A=A*B and X-1
39、=0)n组合公理组合公理(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)n数学定理数学定理:Y+X*A=A*B and X0 (Y+A)+(X-1)*A=A*B and X-1=0)n顺序语句公理顺序语句公理:Y+X*A=A*B and X0 Y:=Y+A;X:=X-1(Y+X*A=A*B and X=0)n数学定理数学定理:(Y+X*A=A*B and X=0)and(X0)Y+X*A=A*B and X0n顺序语句公理顺序语句公理:(Y+X*A=A*B and X=0)and(X0)Y:=Y+A;X:=X-
40、1(Y+X*A=A*B and X=0)用用*来代替来代替nWhile循环语句公理循环语句公理:*Y+X*A=A*B and X=0while X0 do Y:=Y+A;X:=X-1(Y+X*A=A*B and X=0)and not(X0)47证明证明(续续)n数学定理数学定理:(Y+X*A=A*B and X=0)and not(X0)(Y+X*A=A*B and X=0)Y=ABn顺序语句公理顺序语句公理:Y+X*A=A*B and X=0while X0 do Y:=Y+A;X:=X-1 Y+A*Bn赋值语句公理赋值语句公理:0+X*A=A*B and X=0 Y:=0 Y+X*A=A
41、*B and X=0n赋值语句公理赋值语句公理:0+B*A=A*B and B=0 X:=B 0+X*A=A*B and X=0)n组合公理组合公理:0+B*A=A*B and B=0 X:=B;Y:=0 Y+X*A=A*B and X=0)n数学定理数学定理:(B=0)0+B*A=A*B and B=0n顺序语句公理顺序语句公理:B=0 X:=B;Y:=0Y+X*A=A*B and X=0)n组合公理组合公理:B=0 program Y=A*B48公理化验证公理化验证小结小结n需要为语言的所有特征建立公理，能否也为简单数组、需要为语言的所有特征建立公理，能否也为简单数组、过程调用、参数等建立
42、公理？过程调用、参数等建立公理？n即使是要证明小程序也很困难，要证明大型程序就更即使是要证明小程序也很困难，要证明大型程序就更困难了。困难了。n还不能很好地处理非数学方面的问题，处理起来极端还不能很好地处理非数学方面的问题，处理起来极端困难。困难。n很难自动化，而手工又会导致大量错误。很难自动化，而手工又会导致大量错误。n但是但是n准确，能够清楚地区别准确，能够清楚地区别“程序是什么程序是什么”以及以及“程序是如何解程序是如何解决问题决问题”n它是大多数其他验证方法的基础，包括半形式化的规范表示它是大多数其他验证方法的基础，包括半形式化的规范表示法。法。n对于关键应用，付出的代价还是值得的。对
43、于关键应用，付出的代价还是值得的。49程序验证程序验证n只有程序正确性的验证过程能够自动化，只有程序正确性的验证过程能够自动化，程序验证才有实际意义程序验证才有实际意义n但要证明那些没有结构化的程序、以及但要证明那些没有结构化的程序、以及那些具有复杂结构的程序的正确性，非那些具有复杂结构的程序的正确性，非常困难，基本上是不可能的。常困难，基本上是不可能的。n程序验证工作的研究成果通常用来指导程序验证工作的研究成果通常用来指导程序设计语言的设计程序设计语言的设计n例如，在例如，在C+中加断言等。中加断言等。50ML 概述概述nML(元语言元语言)是一种函数式语言，其程序的形式与是一种函数式语言，
44、其程序的形式与 C 或或 Pascal 相似。相似。nML 由由 Robin Milner 于于1970年代中期开发，是一种机器辅助形年代中期开发，是一种机器辅助形式化证明的机制。式化证明的机制。nML 也可以作为一种通用符号操纵语言。也可以作为一种通用符号操纵语言。n1983，该语言中加入了模块等概念，并经过重新设计，形成了，该语言中加入了模块等概念，并经过重新设计，形成了现在的标准现在的标准ML。nML 是一种具有静态类型、强类型、和函数式执行的语言，但类是一种具有静态类型、强类型、和函数式执行的语言，但类型不必由程序员来指定。型不必由程序员来指定。nML 程序由若干个函数定义构成。每个函
45、数的类型是静态的，函程序由若干个函数定义构成。每个函数的类型是静态的，函数可以返回任意类型的值。因为是函数型的语言，变量的存储与数可以返回任意类型的值。因为是函数型的语言，变量的存储与C或或Fortran语言的很不相同。语言的很不相同。nML 可以通过其类型系统支持多态，还支持数据抽象。可以通过其类型系统支持多态，还支持数据抽象。51ML 程序例子程序例子n 1 fun digit(c:string):int=ord(c)-ord(0);n n 2 (*Store values as a list of characters*)n 3 fun SumNext(V)=if V=then(prin
46、t(n Sum=);0)n 4 else(print(hd(V);n 5 SumNext(tl(V)+digit(hd(V);n n 6 fun SumValues(x:string):int=SumNext(explode(x);n n 7 fun ProcessData()=n 8 (let val infile=open_in(data.sml);n 9 val count=digit(input(infile,1)n 10 in n 11 print(SumValues(input(infile,count)n 12 end;n 13 print(n);52把一个列表颠倒过来的函数把一
47、个列表颠倒过来的函数ndatatype list a,b,c,d,enhd(x)：列表的头，或第一个元素：列表的头，或第一个元素ntl(x)：列表的尾，或除第一个元素外的元素：列表的尾，或除第一个元素外的元素nx:y 表示头为表示头为 x，尾为，尾为 y 的列表的列表nxy 表示连接列表表示连接列表 x 和和 ynfun reverse(L)=if L=nil then nilnelse reverse(tl(L)hd(L);n目标：将颠倒列表变成一个更简单的函数：目标：将颠倒列表变成一个更简单的函数：n列表要么是空的，否则，对表头和表尾进行处理列表要么是空的，否则，对表头和表尾进行处理n将表
48、尾颠倒，然后把表头连到后头。将表尾颠倒，然后把表头连到后头。53ML 模式匹配模式匹配n上面的函数也可以写成：上面的函数也可以写成：nfun reverse(x:y)=reverse(y)x|reverse()=;n在这个格式中，模式匹配就是寻找可以运用的在这个格式中，模式匹配就是寻找可以运用的函数定义：函数定义：n如果列表不为空，则匹配如果列表不为空，则匹配 x:y；n否则，匹配否则，匹配 。54ML 的类型的类型n列表列表 Lists:a,b,c,d,e 所有的元素具有相同的类型所有的元素具有相同的类型n元组元组 Tuples:(“a”,1,2.3)简化的静态记录简化的静态记录n记录记录
49、Records:1=“a”,2=1,3=2.3 给出了选择子的名字给出了选择子的名字n构造动态的任意结构：构造动态的任意结构：ndatatype money=penny|nickel|dime;nval x=penny;为常量设定值为常量设定值n零钱的记录：零钱的记录：ndatatype change=coins of money*int;ncoins(penny,3)类型为类型为 change 的对象的对象n构造函数处理零钱：构造函数处理零钱：nfun NumPennies(coins(penny,x)=x;nval x=coins(penny,5);nNumPennies(x);nval it=5:int;55 结束语当你尽了自己的最大努力时，失败也是伟大的，所以不要放弃，坚持就是正确的。When You Do Your Best,Failure Is Great,So DonT Give Up,Stick To The End谢谢大家荣幸这一路，与你同行ItS An Honor To Walk With You All The Way演讲人：XXXXXX 时 间：XX年XX月XX日
