PL设计概述-程序设计语言原理课件.ppt

《PL设计概述-程序设计语言原理课件.ppt》由会员分享，可在线阅读，更多相关《PL设计概述-程序设计语言原理课件.ppt（61页珍藏版）》请在三一办公上搜索。

1、第1页,第二章 程序设计语言设计概述,2.1 表示与抽象2.2 设计目标2.3 设计准则2.4 规格说明,第2页,2.1 表示与抽象,表示是人为制造的符号组合以表达我们需要表达的意思。程序是程序设计语言表示的计算float n;/n 是浮点数变量sqrt(n);/对n取平方根同一程序的高级语言表示、经翻译后的汇编码表示、机器码表示就是该程序在不同抽象层次上的表示。,第3页,2.1 表示与抽象,程序在不同抽象层次表示的关系例：x=x+1在机器码上就有两种方法。,从内存代表x的地址中取出值放在运算器中。加1，将结果放于某临时单元。将临时单元内容做类型检查（必要时转换）并放入x中。,从内存代表x的地

2、址中取出值放在运算器中。加1，将结果放入x地址中。,第4页,2.1 表示与抽象,儿子10岁女儿8岁母亲35岁几年后儿女岁数之和大于等于母亲？,u=m-s-d,每人每年增1岁每增 一年比较一次，满足 条件即所求。,read(m,s,d);u=m-s-d;print(u),read(m,s,d);u=0;while(m+us+d+2u)u+;print(u);,m,s,d,u,指令集,客观世界问题抽象,模型世界数学模型模拟模型,程序世界以程序世界术语表示描述模型,机器世界以机器的术语实现程序,图2-1 计算机解题的四个世界,第5页,2.2 PL设计目标,定义一组能表示某种范型的特征集，每个特征有严

3、格定义并可在机器上高效实现，程序员可灵活运用这些特征表达它所希望的任何计算。,第6页,语言设计：目标演化,第6页,Fortran 设计中最主要的考虑是易用性（与机器和汇编语言比较）和高效实现，特别关注程序能翻译成高效执行的代码，因为这样才可能被接受（今天Fortran 仍高效）。随着计算机变得越来越快，越来越便宜，效率问题虽然还是很重要，但重要性已大大下降。易用性方面的考虑仍非常明显：提高程序设计工作的效率 帮助人们提高程序（软件）的质量，可靠性 设法支持某些高级的软件设计技术 语言最主要作用是用于描述所需要的计算过程。为此需要：清晰，简洁的形式（例子：C，Pascal，APL）清晰简单的语义

4、（易理解，易验证）正交性（避免重复的可相互替代的特征，人们对此有些不同意见）可读性（人容易阅读理解的东西，计算机也容易处理）,第7页,语言设计：目标演化,第7页,随着程序设计语言的发展，语言的设计目标也发生了很大变化语言的初始设计目标就是更方便地为计算机写程序后来人们认识到，程序设计语言也是人的工具，用于描述算法、交流算法，用于服务于交流、教学和科研的需要随着计算机应用发展，程序变得越来越复杂，开发程序变成代价高昂的工作。为支持复杂程序开发，提高开发工作的效率，语言设计有了许多新目标：支持对基本语言的扩充，提供各种扩充定义和抽象机制，过程、函数定义机制，扩充语言的基本操作，数据类型定义机制（及

5、OO机制），扩充数据描述方式和功能。例：C+在语言机制扩充方面有许多考虑（如运算符重载）可扩充语言（Extendable Languages），允许程序形式的改变（Lisp）,第8页,语言设计：目标演化,第8页,2.提供支持复杂程序所需的高级组织的机制，支持大型程序开发模块机制（信息隔离和屏蔽），支持分别编译的机制，支持程序的物理组织3.支持软件重用，包括软件中的部分的重用，支持通用的基本程序库。Pascal 失败之处之一就是忽略了库的开发。C/Fortran 都做得很好。Ada、C+和Java 的设计都特别考虑了对库的支持。许多新语言定义了功能非常丰富的标准程序库。支持库开发：库是最基本的重

6、用方式。是否支持库开发，决定了语言能否大范围使用。支持用户和第三方供应商开发各种扩充的和专用的库 支持某些层次或者方式的软件部件概念问题：库开发或者部件是否需要本语言之外的功能？OO 概念可能在上面许多方面起作用，因此成为复杂软件开发的重要方法,第9页,语言设计：目标演化,第9页,语言设计中需要考虑的另外一些重要问题：正常处理的异常/错误处理的良好集成（在产品软件的程序里，处理错误和各种特殊情况的代码占很大的比例，可能达70%）对于程序的易修改可维护性的支持 对于并发程序设计的支持，用什么样的机制支持并发程序设计。这方面的问题将长期成为语言研究和设计的热点问题 安全性设计：是否有助于程序员写出

7、安全可靠的程序？这一问题在未来许多年都会是语言设计的一个重要关注点 由于语言承载的功能越来越多，设计时需考虑的问题越来越多，新语言正在变得越来越复杂，语言的实现需要做的工作也越来越多（基本处理、对开发过程的支持、库等等），设计一种语言，支持所有需要变得越来越困难。,第10页,2.2 PL设计目标,定义一组能表示某种范型的特征集，每个特征有严格定义并可在机器上高效实现，程序员可灵活运用这些特征表达它所希望的任何计算。,模型有力 Model Power语义清晰 Semantic Clarity移植性好 Portability可读性好 Readability程序质量 Quality安全性并发,方便

8、Convenience简单 Simplicity高效 Efficiency灵活性 Flexibility可扩充性 Extensible 可重用性 Reusable,第11页,2.3 设计准则,频度准则 越常用越简单 方便、可读结构一致 程序结构和计算的逻辑结构一致 可读、方便局部性 Locality 只有全局变量Basic 不鼓励全局变量Pascal,C 无全局变量函数式 Java词法内聚 Lexical Coherence 变量在使用处就近声明（Pascal声明和语句严格分开）,(lambda(x y)(let(x 3.5)(y(+a 2)(+(*x y)(+(*x y)(-x y)(-x

9、y)3.5(+a 2)x.y.(x*y)+(x-y)3.5(a+2),第12页,续,语法一致性 GO TO(L1,L2,Ln),I I=1.n GO TO N,(L1,L2,Ln)ASSIGN Li TO N N=L1.Ln安全性Security 语言编译系统自动找出安全漏洞，不能弥补也要支持 安全性强类型，即每个计算操作运算之前类型必须确定 C 留给程序员 过程参数不检查 一般不安全,第13页,续,正交性和正规性(Orthogonality&Regularity)正交:每个语言特征都是独立的,增减不影响其它 正规:每一约定或规则无一例外 不正规：数组不能作返回值,不能赋值 函数不能做参数 不

10、正交不正规,第14页,续,数据隐藏(Data hiddening)封装,以名字封装内部数据设计者可见使用者不可见 局部性不一定封装，如：Do l0 I=1,10,2 当I=7时 GOTO 20 10 CONTINUE20.R=I 可以,此时R=7.0,.,第15页,续,抽象表达 抽取因子、递归表达、高层模块名、常量名=常量表达式（易于维护）先抽象再修饰具体（如同自然语言）static const int maxlndex=MAX_LENGTH_1MATHLIB.TRIANG COS(X)可移植性 力图不依赖环境 预定义机制、预处理程序,第16页,形式语法：以形式结构规则的语言元素组合规则微语法

11、 词法 Lexicon宏语法 定义特征的规则,2.4 程序设计语言规格说明语言参考手册,2.4.1 语法规格说明,第17页,第17页,词法和词法分析,构成程序的基本词法元素包括标识符、运算符、字面量、注释等。复杂的词（标识符、各种字面量）需要明确定义的构词法，即词法 处理源程序的第一步是词法分析：编译器处理表示源程序的字符序列，根据词法规则做词法分析，将源程序切分为符合词法的段，识别出源程序的有意义单词（token）词法分析得到一个（表达被分析的源程序的）单词流，流中各单词标明了词法类别（是“标识符”，“整数”，“加号”，“左括号”，等等）词法分析中抛弃所有无保留价值的分隔符（如空白符）和噪声

12、词例：对int main(void)return 0;做词法分析，得到的单词序列是：int main(void)return 0;共10个单词类别：标识符，左/右圆括号，左/右花括号，整数，分号,第18页,第18页,词法分析,词法分析通常采用最长可能原则，确定可能成为单词的最长字符串。例：staticint是一个标识符，而不是关键字static 和intx+y（C语言）的分析结果是：x，+，+，y；而不是x，+，+，yx+y 是x,+,+,+,y（语法错，+的运算对象非左值）早期的Fortran 中存在复杂的词法问题。例如：DO 10 I=1.5 的意思类似于C 语言的DO10I=1.5 而D

13、O 10 I=1,5 是枚举循环头部，类似于C 的for(I=1;I 5;+I).后来的语言都避免了这类问题，保证单词很容易识别（能局部识别）人们已经开发了许多帮助构造词法分析器的自动工具，如lex/flex等,第19页,第19页,语法,语法规定位于词法层次之上的程序结构。例如：表达式的合法形式 基本语句的形式，组合语句的构成方式 更上层的结构，如子程序、模块等的构成形式 语法用于确定一个输入序列是否合法的程序。但什么是“合法”？程序存在多个不同层次的合法性问题：1.局部结构 例：C程序里的if 之后是不是左括号，括号是否配对 2.上下文关系 例：变量使用前是否有定义，使用是否符合类型的要求

14、3.深层问题 例：使用变量的值之前，变量是否已经初始化 语言的语法定义通常只描述1（程序形式中的上下文无关部分）编译程序通常检查条件1和2，有人称2 为“静态语义”,第20页,T是终结符号串的有限集。N是非终结符号串的有限集。TN=，即它们是不相交的。S是起始符号串，SN。P是产生式，一般形式是:，(TN)*“”表示左端可推导出右端，如，则可写为：|如果产生式将语言的非终结符中的每一个标记都推得为终结符号，则这一组产生式集即为该语言的全部文法。,2.4.1.1 文法文法 产生符合语法的语言（句子集合）规则，如：G=(S,N,T,P)SN,TN=*,第21页,整数的产生式表示法：设0|1|2|3

15、|4|5|6|7|8|9则 一位数是整数 两位数也是 n位数也是 n个这势必造成产生式臃肿，如果写成：|,续,第22页,续,Chomsky的四种文法产生式 左符号集右符号集 由左符号集推导出右符号集0型文法(NT)+，(NT)*递归可枚举语言 图灵机可以识别1型文法 A B,(NT)*，AN，B(NT)+上下文相关文法上下文敏感语言 线性有界自动机可识别2型文法 A(NUT)*,AN 上下文无关文法语言 非确定下推自动机可识别,第23页,续,3型文法 ABB T*,A,BN 正则文法 正则语言 有限自动机可以识别 可消除右端非终法符 P可以成为终结符表达式 例：N=S,R,Q,T=a,b,c

16、P=SRa，SQ，RQb，Qc 则有 SRaQbacba|SQc RQbcb Qc 简单语言用 3型，汇编，词法子语言 最常用 2型 0、1型无法判定二义性,不常用,0,1,2,3,第24页,2.4.1.2 上下文无关文法,文法的递归表示法 0123|4|5|6|7|89 一位数 二位数.n 位数 n个 左递归 右递归尾递归,第25页,2.4.1.3 BNF 和EBNF,BNF：:=代替 BNF表达能力同EBNF 指示非终结 终结符直接写出(或黑体)或者有扩充：括号内容是可选的 括号内容可重复0至多次或扩充：C+Kleene加 C可重复1至多次 C*Kleene星 C可重复0至多次,第26页,

17、续,BNF示例:=|:=+|-|:=|,:=+|-:=|:=+:=|,第27页,EBNF：左端取消,空白加-减少递归表示再加(,),.,尽量用正则表达式 终结符号加 号或黑体,续,第28页,续,program:=；.program-heading:=program().program-parameters:=.identifier-list:=，.program-block:=.block:=.variable-declaration-part:=var；.variable-declaration:=；.statement-part:=compound-statement.,第29页,comp

18、ound-statement:=begin end.statement-sequence:=；.statement:=：(|).simple-statement:=|.structured-statement:=|.,续,第30页,2.4.1.4 语法图,同EBNF 取消 以短路表示 以迥环表示,非终结符,走向,复合语句,;,begin,end,语句,终结符,终结符,第31页,2.4.1.5 语法分析,语法规格说明定义了该语言程序合法的特征和语句。语言处理器则通过语法分析接受合法的程序，这就叫做程序释义（Parsing a Program）,释义过程是产生式生成句子的逆过程。,语法分析的算法可

19、归为两类：“自顶向下”释义则从文法的起始符开始，按可能产生的表达式寻找语句相同的结构匹配。每一步都产生下一个可能的源符号串，找到再往下走。“由底向上”释义则相反，它先查找源代码的各个符号串，看它能否匹配归结为产生式左边的非终结符，如果有含混则向前多读入k个符号串，为此归约下去，一个短语一个短语，最后到达起始符号串，归约的过程就形成了释义树。,第32页,begin x：=17；writeIn(x)end,标识符,变量标识符,变量访问,无符号常量,完整变量,无符号数,无符号整数,因子,项,简单表达式,表达式,过程标识符,标识符,变量标识符,完整变量,变量访问,因子,项,简单表达式,表达式,writ

20、e参数,writeln参数表,赋值语句,简单语句,语句,过程语句,简单语句,语句,语句序列,复合语句,第33页,第33页,语法分析是语言翻译过程的一个重要阶段。语法分析技术是“编译原理”或“编译技术”课程的重要内容 本课程不准备详细介绍语法分析的技术，词法分析和语法分析过程并不仅用在编译系统里。许多计算机软件的用户输入都需要做词法分析和简单的语法分析今天的大部分语法分析器都是用工具生成的。例yacc/bison。这些工具接受某种类似BNF 的语法描述，生成对应的语法分析器人们为各种主要语言（C/C+/Java等）开发了支持做词法和语法分析的工具或库，有些脚本语言本身就带有词法/语法分析库，可直

21、接使用,2.4.1.5 语法分析,第34页,第34页,常规的语言编译过程,词法分析,语法分析,语义分析和中间代码生成,与机器无关的优化,目标代码生成,机器特定的优化,第35页,2.4.2 语义定义与规格说明,第35页,语义定义：目标是赋予每个合法的程序一个明确的意义 精确定义程序执行的效果（行为，结果）要求编译程序（等）生成这种效果 写程序的人可以依赖于这种效果，据此写自己的程序语义定义的基本方法是基于语言的语法结构：定义语言中各种基本元素的意义 定义语言中各种语法结构的意义基于相应结构的成分的意义，定义整个结构的意义一些具体情况：表达式的意义是其怎样求值，求出什么值语句的意义是其执行时的产生

22、的效果,第36页,第36页,Algol 60 修订报告 用BNF 定义语言的语法，采用自然语言形式的说明和实例的方式，非形式地定义语言的语义Backus 在讨论Algol 60 时说：现在我们已经有办法严格地定义语言的语法了，希望今后不久就能严格地定义语言的语义。很遗憾，至今的语言手册仍一直沿用上述方式。因为：-语义远比语法复杂，至今计算机工作者还没有开发出一种完美、功 能强大、易理解、易使用，适用于定义一切语言中一切结构的语义 描述方式-但是，对于程序语义的研究已经得到许多成果。有关程序语言语义 的研究是计算机科学的一个重要研究领域,2.4.2 语义定义与规格说明,第37页,1、静态语义：类

23、型的理论,第37页,类型是程序设计语言的一个重要问题程序语言需要有清晰定义的类型系统，以确定程序里-各表达式的类型（typing）。注意，表达式可能嵌套-各语句是否类型良好的（well-typed），或称为良类型的-处理程序中与类型有关的各种问题：类型等价、类型相容、类型转换（自动转换规则，手工转换规则）等有关类型的研究形成了计算机科学中一个重要的研究领域：类型理论,第38页,1、类型环境和类型断言,第38页,类型判断的根据：-每个文字量都有自己的确定类型-变量、函数等的声明提出了相关的类型要求-对类型合适的参数，运算符、函数将给出特定类型的结果（注意：重载的运算符也有运算结果和运算对象之间的

24、关系）类型检查需要知道程序里所有变量的类型信息。当前所有可见变量的类型信息的全体构成了当前的类型环境。一个变量的类型信息用变量名和类型的对表示，如x 具有类型T：类型环境就是这种对的序列，如：下面用（可能加下标）表示类型环境,第39页,1、类型推导,第39页,我们用形式化的记法表示有关类型的断言。类型断言有两种形式：在特定类型环境 下，我们确定了表达式 e 的结果类型是 T（表达式：常量、变量、有结构成分的复杂表达式）在环境 下命令（语句）c 是类型良好的（基本语句如赋 值，各种复合语句和更复杂的程序结构）为了作出程序中各种结构是否类型良好的判断，确定有类型结构（表达式）的具体类型，要定义一套

25、做类型推断的规则（类型规则），说明 如何得到程序中基本表达式的类型 基于表达式的部分的类型推出整个表达式的类型 然后基于表达式的类型，推断基本语句是否类型良好；基于基本语句的良类型性得到复合语句的良类型性 不能推导出类型的表达式是类型错误的表达式，对语句也一样,第40页,1、类型规则,第40页,下面用一个简单语言介绍类型规则的一些定义。假定语言里有int 和double 类型变量声明，赋值语句和结构语句类型规则包括（例子）：基本规则（1）基本规则（2）,第41页,1、类型规则,第41页,表达式的类型规则（一组）：语句的类型规则（一组）：变量声明：其他规则可以类似写出,第42页,2、语义基础：环

26、境和状态,第42页,考虑程序的（动态）语义（程序执行的语义）-希望用清晰严格的方式描述程序执行中各种动作的效果对程序动态行为的理解和严格描述依赖于环境的概念-程序执行过程中存在着一些实体（变量、子程序等）-可能存在与这些实体相关的信息（例如，变量的值，函数的定义）程序里动作的执行可能改变与一些实体相关的信息，如改变变量的值-环境记录与各种有效实体相关的信息-因此，动作的执行可能改变环境讨论语义时关心的是程序的动态环境（运行中的环境）编译（和类型检查）工作中维护的符号表是支持语言处理的“静态环境”最简单的环境模型：从合法名字集合到“值”的映射（是一个有限函数）,第43页,2、环境和状态,第43页

27、,程序执行的动作可能依赖于环境，或导致环境的变化：-需要某变量的值时，从当时环境里取出它的值-一些操作修改环境中变量的值，如赋值、输入等-进入或退出作用域（如进入/退出子程序或内部嵌套的复合语句）可能改变当前有定义的变量集合（改变环境的定义域）-程序开始运行前，需要建立一个初始全局环境，其中包含着所有具 有全局定义的名字及与之相关的默认信息下面把环境建模为变量名到其取值的简单的有限函数-如果研究的是更复杂的语言，这种简单形式就可能不够了，需要考虑更复杂的环境模型-例如包含指针和动态存储分配/释放，或面向对象的语言（OO 语言），就需要为更复杂的环境模型 在程序运行中，当时环境中所有可用变量的取

28、值情况构成了运行时的状态,第44页,2、环境和状态,第44页,例：设当时环境中可见的变量是x,y,z，取值情况是x 取值3，y 取值5，z 取值0这个状态就是有限函数：随着程序的执行，特别是赋值语句的执行，环境的状态就可能改变 经过给x 赋值4，给y 赋值1 的两个操作，状态将变成：理解一个（或一段）程序的意义，就是理解它在有关环境下的意义，以及它的执行对环境的作用,第45页,2、环境和状态,第45页,严格些说，一个环境是一个“部分函数”：为描述状态变化，在环境上定义了一种覆盖操作：例：,第46页,2、环境和状态,第46页,对于常量（如整数），任何环境都给出它们的字面值环境确定一组变量的值，就

29、确定了基于这些变量构造的表达式的意义假定我们有：对于一般表达式：由于环境可以确定表达式的意义（确定表达式的值）。我们也可以把环境看成从合法表达式到值集合的映射，有些表达式的值无定义，例如其中出现了在环境取值为无定义的变量，或者求值中出现无定义运算结果（如除数为0）等,第47页,3、语义规格说明,第47页,我们把程序的意义定义为它们对环境的作用。为定义语义需要：-定义基本语句的意义-定义各种结构的意义如何由它们的组成部分得到有了这些定义，就可以确定由这些语言结构构成的复杂程序的意义一个程序的执行导致环境的变化，问题是如何严格定义这种变化人们提出了多种不同的形式化的语义定义方式（技术）：操作语义：

30、把程序运行看成执行了一系列改变环境的操作，用一组描述环境变化的规则定义程序中各种结构的意义公理语义：用谓词描述状态，用公理和推理规则描述各种基本操作和组合结构的语义指称语义：把程序的意义映射到某种的数学结构，这种结构能清晰地表达程序对环境的作用和环境的变化代数语义：考虑程序之间的等价关系，间接定义程序的意义,第48页,操作语义：格局和规则,第48页,首先需要定义格局（configuration）。这里定义两种格局：终止格局，就是一个环境，表示代码运行完成时的状态 非终止格局：表示程序运行中的一个“状态”一段程序代码（待执行代码段）和一个环境结构化操作语义（SOS）用一组格局变迁规则定义语言的语

31、义。可能包括一些无前提的规则和一些有前提的规则赋值语句的语义规则（无前提规则）：复合语句的语义规则（有前提规则）：,第49页,操作语义：续,第49页,if 条件语句的语义规则（两条）：while 循环语句的语义规则（两条）：上面这组规则严格地定义了一个理想的小语言的语义注意这个小语言的特点。它与实际的程序语言还是有很大差距,第50页,第50页,公理语义,R.Floyd 在1967年考虑如何说明一个程序完成了所需工作时，提出用逻辑公式描述程序环境的状态的思想。这种描述环境的逻辑公式称为断言逻辑公式：描述了状态：说明环境满足公式，实际上，这个状态还满足另外的许多逻辑公式，如：反过来看，一个逻辑公式

32、可以被许多状态满足因此可以认为，一个公式描述了一个状态集合。例如，上面第二个公式，描述了所有的其中x 值是1 的环境,第51页,第51页,公理语义：断言,把断言写在程序里某个特定位置，就是想提出一个要求：-程序执行到这个位置，当时的环境状态必须满足断言-如果满足，程序就正常向下执行（就像没有这个断言）-如果不满足，程序就应该（非正常地）终止实例：C 语言标准库提供了断言宏机制，可以在程序里的写assert(x 0);Stroustrup 在The C+Programming Language里特别讨论了如何 定义断言类的问题 有些语言本身提供了断言机制，如Eiffel。见Design by C

33、ontract,中译本：邮电出版社断言的概念在实际程序开发中起着越来越重要的作用,第52页,第52页,公理语义：前条件和后条件,如何借助于逻辑公式描述一段程序的意义？Hoare 提出的方法是用一对公式，放在相应程序段之前和之后，分别称为该程序段的前条件（precondition）和后条件（postcondition）pre P post意思是：如果在程序P 执行之前条件pre 成立（当时的环境满足pre），那么在P 执行终止时的环境中，条件post 一定成立我们可以用一对公式(pre,post)描述一段程序的语义，也可以把这样的公式对(pre,post)看作是对一段程序的语义要求，看作程序的规

34、范前后条件的两种基本用途：作为评判程序是否正确的标准 作为待开发的程序的规范，研究如何从这种规范得到所需的程序,.,第53页,第53页,公理语义：不变式,不变式（不变量，invariant）的概念在许多领域中有重要地位 程序理论中的不变式，指写在程序里特定位置的逻辑公式，要求程序执执行中每次达到某个（某些）情况时，这个公式都必须成立 其实，不变式并不特殊，因为写在程序里的断言，也就是位于代码中相应特定位置的不变式，“情况”就是执行达到这个位置程序理论里最重要的不变式之一是循环不变式（loop invariant），要求一个循环的每次迭代开始之前成立，在描述和推导程序的意义时有特殊价值直接插入排

35、序算法两重循环的不变式（图示）：,第54页,第54页,Floyd 最早提出用断言描述程序的意义，通过逻辑推导证明程序的正确性。他称自己提出的方法为“断言法”。基本方法：-在流程图程序里的每条边上放一条断言-设法证明从一个动作框的入边上的断言出发，执行相应动作产生的效 果能保证该动作框的出边上的断言成立-对分支控制框也有特殊的规则（请自己考虑）-如果对每个动作框都能证明上述事实成立，那么标注在流程图中各条 边上的断言就形成了该程序的一个（一套）语义描述-特别的，标在程序入口和出口上的断言表示了这段程序的整体效果Hoare 总结了Floyd 的工作，针对结构化的程序控制结构提出了一套逻辑推理规则，

36、这就是有名的Hoare 逻辑,公理语义：程序的意义,第55页,第55页,公理语义：Hoare逻辑,Hoare 逻辑是对有关程序意义的逻辑描述的整理和系统化Hoare 逻辑中的逻辑公式形式为（称为Hoare 三元组）：p S q其中p 和q 是谓词逻辑公式，S 是一段程序直观意义：如果在S 执行之前公式p 成立，在S 执行终止时q 就成立Hoare 的最重要贡献是提出了一套推理规则，通过这些规则，可以把证明一个Hoare 公式（程序S 相对于p 和q 的正确性）的问题归结为证明一组普通一阶谓词逻辑公式的问题Dijkstra 在此基础上提出了最弱前条件（weakest precondition）的

37、概念，借助于这一概念，可以 把程序的正确性证明工作进一步规范化 用于做程序的推导（从规范出发推导程序）,第56页,第56页,公理语义：Hoare逻辑,公理：,规则LOOP 里的I 是循环不变式,第57页,第57页,公理语义：Hoare逻辑,可以用Hoare 逻辑证明程序的正确性，也就是说，证明三元组中的程序语句“符合”前后条件的要求。其意义是：若在前条件满足的情况下执行语句且语句执行终止，那么后条件满足 这个证明并不保证语句终止，如果语句的执行不终止，什么后条件都可以证明。因此，这样证明的正确性称为“部分正确性”程序终止性需要另外证明，主要是需要证明其中循环的执行必然终止 如果同时证明程序的部

38、分正确性和终止性，这一程序就是“完全正确的”程序正确性证明中的一个关键点是为各个循环提供适当的不变式 就像做数学归纳法证明中需要合适的归纳假设，过强或过弱都不行人们已证明，循环不变式不可能自动生成（无完全的算法，但有许多研究）公理语义为我们提供了许多有助于理解程序行为的概念，为设计程序时思考其行为提供了重要的依据和线索。,第58页,第58页,指称语义,指称语义学（denotational semantics）有坚实的数学基础，它的基本想法由C.Strachey 提出，D.Scott 完成了它的基础理论并因此获图灵奖指称语义的基本思想是定义一个语义函数（指称函数），把程序的意义映射到某种意义清晰

39、的数学对象（就像用中文解释英文）作为被指的数学对象可以根据需要选择对简单的程序语言，一种自然的选择是把程序的语义定义为从环境到环境的函数（作为指称）。定义语义就是指定每个程序对应的函数,环境的集合：语义映射：表达式的语义：假设是整型表达式 命令的语义：,第59页,第59页,指称语义,表达式的语义定义：语句的语义定义：,第60页,specification LISTS sorts List NATURALS formal sort Component Operations empty_list:List cons(_，_):Component,ListList headof_:List Comp

40、onent tailof_:List List lengthof_:List NATURALSs variables c:Component l:List equations headof cons(c,l)=c tailof cons(c,l)=l tailof empty_list=empty_list lengthof empty_list=0 lengthof cons(c,l)=succ(length of l)end specification,代数语义把语义模型的集合看成是一个代数结构，模型簇对应为代数系统。用代数方法描述数据类型 A=(V,Op),代数语义,第61页,语法、语义和语用,语法：规定合法程序的形式，清晰定义语言中各种结构的形式。上下文关系采用自然语言说明。语义：规定合法程序的意义，程序执行时所产生的效果。形式语义学探讨形式化定义程序的语义。语用：程序设计技术，具体语言的使用技术和惯用方法。程序设计技术、技巧和设计模式等。,