第2章 PL设计概述

Size: px

Start display at page:

Download "第2章 PL设计概述"

贴题机
5 years ago
Views:

1 第二章程序设计语言设计概述 2.1 表示与抽象 2.2 设计目标 2.3 设计准则 2.4 规格说明第 1 页

2 计算机语言定义表示法 ( 或符号 ) 系统 LRM 可以编制软件机器可识别可执行 ( 应用 ) 第 2 页

3 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+u>s+d+2u) u++; print(u); m s d u 指令集客观世界模型世界程序世界机器世界问题抽象数学模型以程序世界术语以机器的术语模拟模型表示描述模型实现程序图 2-1 计算机解题的四个世界第 3 页

4 语言实现 : 在裂谷上架桥第一种方式 : 将语言降低到机器水平通过编译器的翻译程序完成编译器把程序翻译成能运行的代码编译器的输入称作源语言, 输出称为目标语言编译器将源语言翻译为目标语言的等价语言第 4 页

5 语言实现 : 在裂谷上架桥第一种方式 : 将语言降低到机器水平第二种方式 : 把机器提升到语言的水平构造称为解释器的高级机器解释器直接运行程序程序输入解释器输出 Fuction eval(e)= if E is the constant I then I else if E is the sum of E 1 and E 2 then eval(e 1 )+eval(e 2 ) else if E is the product of E 1 and E 2 then eval(e 1 )*eval(e 2 ) 第 5 页

6 对比编译器和解释器程序的静态性质和动态性质静态 : 由程序正文显现出来的性质动态 : 依靠程序运行才能显现出来的性质效率 : 编译可能取得比解释更高的效率灵活性 : 使在运行中修改程序成为可能可以在源程序正文中精确定位错误和报告第 6 页

7 2.1 表示与抽象表示是人为制造的符号组合以表达我们需要表达的意思程序是程序设计语言表示的计算 float n; //n 是浮点数变量 sqrt(n) ; // 对 n 取平方根同一程序的高级语言表示经翻译后的汇编码表示机器码表示就是该程序在不同抽象层次上的表示第 7 页

8 2.1 表示与抽象程序在不同抽象层次表示的关系例 :x = x + 1 在机器码上就有两种方法从内存代表 x 的地址中取出值放在运算器中加 1, 将结果放于某临时单元从内存代表 x 的地址中取出值放在运算器中加 1, 将结果放入 x 地址中将临时单元内容做类型检查 ( 必要时转换 ) 并放入 x 中第 8 页

9 2.2 PL 设计目标 ( 功能 ) 定义一组能表示某种范型的特征集, 每个特征有严格定义并可在机器上高效实现, 程序员可灵活运用这些特征表达它所希望的任何计算指挥机器的工具程序员交流的方式表达高层设计的媒介算法的记述方式表达观念间关系的途径控制计算机化设备的途径第 9 页

10 语言设计 : 目标演化 Fortran 设计中最主要的考虑是易用性 ( 与机器和汇编语言比较 ) 和高效实现, 特别关注程序能翻译成高效执行的代码, 因为这样才可能被接受 ( 今天 Fortran 仍高效 ) 随着计算机变得越来越快, 越来越便宜, 效率问题虽然还是很重要, 但重要性已大大下降易用性方面的考虑仍非常明显 : 提高程序设计工作的效率帮助人们提高程序 ( 软件 ) 的质量, 可靠性设法支持某些高级的软件设计技术语言最主要作用是用于描述所需要的计算过程为此需要 : 清晰, 简洁的形式 ( 例子 :C,Pascal,APL ) 清晰简单的语义 ( 易理解, 易验证 ) 正交性 ( 避免重复的可相互替代的特征, 人们对此有些不同意见 ) 可读性 ( 人容易阅读理解的东西, 计算机也容易处理 ) 第 10 页

11 语言设计 : 目标演化随着程序设计语言的发展, 语言的设计目标也发生了很大变化语言的初始设计目标就是更方便地为计算机写程序后来人们认识到, 程序设计语言也是人的工具, 用于描述算法交流算法, 用于服务于交流教学和科研的需要随着计算机应用发展, 程序变得越来越复杂, 开发程序变成代价高昂的工作为支持复杂程序开发, 提高开发工作的效率, 语言设计有了许多新目标 : 1. 支持对基本语言的扩充, 提供各种扩充定义和抽象机制, 过程函数定义机制, 扩充语言的基本操作, 数据类型定义机制 ( 及 OO 机制 ), 扩充数据描述方式和功能例 :C++ 在语言机制扩充方面有许多考虑 ( 如运算符重载 ) 可扩充语言 (Extendable Languages), 允许程序形式的改变 (Lisp) 第 11 页

12 语言设计 : 目标演化 2. 提供支持复杂程序所需的高级组织的机制, 支持大型程序开发模块机制 ( 信息隔离和屏蔽 ), 支持分别编译的机制, 支持程序的物理组织 3. 支持软件重用, 包括软件中的部分的重用, 支持通用的基本程序库 Pascal 失败之处之一就是忽略了库的开发 C/Fortran 都做得很好 Ada C++ 和 Java 的设计都特别考虑了对库的支持许多新语言定义了功能非常丰富的标准程序库支持库开发 : 库是最基本的重用方式是否支持库开发, 决定了语言能否大范围使用支持用户和第三方供应商开发各种扩充的和专用的库支持某些层次或者方式的软件部件概念问题 : 库开发或者部件是否需要本语言之外的功能? OO 概念可能在上面许多方面起作用, 因此成为复杂软件开发的重要方法第 12 页

13 语言设计 : 目标演化语言设计中需要考虑的另外一些重要问题 : 正常处理的异常 / 错误处理的良好集成 ( 在产品软件的程序里, 处理错误和各种特殊情况的代码占很大的比例, 可能达 70%) 对于程序的易修改可维护性的支持对于并发程序设计的支持, 用什么样的机制支持并发程序设计这方面的问题将长期成为语言研究和设计的热点问题安全性设计 : 是否有助于程序员写出安全可靠的程序? 这一问题在未来许多年都会是语言设计的一个重要关注点由于语言承载的功能越来越多, 设计时需考虑的问题越来越多, 新语言正在变得越来越复杂, 语言的实现需要做的工作也越来越多 ( 基本处理对开发过程的支持库等等 ), 设计一种语言, 支持所有需要变得越来越困难第 13 页

14 2.2 PL 设计目标定义一组能表示某种范型的特征集, 每个特征有严格定义并可在机器上高效实现, 程序员可灵活运用这些特征表达它所希望的任何计算模型有力 Model Power 语义清晰 Semantic Clarity 移植性好 Portability 可读性好 Readability 方便 Convenience 简单 Simplicity 高效 Efficiency 灵活性 Flexibility 程序质量 Quality 安全性并发可扩充性 Extensible 可重用性 Reusable 第 14 页

15 什么是好 PL 透明性简单性和统一性正交性应用的自然性对抽象性的支持程序的易验证性编程环境程序的可移植性使用代价程序执行的代价翻译的代价程序创建测试第 15 页和使用的代价程序维护的代价

16 好 PL 的评价标准与矛盾可读性 : 如果一个程序算法和数据结构能够明显地从程序文本中观察出来, 那么这个程序就是可读的可写性 : 使用简洁的整齐的语法结构将会增强程序的可写性易检验性 : 能够使用数学方法证明程序的正确性易翻译性 : 关键是结构的规范化无二义性 : 为每一种程序员可能写出的语法构造提供独一无二的解释第 16 页

17 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 y))) 3.5 (+ a 2)) λx.λy.((x*y)+(x-y) 3.5 (a+2) 第 17 页

18 续语法一致性 GO TO (L1, L2,, Ln), I I={1..n} GO TO N, (L1, L2,, Ln) ASSIGN Li TO N N={L1...Ln} 安全性 Security 语言编译系统自动找出安全漏洞, 不能弥补也要支持安全性强类型, 即每个计算操作运算之前类型必须确定 C 留给程序员过程参数不检查一般不安全第 18 页

19 续正交性和正规性 (Orthogonality & Regularity) 正交 : 每个语言特征都是独立的, 增减不影响其它正规 : 每一约定或规则无一例外不正规 : 数组不能作返回值, 不能赋值函数不能做参数不正交不正规第 19 页

20 续数据隐藏 (Data hiddening) 封装, 以名字封装内部数据设计者可见使用者不可见局部性不一定封装, 如 : Do l0 I=1,10,2 当 I=7 时 GOTO CONTINUE R=I 可以, 此时 R=7.0 第 20 页

21 续抽象表达抽取因子递归表达高层模块名常量名 = 常量表达式 ( 易于维护 ) 先抽象再修饰具体 ( 如同自然语言 ) static const int maxlndex=max_length_1 MATHLIB.TRIANG COS(X) 可移植性力图不依赖环境预定义机制预处理程序第 21 页

22 显示表式和隐式表示语言一开始就追求无二义性, 都希望显式表示太繁在不产生二义情况下用约定代替显示表示简化 PI: Constant FLOAT:= ; PI: Constant:= ; 第 22 页

23 FORTH 聚合和分散表示 + 单字长加 + 什么都表示 D+ 双字长加要求编译有解析能力 M+ 混合加 FORTRAN FUNCTION SUM(V,N) REAL V(N) SUM=0.0 DO 200 I=1,N SUM=SUM+V(I) 200 RETURN END C Ada function SUM(V:VECTOR, N:INTEGER) return FLOAT; 第 23 页

24 2.4 程序设计语言规格说明语言参考手册语法规格说明形式语法 : 以形式结构规则的语言元素组合规则微语法词法 Lexicon 宏语法定义特征的规则第 24 页

25 语言组织的基本方案语法 : 以句子中词的排列来表明它们的彼此关系理解一个程序提供重要信息为程序翻译提供必要信息除语法结构外, 在完全描述一个程序时还需要其他信息第 25 页

26 语法要素和语法单元组织字符集标识符操作符关键字和保留字噪声码注释空白符定界符和括号自由或固定字段格式表达式语句独立子程序定义独立数据定义嵌套子程序定义独立接口定义从可执行语句中独立出来的数据描述非独立子程序定义第 26 页

27 从头到尾的翻译过程词法分析 : 任何翻译最基本的步骤总是将符号串划分成基本单元 ( 语法项 / 语法要素 ) 语法分析 : 识别出由词法分析器所产生的词法项组成的更大的程序结构 ( 如语句声明表达式等 ) 语义分析 : 由语法分析器识别出的语法结构将在这里处理, 同时可执行代码结构开始成型第 27 页

28 程序设计语言规格说明 : 定义语言语法规格说明形式语法 : 以形式结构规则的语言元素组合规则微语法 / 词法 (Lexicon) 宏语法 : 定义词法短语组合是合法的语法特征考察所有具有字母 ab 的字符序列所构成的集合如 ab,aab,abb, 第 28 页

29 词法和词法分析构成程序的基本词法元素包括标识符运算符字面量注释等复杂的词 ( 标识符各种字面量 ) 需要明确定义的构词法, 即词法处理源程序的第一步是词法分析 : 编译器处理表示源程序的字符序列, 根据词法规则做词法分析, 将源程序切分为符合词法的段, 识别出源程序的有意义单词 (token) 词法分析得到一个 ( 表达被分析的源程序的 ) 单词流, 流中各单词标明了词法类别 ( 是标识符, 整数, 加号, 左括号, 等等 ) 词法分析中抛弃所有无保留价值的分隔符 ( 如空白符 ) 和噪声词例 : 对 int main (void) { return 0; } 做词法分析, 得到的单词序列是 : "int" "main" "(" "void" ")" "{" "return" "0" ";" "}" 共 10 个单词类别 : 标识符, 左 / 右圆括号, 左 / 右花括号, 整数, 分号第 29 页

30 词法分析词法分析通常采用最长可能原则, 确定可能成为单词的最长字符串例 :staticint 是一个标识符, 而不是关键字 static 和 int x+++y (C 语言 ) 的分析结果是 :x,++,+,y; 而不是 x,+,++,y x+++++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 等第 30 页

31 语法语法规定位于词法层次之上的程序结构例如 : 表达式的合法形式基本语句的形式, 组合语句的构成方式更上层的结构, 如子程序模块等的构成形式语法用于确定一个输入序列是否合法的程序但什么是合法? 程序存在多个不同层次的合法性问题 : 1. 局部结构例 :C 程序里的 if 之后是不是左括号, 括号是否配对 2. 上下文关系例 : 变量使用前是否有定义, 使用是否符合类型的要求 3. 深层问题例 : 使用变量的值之前, 变量是否已经初始化语言的语法定义通常只描述 1( 程序形式中的上下文无关部分 ) 编译程序通常检查条件 1 和 2, 有人称 2 为静态语义第 31 页

32 文法文法产生符合语法的语言 ( 句子集合 ) 规则, 如 : G=(S,N,T,P) S N,T N=Φ * T 是终结符号串的有限集 N 是非终结符号串的有限集 T N = Φ, 即它们是不相交的 S 是起始符号串, S N P 是产生式, 一般形式是 :α β α,β (T N) * 表示左端可推导出右端, 如 α β, α Υ, α δ 则可写为 :α β Υ δ 如果产生式将语言的非终结符中的每一个标记都推得为终结符号, 则这一组产生式集即为该语言的全部文法第 32 页

33 续整数的产生式表示法 : 设 <digit> 则 <Integer> <digit> <Integer> <digit><digit> <Integer> <digit> <digit> 一位数是整数两位数也是 n 位数也是 n 个这势必造成产生式臃肿, 如果写成 : <Integer> <digit> <Integer><digit> <digit> <Integer> 第 33 页

34 续 Chomsky 的四种文法产生式左符号集右符号集由左符号集推导出右符号集 0 型文法 α β α (N T) +,β (N T) * 递归可枚举语言图灵机可以识别 1 型文法 α A β αbβ α,β (N T) *, A N, B (N T) + 上下文相关文法上下文敏感语言线性有界自动机可识别 2 型文法 A α α (NUT) *, A N 上下文无关文法语言非确定下推自动机可识别第 34 页

35 续 3 型文法 A αb Bα α T *, A,B N 正则文法正则语言有限自动机可以识别可消除右端非终法符 P 可以成为终结符表达式例 : N={S,R,Q}, T={a,b,c} P={S Ra,S Q,R Qb,Q c} 则有 S Ra Qba cba S Q c R Qb cb Q c 简单语言用最常用 3 型, 汇编, 词法子语言 2 型 0 1 型无法判定二义性, 不常用第 35 页

36 BNF 上下文无关文法文法的递归表示法 <digit> <integer> <digit> <integer> <digit><digit> <integer> <digit>...<digit> n 个一位数二位数 n 位数 <integer> <digit> <integer><digit> 左递归 <digit><integer> 右递归 ( 尾递归 ) 一个上下文无关文法, 包含以下四个部分 : 1) 一集单词或终结符, 它们是语言里的原子符号 2) 一集非终结符, 它们是语言里的原子符号 3) 一集称为产生式的规则, 每条规则确定一个结构的各个成分 4) 选定了一个非终结符作为开始符号, 它代表语言的主结构第 36 页

37 续 BNF 示例 <unsigned integer> ::= <digit> <unsigned integer> <digit> <integer> ::= +<unsigned integer> -<unsigned integer> <unsigned integer> <identifier> ::= <letter> <idenfitier> < digit> <identifier> <letter> <integer> ::= [ + -]<unsigned integer> <identifier> ::= <letter> {<digit> <letter>} <unsigned integer> ::= <digit> + <identifier> ::= <letter> {<digit> < letter>} 第 37 页

38 BNF 和 EBNF BNF: ::= 代替 BNF 表达能力同 EBNF < > 指示非终结终结符直接写出 ( 或黑体 ) 或者有扩充 : [ ] 括号内容是可选的 { } 括号内容可重复 0 至多次或扩充 : C+ 'Kleene 加 ' C 可重复 1 至多次 C* Kleene 星 C 可重复 0 至多次第 38 页

39 续 EBNF: 左端取消 < >, 空白加 - 减少递归表示再加 (, ),., 尽量用正则表达式终结符号加号或黑体第 39 页

40 BNF 和 EBNF 如 : 有符号整型是由一系列前边加正号或负号的数字所组成 BNF < 有符号整型 > ::= +< 整型 > -< 整型 > < 整型 > ::= < 数字 > < 整型 >< 数字 > EBNF < 有符号整型 > ::= [+ -]< 数字 >{< 数字 >} * 第 40 页

41 续 program ::= <program-heading> ';' <program-block> '.'. program-heading ::= 'program' <identifier> [ '('<program-parameters> ')']. program-parameters ::= <identifier-list>. identifier-list ::= <identifier> {',' <identifier>}. program-block ::= <block>. block ::= <label-declaration-part> <constant-declaration-part> <type-declaration-part><variable-declaration-part> <procedure-and-function-declaration-part><statement-part>. variable-declaration-part ::= ['var' <variable-declaration> ';' {<variabe-declaration> ';' }]. variable-declaration ::= <identifier-list> ';' <type-denoter>. statement-part ::= compound-statement. 第 41 页

42 续 compound-statement ::= 'begin' <statement-sequence> 'end'. statement-sequence ::= <statement> {';' <statement>}. statement::=[<label> ':'](<simple-statement> <structured-statement>). simple-statement ::= <empty-statement> <assignment-statement> <procedure-statement> < goto-statement>. structured-statement ::= <compound-statement> <conditional-statement> <repetitive-statement> <with-statement>. 第 42 页

43 语法图同 EBNF 非终结符终结符终结符走向取消 [ ] 以短路表示 { } 以迥环表示 ; 复合语句 begin 语句 end 第 43 页

44 语法分析语法规格说明定义了该语言程序合法的特征和语句语言处理器则通过语法分析接受合法的程序, 这就叫做程序释义 (Parsing a Program), 释义过程是产生式生成句子的逆过程语法分析的算法可归为两类 : 自顶向下释义则从文法的起始符开始, 按可能产生的表达式寻找语句相同的结构匹配每一步都产生下一个可能的源符号串, 找到再往下走由底向上释义则相反, 它先查找源代码的各个符号串, 看它能否匹配归结为产生式左边的非终结符, 如果有含混则向前多读入 k 个符号串, 为此归约下去, 一个短语一个短语, 最后到达起始符号串, 归约的过程就形成了释义树第 44 页

45 begin x := 17 ; writein ( x ) end 标识符变量标识符完整变量变量访问赋值语句简单语句语句无符号整数无符号数无符号常量因子项简单表达式表达式过程标识符标识符变量标识符完整变量变量访问因子项简单表达式表达式 write 参数 writeln 参数表过程语句简单语句语句语句序列复合语句第 45 页

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

47 常规的语言编译过程词法分析语法分析语义分析和中间代码生成与机器无关的优化目标代码生成机器特定的优化第 47 页第 47 页

48 上下文规格说明表达式 : x/2 X 是字符还是数值? 这是一个语义错误因为有一个 '/' 的操作数不是数字, 导致对表达式的求值失败这是一个语法错误因为不能孤立地看这个表达式而应将它作为程序的一部分上下文约束 (contextual constraints), 它与语法和语义都有区别限定程序短语的良构规则简化语法语义形式化使上下文无关文法得以使用第 48 页

49 2.4.2 语义定义与规格说明语义定义 : 目标是赋予每个合法的程序一个明确的意义精确定义程序执行的效果 ( 行为, 结果 ) 要求编译程序 ( 等 ) 生成这种效果写程序的人可以依赖于这种效果, 据此写自己的程序语义定义的基本方法是基于语言的语法结构 : 定义语言中各种基本元素的意义定义语言中各种语法结构的意义基于相应结构的成分的意义, 定义整个结构的意义一些具体情况 : 表达式的意义是其怎样求值, 求出什么值语句的意义是其执行时的产生的效果第 49 页

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

51 1 静态语义 : 类型的理论类型是程序设计语言的一个重要问题程序语言需要有清晰定义的类型系统, 以确定程序里 - 各表达式的类型 (typing) 注意, 表达式可能嵌套 - 各语句是否类型良好的 (well-typed), 或称为良类型的 - 处理程序中与类型有关的各种问题 : 类型等价类型相容类型转换 ( 自动转换规则, 手工转换规则 ) 等有关类型的研究形成了计算机科学中一个重要的研究领域 : 类型理论第 51 页

52 1 类型环境和类型断言类型判断的根据 : - 每个文字量都有自己的确定类型 - 变量函数等的声明提出了相关的类型要求 - 对类型合适的参数, 运算符函数将给出特定类型的结果 ( 注意 : 重载的运算符也有运算结果和运算对象之间的关系 ) 类型检查需要知道程序里所有变量的类型信息当前所有可见变量的类型信息的全体构成了当前的类型环境一个变量的类型信息用变量名和类型的对表示, 如 x 具有类型 T: 类型环境就是这种对的序列, 如 : 下面用 Γ ( 可能加下标 ) 表示类型环境第 52 页

53 1 类型推导我们用形式化的记法表示有关类型的断言类型断言有两种形式 : 在特定类型环境 Γ 下, 我们确定了表达式 e 的结果类型是 T ( 表达式 : 常量变量有结构成分的复杂表达式 ) 在环境 Γ 下命令 ( 语句 )c 是类型良好的 ( 基本语句如赋值, 各种复合语句和更复杂的程序结构 ) 为了作出程序中各种结构是否类型良好的判断, 确定有类型结构 ( 表达式 ) 的具体类型, 要定义一套做类型推断的规则 ( 类型规则 ), 说明如何得到程序中基本表达式的类型基于表达式的部分的类型推出整个表达式的类型然后基于表达式的类型, 推断基本语句是否类型良好 ; 基于基本语句的良类型性得到复合语句的良类型性不能推导出类型的表达式是类型错误的表达式, 对语句也一样第 53 页

54 1 类型规则下面用一个简单语言介绍类型规则的一些定义假定语言里有 int 和 double 类型变量声明, 赋值语句和结构语句类型规则包括 ( 例子 ): 基本规则 (1) 基本规则 (2) 第 54 页

55 1 类型规则表达式的类型规则 ( 一组 ): 语句的类型规则 ( 一组 ): 变量声明 : 其他规则可以类似写出第 55 页

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

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

58 2 环境和状态例 : 设当时环境中可见的变量是 x, y, z, 取值情况是 x 取值 3,y 取值 5,z 取值 0 这个状态就是有限函数 : 随着程序的执行, 特别是赋值语句的执行, 环境的状态就可能改变经过给 x 赋值 4, 给 y 赋值 1 的两个操作, 状态将变成 : 理解一个 ( 或一段 ) 程序的意义, 就是理解它在有关环境下的意义, 以及它的执行对环境的作用第 58 页

59 2 环境和状态严格些说, 一个环境是一个部分函数 : 为描述状态变化, 在环境上定义了一种覆盖操作 : 例 : 第 59 页

60 2 环境和状态对于常量 ( 如整数 ), 任何环境都给出它们的字面值环境确定一组变量的值, 就确定了基于这些变量构造的表达式的意义假定我们有 : 对于一般表达式 : 由于环境可以确定表达式的意义 ( 确定表达式的值 ) 我们也可以把环境看成从合法表达式到值集合的映射, 有些表达式的值无定义, 例如其中出现了在环境取值为无定义的变量, 或者求值中出现无定义运算结果 ( 如除数为 0) 等第 60 页

61 3 语义规格说明我们把程序的意义定义为它们对环境的作用为定义语义需要 : - 定义基本语句的意义 - 定义各种结构的意义如何由它们的组成部分得到有了这些定义, 就可以确定由这些语言结构构成的复杂程序的意义一个程序的执行导致环境的变化, 问题是如何严格定义这种变化人们提出了多种不同的形式化的语义定义方式 ( 技术 ): 操作语义 : 把程序运行看成执行了一系列改变环境的操作, 用一组描述环境变化的规则定义程序中各种结构的意义公理语义 : 用谓词描述状态, 用公理和推理规则描述各种基本操作和组合结构的语义指称语义 : 把程序的意义映射到某种的数学结构, 这种结构能清晰地表达程序对环境的作用和环境的变化代数语义 : 考虑程序之间的等价关系, 间接定义程序的意义第 61 页

62 操作语义 : 格局和规则首先需要定义格局 (configuration) 这里定义两种格局 : 终止格局, 就是一个环境, 表示代码运行完成时的状态非终止格局 : 表示程序运行中的一个状态一段程序代码 ( 待执行代码段 ) 和一个环境结构化操作语义 (SOS) 用一组格局变迁规则定义语言的语义可能包括一些无前提的规则和一些有前提的规则赋值语句的语义规则 ( 无前提规则 ): 复合语句的语义规则 ( 有前提规则 ): 第 62 页

63 操作语义 : 续 if 条件语句的语义规则 ( 两条 ): while 循环语句的语义规则 ( 两条 ): 上面这组规则严格地定义了一个理想的小语言的语义注意这个小语言的特点它与实际的程序语言还是有很大差距第 63 页

64 公理语义 R. Floyd 在 1967 年考虑如何说明一个程序完成了所需工作时, 提出用逻辑公式描述程序环境的状态的思想这种描述环境的逻辑公式称为断言逻辑公式 : 描述了状态 : 说明环境满足公式, 实际上, 这个状态还满足另外的许多逻辑公式, 如 : 反过来看, 一个逻辑公式可以被许多状态满足因此可以认为, 一个公式描述了一个状态集合例如, 上面第二个公式, 描第 64 页述了所有的其中 x 值是 1 的环境

65 公理语义 : 断言把断言写在程序里某个特定位置, 就是想提出一个要求 : - 程序执行到这个位置, 当时的环境状态必须满足断言 - 如果满足, 程序就正常向下执行 ( 就像没有这个断言 ) - 如果不满足, 程序就应该 ( 非正常地 ) 终止实例 : C 语言标准库提供了断言宏机制, 可以在程序里的写 assert(x > 0); Stroustrup 在 The C++ Programming Language 里特别讨论了如何定义断言类的问题有些语言本身提供了断言机制, 如 Eiffel 见 Design by Contract, 中译本 : 邮电出版社断言的概念在实际程序开发中起着越来越重要的作用第 65 页

66 公理语义 : 前条件和后条件如何借助于逻辑公式描述一段程序的意义? Hoare 提出的方法是用一对公式, 放在相应程序段之前和之后, 分别称为该程序段的前条件 (precondition) 和后条件 (postcondition) pre P post 意思是 : 如果在程序 P 执行之前条件 pre 成立 ( 当时的环境满足 pre), 那么在 P 执行终止时的环境中, 条件 post 一定成立我们可以用一对公式 (pre, post) 描述一段程序的语义, 也可以把这样的公式对 (pre, post) 看作是对一段程序的语义要求, 看作程序的规范... 前后条件的两种基本用途 : 作为评判程序是否正确的标准作为待开发的程序的规范, 研究如何从这种规范得到所需的程序第 66 页

67 公理语义 : 不变式不变式 ( 不变量,invariant) 的概念在许多领域中有重要地位程序理论中的不变式, 指写在程序里特定位置的逻辑公式, 要求程序执执行中每次达到某个 ( 某些 ) 情况时, 这个公式都必须成立其实, 不变式并不特殊, 因为写在程序里的断言, 也就是位于代码中相应特定位置的不变式, 情况就是执行达到这个位置程序理论里最重要的不变式之一是循环不变式 (loop invariant), 要求一个循环的每次迭代开始之前成立, 在描述和推导程序的意义时有特殊价值直接插入排序算法两重循环的不变式 ( 图示 ): 第 67 页

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

69 公理语义 :Hoare 逻辑 Hoare 逻辑是对有关程序意义的逻辑描述的整理和系统化 Hoare 逻辑中的逻辑公式形式为 ( 称为 Hoare 三元组 ): {p} S {q} 其中 p 和 q 是谓词逻辑公式,S 是一段程序直观意义 : 如果在 S 执行之前公式 p 成立, 在 S 执行终止时 q 就成立 Hoare 的最重要贡献是提出了一套推理规则, 通过这些规则, 可以把证明一个 Hoare 公式 ( 程序 S 相对于 p 和 q 的正确性 ) 的问题归结为证明一组普通一阶谓词逻辑公式的问题 Dijkstra 在此基础上提出了最弱前条件 (weakest precondition) 的概念, 借助于这一概念, 可以把程序的正确性证明工作进一步规范化用于做程序的推导 ( 从规范出发推导程序 ) 第 69 页

70 公理语义 :Hoare 逻辑公理 : 规则 [LOOP] 里的 I 是循环不变式第 70 页

71 公理语义 :Hoare 逻辑可以用 Hoare 逻辑证明程序的正确性, 也就是说, 证明三元组中的程序语句符合前后条件的要求其意义是 : 若在前条件满足的情况下执行语句且语句执行终止, 那么后条件满足这个证明并不保证语句终止, 如果语句的执行不终止, 什么后条件都可以证明因此, 这样证明的正确性称为部分正确性程序终止性需要另外证明, 主要是需要证明其中循环的执行必然终止如果同时证明程序的部分正确性和终止性, 这一程序就是完全正确的程序正确性证明中的一个关键点是为各个循环提供适当的不变式就像做数学归纳法证明中需要合适的归纳假设, 过强或过弱都不行人们已证明, 循环不变式不可能自动生成 ( 无完全的算法, 但有许多研究 ) 公理语义为我们提供了许多有助于理解程序行为的概念, 为设计程序时思考其行为提供了重要的依据和线索第 71 页

72 指称语义指称语义学 (denotational semantics) 有坚实的数学基础, 它的基本想法由 C.Strachey 提出,D. Scott 完成了它的基础理论并因此获图灵奖指称语义的基本思想是定义一个语义函数 ( 指称函数 ), 把程序的意义映射到某种意义清晰的数学对象 ( 就像用中文解释英文 ) 作为被指的数学对象可以根据需要选择对简单的程序语言, 一种自然的选择是把程序的语义定义为从环境到环境的函数 ( 作为指称 ) 定义语义就是指定每个程序对应的函数环境的集合 : 语义映射 : 表达式的语义 : 假设是整型表达式命令的语义 : 第 72 页

73 指称语义表达式的语义定义 : 语句的语义定义 : 第 73 页

74 代数语义代数语义把语义模型的集合看成是一个代数结构, 模型簇对应为代数系统用代数方法描述数据类型 A=(V, Op) specification LISTS sorts List NATURALS formal sort Component Operations empty_list : List cons(_,_) : Component,List List headof_ : List Component 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 第 74 页

75 语法语义和语用语法 : 规定合法程序的形式, 清晰定义语言中各种结构的形式上下文关系采用自然语言说明语义 : 规定合法程序的意义, 程序执行时所产生的效果形式语义学探讨形式化定义程序的语义语用 : 程序设计技术, 具体语言的使用技术和惯用方法程序设计技术技巧和设计模式等第 75 页

Microsoft PowerPoint - plan02.ppt

Microsoft PowerPoint - plan02.ppt 程序设计语言原理 Principle of Programming Languages 裘宗燕北京大学数学学院 2012.2~2012.6 2. 程序设计语言的定义语言的基本元素词法和语法语法的形式描述朴素的语义描述操作语义前后条件和 Hoare 公理指称语义 2012 年 2 月 2 语言的字符集大多数语言采用文本表示形式, 其中的程序就是字符的序列 ( 一维形式 ) 完全可以采用其他形式定义语言,