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，将结果放于某临时单元。将临
2、时单元内容做类型检查（必要时转换）并放入x中。从内存代表x的地址中取出值放在运算器中。加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);msdu指令集客观世界问题抽象模型世界数学模型模拟模型程序世界以程序世界术语表示描述模型机器世界以机器的术语实现程序图2-1 计算机解题的四个世界第5页2.2 PL设计目标定义一组
3、能表示某种范型的特征集，每个特征有严格定义并可在机器上高效实现，程序员可灵活运用这些特征表达它所希望的任何计算。第6页语言设计：目标演化第6页 Fortran 设计中最主要的考虑是易用性（与机器和汇编语言比较）和高效实现高效实现，特别关注程序能翻译成高效执行的代码，因为这样才可能被接受（今天Fortran 仍高效） 。 随着计算机变得越来越快，越来越便宜，效率问题虽然还是很重要，但重要性已大大下降。易用性易用性方面的考虑仍非常明显： 提高程序设计工作的效率 帮助人们提高程序（软件）的质量，可靠性 设法支持某些高级的软件设计技术 语言最主要作用是用于描述所需要的计算过程。为此需要： 清晰，简洁清
4、晰，简洁的形式（例子：C，Pascal，APL ） 清晰简单的语义清晰简单的语义（易理解，易验证） 正交性正交性（避免重复的可相互替代的特征，人们对此有些不同意见） 可读性可读性（人容易阅读理解的东西，计算机也容易处理）第7页语言设计：目标演化第7页随着程序设计语言的发展，语言的设计目标也发生了很大变化语言的初始设计目标就是更方便地为计算机写程序后来人们认识到，程序设计语言也是人的工具，用于描述算法、交流算法，用于服务于交流、教学和科研的需要随着计算机应用发展，程序变得越来越复杂，开发程序变成代价高昂的工作。为支持复杂程序开发，提高开发工作的效率，语言设计有了许多新目标：1.支持对基本语言的扩
5、充扩充，提供各种扩充定义和抽象机制，过程、函数定义机制，扩充语言的基本操作，数据类型定义机制（及OO机制），扩充数据描述方式和功能。例：C+ 在语言机制扩充方面有许多考虑（如运算符重载）可扩充语言（Extendable Languages），允许程序形式的改变（Lisp）第8页语言设计：目标演化第8页2. 提供支持复杂程序所需的高级组织高级组织的机制，支持大型程序开发模块机制（信息隔离和屏蔽），支持分别编译的机制，支持程序的物理组织3 3. 支持软件重用软件重用，包括软件中的部分的重用，支持通用的基本程序库。Pascal Pascal 失败之处之一就是忽略了库的开发。C/Fortran C/F
6、ortran 都做得很好。AdaAda、C+ C+ 和Java Java 的设计都特别考虑了对库的支持。许多新语言定义了功能非常丰富的标准程序库。 支持库开发：库是最基本的重用方式。是否支持库开发，决定了语言能否大范围使用。支持用户和第三方供应商开发各种扩充的和专用的库 支持某些层次或者方式的软件部件概念问题：库开发或者部件是否需要本语言之外的功能？OO OO 概念可能在上面许多方面起作用，因此成为复杂软件开发的重要方法第9页语言设计：目标演化第9页语言设计中需要考虑的另外一些重要问题： 正常处理的异常异常/ /错误处理错误处理的良好集成（在产品软件的程序里，处理错误和各种特殊情况的代码占很大
7、的比例，可能达70%70%） 对于程序的易修改可维护性易修改可维护性的支持 对于并发程序设计并发程序设计的支持，用什么样的机制支持并发程序设计。这方面的问题将长期成为语言研究和设计的热点问题 安全性设计安全性设计：是否有助于程序员写出安全可靠的程序？这一问题在未来许多年都会是语言设计的一个重要关注点 由于语言承载的功能越来越多，设计时需考虑的问题越来越多，新语言正在变得越来越复杂，语言的实现需要做的工作也越来越多（基本处理、对开发过程的支持、库等等），设计一种语言，支持所有需要变得越来越困难。第10页2.2 PL设计目标 定义一组能表示某种范型的特征集，每个特征有严格定义并可在机器上高效实现，
8、程序员可灵活运用这些特征表达它所希望的任何计算。模型有力 Model Power语义清晰 Semantic Clarity移植性好 Portability可读性好 Readability程序质量 Quality安全性并发方便 Convenience简单 Simplicity高效 Efficiency灵活性 Flexibility可扩充性 Extensible 可重用性 Reusable第11页2.3 设计准则 频度准则 越常用越简单 方便、可读 结构一致 程序结构和计算的逻辑结构一致 可读、方便 局部性 Locality 只有全局变量Basic 不鼓励全局变量Pascal,C 无全局变量函数式
9、 Java 词法内聚 Lexical Coherence 变量在使用处就近声明 （Pascal声明和语句严格分开） (lambda (x y) (let (x 3.5) (y (+ a 2)(+ (* x y) (+ (* x y) (- x y) (- x 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 语言编译系统自动找出安全漏洞，不能弥补也要支持 安全性强类型，即
10、每个计算操作运算之前类型必须确定 C 留给程序员 过程参数不检查 一般不安全第13页续正交性和正规性(Orthogonality & Regularity) 正交: 每个语言特征都是独立的, 增减不影响其它 正规: 每一约定或规则无一例外 不正规：数组不能作返回值, 不能赋值 函数不能做参数 不正交不正规第14页续数据隐藏 (Data hiddening) 封装,以名字封装内部数据设计者可见使用者不可见 局部性不一定封装，如： Do l0 I=1,10,2 当I=7时 GOTO 20 10 CONTINUE20 . R=I 可以,此时R=7.0.第15页续抽象表达 抽取因子、递归表达、高层模块
11、名、 常量名=常量表达式（易于维护） 先抽象再修饰具体（如同自然语言）static const int maxlndex=MAX_LENGTH_1MATHLIB.TRIANG COS(X)可移植性 力图不依赖环境 预定义机制、预处理程序第16页形式语法：以形式结构规则的语言元素组合规则微语法 词法 Lexicon宏语法 定义特征的规则2.4 2.4 程序设计语言规格说明程序设计语言规格说明语言参考手册语言参考手册 2.4.1 语法规格说明第17页第17页词法和词法分析 构成程序的基本词法元素包括标识符、运算符、字面量、注释等。复杂的词（标识符、各种字面量）需要明确定义的构词法，即词法 处理源程
12、序的第一步是词法分析： 编译器处理表示源程序的字符序列，根据词法规则做词法分析，将源程序切分为符合词法的段，识别出源程序的有意义单词（token） 词法分析得到一个（表达被分析的源程序的）单词流，流中各单词标明了词法类别（是“标识符”，“整数”，“加号”，“左括号”，等等） 词法分析中抛弃所有无保留价值的分隔符（如空白符）和噪声词例：对int main (void) return 0; 做词法分析，得到的单词序列是：int main ( void ) return 0 ; 共10个单词类别：标识符，左/右圆括号，左/右花括号，整数，分号第18页第18页词法分析 词法分析通常采用最长可能原则，确
13、定可能成为单词的最长字符串。例：staticint是一个标识符，而不是关键字static 和intx+y （C语言）的分析结果是：x，+，+，y；而不是x，+，+，yx+y 是x, +, +, +, y（语法错，+ 的运算对象非左值） 早期的Fortran 中存在复杂的词法问题。例如：DO 10 I = 1.5 的意思类似于C 语言的DO10I = 1.5 而DO 10 I = 1,5 是枚举循环头部，类似于C 的for (I = 1; I 5; +I) . 后来的语言都避免了这类问题，保证单词很容易识别（能局部识别）人们已经开发了许多帮助构造词法分析器的自动工具，如lex/flex等第19页
14、第19页语法 语法规定位于词法层次之上的程序结构。例如： 表达式的合法形式 基本语句的形式，组合语句的构成方式 更上层的结构，如子程序、模块等的构成形式 语法用于确定一个输入序列是否合法的程序。但什么是“合法”？ 程序存在多个不同层次的合法性问题： 1. 1. 局部结构 例：C C程序里的if if 之后是不是左括号，括号是否配对 2. 2. 上下文关系 例：变量使用前是否有定义，使用是否符合类型的要求 3. 3. 深层问题 例：使用变量的值之前，变量是否已经初始化 语言的语法定义通常只描述1 1（程序形式中的上下文无关部分） 编译程序通常检查条件1 1和2 2，有人称2 2 为“静态语义”第
15、20页T是终结符号串的有限集。N是非终结符号串的有限集。TN = ，即它们是不相交的。S是起始符号串， SN。P是产生式， 一般形式是: ，(TN)*“”表示左端可推导出右端，如， ， 则可写为：|如果产生式将语言的非终结符中的每一个标记都推得为终结符号， 则这一组产生式集即为该语言的全部文法。2.4.1.1 文法文法 产生符合语法的语言（句子集合）规则，如：G=(S,N,T,P) SN,TN=*第21页整数的产生式表示法：整数的产生式表示法：设设 0|1|2|3|4|5|6|7|8|9digit0|1|2|3|4|5|6|7|8|9则则 Integer 一位数是整数一位数是整数 Intege
16、r 两位数也是两位数也是 Integer n n位数也是位数也是 n n个个这势必造成产生式臃肿，这势必造成产生式臃肿， 如果写成：如果写成： |Integer| | | 续续第22页续 Chomsky的四种文法产生式 左符号集右符号集 由左符号集推导出右符号集0型文法 (NT)+，(NT)* 递归可枚举语言 图灵机可以识别1型文法 A B ,(NT)*， AN， B(NT)+ 上下文相关文法上下文敏感语言 线性有界自动机可识别2型文法 A (NUT)*, AN 上下文无关文法语言 非确定下推自动机可识别第23页续3型文法 ABB T*, A,BN 正则文法 正则语言 有限自动机可以识别 可消
17、除右端非终法符 P可以成为终结符表达式 例： N=S,R,Q, T=a,b,c P=SRa，SQ，RQb，Qc 则有 SRaQbacba|SQc RQbcb Qc 简单语言用 3型，汇编，词法子语言 最常用 2型 0、1型无法判定二义性, 不常用0 01 12 23 3第24页2.4.1.2 上下文无关文法文法的递归表示法 0123|4|5|6|7|89 一位数 二位数 . n 位数 n个 左递归 右递归尾递归第25页2.4.1.3 BNF 和EBNFBNF： :=代替 BNF表达能力同EBNF 指示非终结 终结符直接写出(或黑体) 或者有扩充： 括号内容是可选的 括号内容可重复0至多次或扩充
18、： C+ Kleene加 C可重复1至多次 C* Kleene星 C可重复0至多次第26页续续BNFBNF示例示例 := unsigned integer := | | := + := + |- |- | | := := | | | | := +|-integer := +|- := | := | := := + + := | := | 第27页EBNF： 左端取消, 空白加- 减少递归表示再加(,),., 尽量用正则表达式 终结符号加 号或黑体续第28页续program := program := ； . .program-heading := program program-heading
19、 := program ( ). ( ).program-parameters := .program-parameters := .identifier-list := identifier-list := ， . .program-block := .program-block := .block := block := . .variable-declaration-part := var variable-declaration-part := var ； ； . .variable-declaration := variable-declaration := ； . .stateme
20、nt-part := compound-statement.statement-part := compound-statement.第29页compound-statement := begin pound-statement := begin end.statement-sequence := statement-sequence := ； . .statement:= statement:= ：(|).(|).simple-statement := | |simple-statement := | | | . | .structured-statement := |structured-
21、statement := | | | . | | . 续第30页2.4.1.4 语法图同同EBNF EBNF 取消取消 以以短路表示短路表示 以以迥环表示迥环表示非终结非终结符符走向走向复合语句复合语句; ;beginbeginendend语句语句终结终结符符终结终结符符第31页2.4.1.5 语法分析语法规格说明定义了该语言程序合法的特征和语句。语言处理器语法规格说明定义了该语言程序合法的特征和语句。语言处理器则通过语法分析接受合法的程序，这就叫做程序释义（则通过语法分析接受合法的程序，这就叫做程序释义（Parsing a Parsing a ProgramProgram）, ,释义过程是产
22、生式生成句子的逆过程。释义过程是产生式生成句子的逆过程。语法分析的算法可归为两类：语法分析的算法可归为两类：“自顶向下自顶向下” 释义则从文法的起始符开始，按可能产生的表达式释义则从文法的起始符开始，按可能产生的表达式寻找语句相同的结构匹配。每一步都产生下一个可能的源符号串，寻找语句相同的结构匹配。每一步都产生下一个可能的源符号串，找到再往下走。找到再往下走。“由底向上由底向上”释义则相反，它先查找源代码的各个符号串，看它释义则相反，它先查找源代码的各个符号串，看它能否匹配归结为产生式左边的非终结符，如果有含混则向前多读能否匹配归结为产生式左边的非终结符，如果有含混则向前多读入入k k个符号串
23、，为此归约下去，一个短语一个短语，最后到达起始个符号串，为此归约下去，一个短语一个短语，最后到达起始符号串，归约的过程就形成了释义树。符号串，归约的过程就形成了释义树。第32页beginbegin x x ：= = 17 17 ； writeInwriteIn ( ( x x ) ) endend标识符标识符变量标识符变量标识符变量访问变量访问无符号常量无符号常量完整变量完整变量无符号数无符号数无符号整数无符号整数因子因子项项简单表达式简单表达式表达式表达式过程标识符过程标识符标识符标识符变量标识符变量标识符完整变量完整变量变量访问变量访问因子因子项项简单表达式简单表达式表达式表达式write
24、write参数参数writelnwriteln参数表参数表赋赋值语句值语句简单语句简单语句语句语句过程语句过程语句简单语句简单语句语句语句语句序列语句序列复合语句复合语句第33页第33页 语法分析是语言翻译过程的一个重要阶段。语法分析技术是“编译原理”或“编译技术”课程的重要内容 本课程不准备详细介绍语法分析的技术，词法分析和语法分析过程并不仅用在编译系统里。 许多计算机软件的用户输入都需要做词法分析和简单的语法分析今天的大部分语法分析器都是用工具生成的。例yacc/bisonyacc/bison。 这些工具接受某种类似BNF BNF 的语法描述，生成对应的语法分析器人们为各种主要语言（C/C
25、+/JavaC/C+/Java等）开发了支持做词法和语法分析的工具或库，有些脚本语言本身就带有词法/ /语法分析库，可直接使用2.4.1.5 语法分析第34页第34页常规的语言编译过程词法分析语法分析语义分析和中间代码生成与机器无关的优化目标代码生成机器特定的优化第35页2.4.2 语义定义与规格说明第35页语义定义：目标是赋予每个合法的程序一个明确的意义 精确定义程序执行的效果（行为，结果） 要求编译程序（等）生成这种效果 写程序的人可以依赖于这种效果，据此写自己的程序语义定义的基本方法是基于语言的语法结构： 定义语言中各种基本元素的意义 定义语言中各种语法结构的意义基于相应结构的成分的意义
26、，定义整个结构的意义一些具体情况：表达式的意义是其怎样求值，求出什么值语句的意义是其执行时的产生的效果第36页第36页Algol 60 Algol 60 修订报告 用BNF BNF 定义语言的语法， 采用自然语言形式的说明和实例的方式，非形式地定义语言的语义Backus Backus 在讨论Algol 60 Algol 60 时说： 现在我们已经有办法严格地定义语言的语法了，希望今后不久就能严格地定义语言的语义。很遗憾，至今的语言手册仍一直沿用上述方式。因为： - 语义远比语法复杂，至今计算机工作者还没有开发出一种完美、功 能强大、易理解、易使用，适用于定义一切语言中一切结构的语义 描述方式
27、- 但是，对于程序语义的研究已经得到许多成果。有关程序语言语义 的研究是计算机科学的一个重要研究领域 2.4.2 语义定义与规格说明第37页1、静态语义：类型的理论第37页类型是程序设计语言的一个重要问题程序语言需要有清晰定义的类型系统，以确定程序里- 各表达式的类型（typingtyping）。注意，表达式可能嵌套- 各语句是否类型良好的（well-typedwell-typed），或称为良类型的- 处理程序中与类型有关的各种问题：类型等价、类型相容、类型转换（自动转换规则，手工转换规则）等有关类型的研究形成了计算机科学中一个重要的研究领域：类型理论 第38页1、类型环境和类型断言第38页类
28、型判断的根据： - 每个文字量都有自己的确定类型 - 变量、函数等的声明提出了相关的类型要求 - 对类型合适的参数，运算符、函数将给出特定类型的结果（注意 ：重载的运算符也有运算结果和运算对象之间的关系）类型检查需要知道程序里所有变量的类型信息。当前所有可见变量的类型信息的全体构成了当前的类型环境。一个变量的类型信息用变量名和类型的对表示，如x x 具有类型T T：类型环境就是这种对的序列，如：下面用 （可能加下标）表示类型环境第39页1、类型推导第39页我们用形式化的记法表示有关类型的断言。类型断言有两种形式： 在特定类型环境 下，我们确定了表达式 e 的结果类型是 T （表达式：常量、变量
29、、有结构成分的复杂表达式） 在环境 下命令（语句）c 是类型良好的（基本语句如赋 值，各种复合语句和更复杂的程序结构）为了作出程序中各种结构是否类型良好的判断，确定有类型结构（表达式）的具体类型，要定义一套做类型推断的规则（类型规则），说明 如何得到程序中基本表达式的类型 基于表达式的部分的类型推出整个表达式的类型 然后基于表达式的类型，推断基本语句是否类型良好； 基于基本语句的良类型性得到复合语句的良类型性 不能推导出类型的表达式是类型错误的表达式，对语句也一样第40页1、类型规则第40页下面用一个简单语言介绍类型规则的一些定义。假定语言里有intint 和double double 类型变
30、量声明，赋值语句和结构语句类型规则包括（例子）：基本规则（1 1）基本规则（2 2）第41页1、类型规则第41页表达式的类型规则（一组）：语句的类型规则（一组）：变量声明：其他规则可以类似写出第42页2、语义基础：环境和状态第42页考虑程序的（动态）语义（程序执行的语义） - 希望用清晰严格的方式描述程序执行中各种动作的效果对程序动态行为的理解和严格描述依赖于环境的概念 - 程序执行过程中存在着一些实体（变量、子程序等） - 可能存在与这些实体相关的信息（例如，变量的值，函数的定义） 程序里动作的执行可能改变与一些实体相关的信息，如改变变量的值 - 环境记录与各种有效实体相关的信息 - 因此，
31、动作的执行可能改变环境讨论语义时关心的是程序的动态环境（运行中的环境）编译（和类型检查）工作中维护的符号表是支持语言处理的“静态环境”最简单的环境模型：从合法名字集合到“值”的映射（是一个有限函数）第43页2、环境和状态第43页程序执行的动作可能依赖于环境，或导致环境的变化： - 需要某变量的值时，从当时环境里取出它的值 - 一些操作修改环境中变量的值，如赋值、输入等 - 进入或退出作用域（如进入/ /退出子程序或内部嵌套的复合语句） 可能改变当前有定义的变量集合（改变环境的定义域） - 程序开始运行前，需要建立一个初始全局环境，其中包含着所有具 有全局定义的名字及与之相关的默认信息下面把环境
32、建模为变量名到其取值的简单的有限函数 - 如果研究的是更复杂的语言，这种简单形式就可能不够了，需要考虑更复杂的环境模型 - 例如包含指针和动态存储分配/ /释放，或面向对象的语言（OO OO 语言），就需要为更复杂的环境模型 在程序运行中，当时环境中所有可用变量的取值情况构成了运行时的状态第44页2、环境和状态第44页例：设当时环境中可见的变量是x, y, zx, y, z，取值情况是x x 取值3 3，y y 取值5 5，z z 取值0 0这个状态就是有限函数：随着程序的执行，特别是赋值语句的执行，环境的状态就可能改变 经过给x x 赋值4 4，给y y 赋值1 1 的两个操作，状态将变成：
33、理解一个（或一段）程序的意义，就是理解它在有关环境下的意义，以及它的执行对环境的作用第45页2、环境和状态第45页严格些说，一个环境是一个“部分函数”：为描述状态变化，在环境上定义了一种覆盖操作：例：第46页2、环境和状态第46页对于常量（如整数），任何环境都给出它们的字面值环境确定一组变量的值，就确定了基于这些变量构造的表达式的意义假定我们有：对于一般表达式：由于环境可以确定表达式的意义（确定表达式的值）。我们也可以把环境看成从合法表达式到值集合的映射，有些表达式的值无定义，例如其中出现了在环境取值为无定义的变量，或者求值中出现无定义运算结果（如除数为0 0）等第47页3、语义规格说明第47
34、页我们把程序的意义定义为它们对环境的作用。为定义语义需要： - 定义基本语句的意义 - 定义各种结构的意义如何由它们的组成部分得到有了这些定义，就可以确定由这些语言结构构成的复杂程序的意义一个程序的执行导致环境的变化，问题是如何严格定义这种变化人们提出了多种不同的形式化的语义定义方式（技术）：操作语义：把程序运行看成执行了一系列改变环境的操作，用一组描述环境变化的规则定义程序中各种结构的意义公理语义：用谓词描述状态，用公理和推理规则描述各种基本操作和组合结构的语义指称语义：把程序的意义映射到某种的数学结构，这种结构能清晰地表达程序对环境的作用和环境的变化代数语义：考虑程序之间的等价关系，间接定
35、义程序的意义第48页操作语义：格局和规则第48页首先需要定义格局（configurationconfiguration）。这里定义两种格局： 终止格局，就是一个环境，表示代码运行完成时的状态 非终止格局： 表示程序运行中的一个“状态” 一段程序代码（待执行代码段）和一个环境结构化操作语义（SOSSOS）用一组格局变迁规则定义语言的语义。可能包括一些无前提的规则和一些有前提的规则赋值语句的语义规则（无前提规则）：复合语句的语义规则（有前提规则）：第49页操作语义：续第49页if if 条件语句的语义规则（两条）：while while 循环语句的语义规则（两条）：上面这组规则严格地定义了一个理想
36、的小语言的语义注意这个小语言的特点。它与实际的程序语言还是有很大差距第50页第50页公理语义 R. Floyd 在1967年考虑如何说明一个程序完成了所需工作时，提出用逻辑公式描述程序环境的状态的思想。这种描述环境的逻辑公式称为断言逻辑公式：描述了状态：说明环境满足公式，实际上，这个状态还满足另外的许多逻辑公式，如：反过来看，一个逻辑公式可以被许多状态满足因此可以认为，一个公式描述了一个状态集合。例如，上面第二个公式，描述了所有的其中x 值是1 的环境第51页第51页公理语义：断言把断言写在程序里某个特定位置，就是想提出一个要求： - 程序执行到这个位置，当时的环境状态必须满足断言 - 如果满
37、足，程序就正常向下执行（就像没有这个断言） - 如果不满足，程序就应该（非正常地）终止实例： C 语言标准库提供了断言宏机制，可以在程序里的写assert(x 0); Stroustrup 在The C+ Programming Language里特别讨论了如何 定义断言类的问题 有些语言本身提供了断言机制，如Eiffel。见Design by Contract, 中译本：邮电出版社断言的概念在实际程序开发中起着越来越重要的作用第52页第52页公理语义：前条件和后条件如何借助于逻辑公式描述一段程序的意义？Hoare 提出的方法是用一对公式，放在相应程序段之前和之后，分别称为该程序段的前条件（p
38、recondition）和后条件（postcondition）pre P post意思是：如果在程序P 执行之前条件pre 成立（当时的环境满足pre），那么在P 执行终止时的环境中，条件post 一定成立我们可以用一对公式(pre, post) 描述一段程序的语义，也可以把这样的公式对(pre, post) 看作是对一段程序的语义要求，看作程序的规范前后条件的两种基本用途： 作为评判程序是否正确的标准 作为待开发的程序的规范，研究如何从这种规范得到所需的程序.第53页第53页公理语义：不变式不变式（不变量，invariant）的概念在许多领域中有重要地位 程序理论中的不变式，指写在程序里特定
39、位置的逻辑公式，要求程序执执行中每次达到某个（某些）情况时，这个公式都必须成立 其实，不变式并不特殊，因为写在程序里的断言，也就是位于代码中相应特定位置的不变式，“情况”就是执行达到这个位置程序理论里最重要的不变式之一是循环不变式（loop invariant），要求一个循环的每次迭代开始之前成立，在描述和推导程序的意义时有特殊价值直接插入排序算法两重循环的不变式（图示）：第54页第54页Floyd 最早提出用断言描述程序的意义，通过逻辑推导证明程序的正确性。他称自己提出的方法为“断言法”。基本方法： - 在流程图程序里的每条边上放一条断言 - 设法证明从一个动作框的入边上的断言出发，执行相应
40、动作产生的效 果能保证该动作框的出边上的断言成立 - 对分支控制框也有特殊的规则（请自己考虑） - 如果对每个动作框都能证明上述事实成立，那么标注在流程图中各条 边上的断言就形成了该程序的一个（一套）语义描述 - 特别的，标在程序入口和出口上的断言表示了这段程序的整体效果Hoare 总结了Floyd 的工作，针对结构化的程序控制结构提出了一套逻辑推理规则，这就是有名的Hoare 逻辑 公理语义：程序的意义第55页第55页公理语义：Hoare逻辑Hoare 逻辑是对有关程序意义的逻辑描述的整理和系统化Hoare 逻辑中的逻辑公式形式为（称为Hoare 三元组）： p S q其中p 和q 是谓词逻
41、辑公式，S 是一段程序直观意义：如果在S 执行之前公式p 成立，在S 执行终止时q 就成立Hoare 的最重要贡献是提出了一套推理规则，通过这些规则，可以把证明一个Hoare 公式（程序S 相对于p 和q 的正确性）的问题归结为证明一组普通一阶谓词逻辑公式的问题Dijkstra 在此基础上提出了最弱前条件（weakest precondition）的概念，借助于这一概念，可以 把程序的正确性证明工作进一步规范化 用于做程序的推导（从规范出发推导程序）第56页第56页公理语义：Hoare逻辑公理：规则LOOP 里的I 是循环不变式第57页第57页公理语义：Hoare逻辑 可以用Hoare Hoa
42、re 逻辑证明程序的正确性，也就是说，证明三元组中的程序语句“符合”前后条件的要求。其意义是： 若在前条件满足的情况下执行语句且语句执行终止，那么后条件满足 这个证明并不保证语句终止，如果语句的执行不终止，什么后条件都可以证明。因此，这样证明的正确性称为“部分正确性” 程序终止性需要另外证明，主要是需要证明其中循环的执行必然终止 如果同时证明程序的部分正确性和终止性，这一程序就是“完全正确的”程序正确性证明中的一个关键点是为各个循环提供适当的不变式 就像做数学归纳法证明中需要合适的归纳假设，过强或过弱都不行人们已证明，循环不变式不可能自动生成（无完全的算法，但有许多研究）公理语义为我们提供了许
43、多有助于理解程序行为的概念，为设计程序时思考其行为提供了重要的依据和线索。第58页第58页指称语义 指称语义学（denotational semantics）有坚实的数学基础，它的基本想法由C.Strachey 提出，D. Scott 完成了它的基础理论并因此获图灵奖指称语义的基本思想是定义一个语义函数（指称函数），把程序的意义映射到某种意义清晰的数学对象（就像用中文解释英文）作为被指的数学对象可以根据需要选择对简单的程序语言，一种自然的选择是把程序的语义定义为从环境到环境的函数（作为指称）。定义语义就是指定每个程序对应的函数环境的集合：语义映射：表达式的语义： 假设是整型表达式 命令的语义：
44、第59页第59页指称语义表达式的语义定义：语句的语义定义：第60页specificationspecification LISTS sorts sorts List NATURALS formal sort Component Operations Operations empty_list : List cons(_，_) : Component,ListList headof_ : List Component tailof_ : List List lengthof_ : List NATURALSs variables variables c: Component l: List eq
45、uationsequations 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 end specification代数语义把语义模型的集合看成是一个代数结构，模型簇对应为代数系统 。用代数方法描述数据类型 A=(V, Op)代数语义第61页语法、语义和语用语法、语义和语用语法：规定合法程序的形式，清晰定义语言中各种结构的形式。上下文关系采用自然语言说明。语义：规定合法程序的意义，程序执行时所产生的效果。形式语义学探讨形式化定义程序的语义。语用：程序设计技术，具体语言的使用技术和惯用方法。程序设计技术、技巧和设计模式等。
