无

在给出程序设计语言的形式语义时，我们应当着重于建立一个数学模型。目的是使其作为理解程序以及对程序的行为进行推导的基础。数学模型不仅对于各种各样的分析和验证是有用的，同时在更为基础的层次上，应认识到数学模型的重要性在于通过它来精确地刻画程序结构的含义时更能显示出各种精妙细微之处。本书主要介绍支撑形式语义学的数学理论、技术和概念。
　　由于历史的原因，人们通常认为程序设计语言的语义由三条主线构成：
　　操作语义通过规定在抽象机器上的执行过程来描述程序设计语言的含义。我们侧重于“结构化操作语义”，这是Gordon Plotkin在Aarhus的演讲中提倡的方法，由规则规定求值和执行的关系，它是语法制导的。
　　指称语义是由Christopher Strachey首先提出的一种定义程序设计语言含义的技术，Dana Scott 奠定了它的数学基础。由于使用了完全偏序、连续函数和最小不动点等更为抽象的数学概念，曾一度被称为“数学语义”。
　　公理语义试图通过在程序逻辑的范围内给出证明规则来确定程序设计构造的含义，该方法的代表人物是R.W.Floyd和C.A.R.Hoare。因此，从一开始，公理语义就强调正确性的证明.
　　然而，将这三种类型的方法看作是彼此对立的观点是错误的. 它们各有各的用处. 一个清晰的操作语义有助于语言的实现. 公理语义对于特定类型的语言可以给出十分优美的证明系统，对开发和验证程序同样是有用的。在强大的数学理论支持下，指称语义提供了最有深度和最为广泛的可应用技术。事实上，这些不同的语义类型是高度相互依赖的。例如，要证明公理语义的证明规则是正确的，必须依赖于基本的指称语义或操作语义。要证明语言的实现是正确的，正是要依据指称语义去判断，要求证明操作语义和指称语义是一致的。同时，关于操作语义的论证对使用指称语义有巨大的帮助，指称语义往往远离不重要的实现细节，有着比较抽象的优势，可以给出用来理解计算行为的高层概念。近几年的研究使这几个不同的方法有望得到统一，我们希望能看到一种途径，使指称语义、操作语义和程序逻辑携手共同发展。本书的一个目标已经表明了操作语义和指称语义是如何结合在一起的。
　　语义学使用的技术绝大多数是依赖于数理逻辑的。如果没有一个好的逻辑知识背景，这些技术并不总能很容易地被计算机科学或数学专业的学生所接受。在这里，我们试图提供一个可能是周到的当然也是基本的方式。例如，在对操作语义作了介绍之后，引出了归纳定义的论述和推导操作语义的技术，从而使我们处于一个很好的境地，进一步学习抽象的指称语义的基础—完全偏序和连续函数。从操作语义的有限规则到集合上的连续算子，再到连续函数，这种过渡安排有助于理解为什么可计算函数要求有连续性。关于各种归纳原理，包括更一般的良基递归原理的论述，对于用良基关系定义集合上的函数是很重要的。在对递归类型语言的更为深入的研究中，利用信息系统不仅可以给出求解递归域方程的一个基本方法，同时还产生了能结合操作语义和指称语义的技术。

本书简介
　　本书以作者在Combridge 和Aarhus 大学的讲座内容为基础，主要针对计算机科学和数学专业的大学生和研究生而作，在他们开始学习形式化和推导程序设计语言的方法时可作为教材。本书介绍了必要的数学背景知识，读者可以运用它们去创造、形式化和证明一些规则，使用这些规则可推导各种各样的程序设计语言。本书的内容是基础的，但其中有一些来自于最近的研究。书中包含了从简单到复杂的众多丰富的练习。
　　本书首先介绍集合论基础，接着是结构化操作语义，并将其作为定义程序设计语言含义的一种方式，同时也介绍了一些基本的证明技术。而对指称语义和公理语义，以一个简单的while 循环语言为例进行说明，并给出了操作语义和指称语义之间等价的完整证明，以及公理语义的可靠性和相对完备性，也包括哥德尔不完备性定理的一个证明。该定理强调公理语义不可能达到绝对的完备性，这一结论可以在附录中得到支持，附录基于while循环语言介绍了可计算理论。在域论之后，介绍了指称语义的基础，论述了几种函数式语言的语义及其证明方法。最简单的函数式语言是既可以传值调用也可以传名调用求值计算的递归方程。这些研究工作可以进一步扩展到含有高阶类型和递归类型的语言，其中包括对活性和惰性λ演算的论述。本书始终强调指称语义和操作语义的联系，并给出它们的一致性证明。本书较先进的部分之一—递归类型的论述要利用信息系统来表示论域。在最后一章里介绍了并行程序设计语言，并讨论了不确定性和并行程序的验证方法。

本书的使用
　　下面标明的各章节的依赖关系，希望有助于本书的阅读、参考和讲课内容的取舍。例如，“逻辑和计算” 课程的内容可以只用1到7章以及附录。附录包含了第7章要用到的概念, 如果读者已学习过这方面的知识，则可以绕过附录。此外，象“语义学介绍” 这样的课程只用1 到5 章的内容就可以了，也可以加上第14章。第8，10，12章的内容可作为“域论” 课程的基础内容，有时可能要简单地引用一下第5 章的内容。第8到13章可以作为“函数式程序设计的数学基础” 课程的内容。第14章相对独立，大体上，只加上第2章就可以作为“不确定性和并行性” 课程的概论，只是关于模型检查的讨论要用到克纳斯特—塔尔斯基定理，它的证明在第5章。
　　有一些练习包含了一些小的实现任务。在Aarhus 的课上发现使用Prolog语 言很有帮助，可以举出例子，使前面的操作语义讲述更为生动。在讲述后面章节的语言时，用标准ML 语言或Miranda 语言可能更合适一些。

致谢
　　首先，我要感谢Dana Scott和Gordon Plotkin所做的基础性工作，它们从根本上影响了本书。如果阅读本书时条理清楚，是因为本书受到Gordon Plotkin的工作，尤其是他在Edinbrugh 大学关于完全偏序和指 称语义演讲稿的极大影响。
　　在Combadge，Tom Melham，Ken Moody，Larry Paulson 和Andy Pitts的评论意见对我很有帮助(特别是Andy的讲稿和对Eugenio Moggi工作的评论意见都已写进了域论一章中)。在Aarhus，Mogens Nielsen 提供了有价值的反馈和鼓励，他用最早的草稿开设了课程。Erik Meineche Schmidt 的建议改进了相对完备性定理和哥德尔定理的证明。在Aarhus，众多的学生提供了改正和建议，我要特别感谢Henrik Reif Andersen，Torben Brauner，Christian Clausen，Allan Cheng，Urban Engberg，Torben Amtoft Hansen，Ole Hougaard 和Jakob Seligman。非常感谢Bettina Blaaberg Sørensen，在准备本书的各个阶段，她都快速地阅读并提出建议。感谢Douglas Gurr对域论有关的章节提出了诚恳的批评意见。Kim Guldstrand Larsen对不确定性和并行性一章提出了改进意见。
在1991年的秋季，Albert Meyer以本书为基础开设了课程，他和其他教师A.Lent，M.Sheldon 和C.Yoder，非常友善地对打字稿中证明结构的调整给出了很多宝贵的意见。另外，Albert 慷慨地提供了可计算理论的讲稿，作为附录的基础。我感谢他们，但愿他们对最后的结果不感到失望。
　　感谢Karen Møller 在打字上提供的帮助。最后，向MIT 出版社，特别是Terry Ehling，对他们的耐心表示感谢。

各章之间的关系
　　● 第1章　集合论基础
　　● 第2章　操作语义
　　● 第3章　归纳原理
　　● 第4章　归纳定义
　　● 第5章　IMP的指称语义
　　● 第6章　IMP的公理语义
　　● 第7章　霍尔规则的完备性
　　● 第8章　域论
　　● 第9章　 递归方程
　　● 第10章　递归技术
　　● 第11章　高阶类型语言
　　● 第12章　信息系统
　　● 第13章　递归类型
　　● 第14章　不确定性和并行性
　　● 附录A　 不完备性和不可判定性

Glynn Winskel：Glynn Winskel: 曾任丹麦Aarhus大学计算机科学系教授，计算机科学基础研究中心(BRICS)主任，现任剑桥大学计算机实验室教授。

宋国新 邵志清 等：宋国新: 教授，博士生导师。1945年生，1968年毕业于华东水利学院水港系，1983年毕业于上海交通大学计算机软件专业，获工学硕士学位。1983-1987年在上海交通大学计算机系任教，1987年至今在华东理工大学信息学院计算机系任教。1991-1993年在美国休斯顿大学计算机系作访问学者。曾任华东理工大学计算机系主任兼计算中心主任，现任信息学院副院长，计算机研究所所长。主要研究程序验证、软件测试、软件开发方法、嵌入式系统软硬件协同设计等方向。主持“并行程序的验证”等多项国家自然基金和863项目的研究工作。已在国内外主要学术刊物上发表论文30多篇。获教育部科技进步二等奖两项，国家教学改革成果二等奖一项，上海市教学改革成果一等奖一项。
邵志清: 教授，博士生导师，现任华东理工大学计算机科学与工程系系主任。1966年生，1986年毕业于南京大学数学系，获理学学士学位；1989年毕业于中国科学院软件研究所，获理学硕士学位；1998年毕业于上海交通大学计算机科学与工程系，获工学博士学位。2001-2002年以国家杰出访问学者身份赴美国Rensselaer Polytechnic Institute计算机系进行合作研究。主持国家自然科学基金项目等多项课题，发表学术论文60多篇，获教育部科技进步二等奖。出版教材《离散数学》，受聘为教育部高等学校本科教学工作水平评估中青年专家，获国务院政府特殊津贴、霍英东教育基金会高等院校青年教师奖、上海市高校优秀青年教师等奖励。

“计算机科学与技术”这一门学科，顾名思义，要求计算机工作者既具有坚实的计算机基础理论方面的科学涵养，又具有熟练解决实际问题的综合技术。几十年来，理论计算机科学
方面的研究结果，为计算机技术与应用的发展提供了有力的支撑; 同样，迅速发展的应用领域又为理论工作者提出了更多更新的课题。实践表明，正是理论与应用的紧密联系和相互渗透，才使得计算机学科不断向前蓬勃发展。
　　程序设计语言是计算机学科的一个重要组成部分，是理论与应用紧密联系的典型。程序设计语言的每一次技术飞跃都极大地推动了整个计算机学科的发展。尽管程序设计语言品种繁多、层次不一，但总体上讲，与之相关的人有三类：一类是程序设计语言的设计者，他们针对不同的应用定义语言的成分要素; 另一类是程序设计语言的实现者，他们针对具体的机器提出语言的实现方案; 再一类是程序设计语言的使用者，他们针对具体的问题进行程序设计以给出相应的解决方案。这样，人们可以从各种不同的角度来观察和刻画程序设计语言，从而导致三种主要的理解方式：指称语义、操作语义和公理语义。这三种语义的精确描述需要严密的数学工具。在长期的数学工具的寻找过程中，逐渐形成了有关域论、推导规则、正确性断言等方面的理论和方法，奠定了形式语义学的基础。
　　本书涉及的程序设计语言既包括命令式(imperative) 语言又包括函数式(functional)语言，既包括顺序(sequential)语言又包括并行(parallel)语言，既包括确定性(deterministic)语言又包括不确定性(nondeterministic)语言。书中介绍了支撑这些语言的形式语义的数学理论、方法和概念。读者掌握了这些必要的数学知识，能运用它们去创造规则、刻画规则和证明规则，从而可以描述和推导各类程序设计语言的各种成分和性质。
　　本书第1章到第10章由潘俊和宋国新翻译，第11章到第14章由孙霖和宋国新翻译，附录由丁志义翻译，全书由宋国新和邵志清负责整理和统译。译者十分感谢本书的责任编辑杨海玲的细心校阅，她指出了原始译本中多处符号与原著的不一致。
　　本书结构合理、内容丰富、蔚为大观，是一本难得的形式语义学经典著作和教材。译者
在翻译过程中获益良多，但限于译者水平，译本中错误和疏漏之处在所难免。读者如果发现译本中有错误，请与译者联系：gxsong@ecust.edu.cn或zshao@ecust.edu.cn。

　　　　　　　　　　　　　　　　　　　　译者于华东理工大学　　
　　　　　　　　　　　　　　　　　　　　　 2003年11月28日
　　　　　　　　　　　　　　　　　　　　　　　

第1章 集合论基础
1.1 逻辑记号
1.2 集合
1.2.1集合与性质
1.2.2 一些重要集合
1.2.3 集合构造
1.2.4 基本公理
1.3 关系与函数
1.3.1 Λ记号
1.3.2 复合关系与复合函数
1.3.3 关系的正象与逆象
1.3.4 等价关系
1.4 进一步阅读

第2章 操作语义
2.1 IMP——一种简单的命令式语言
2.2 算术表达式的求值
2.3 布尔表达式的求值
2.4 命令的执行
2.5 一个简单的证明
2.6 另一种语义
2.7 进一步阅读

第3章 归纳原理
3.1数学归纳法
3.2结构归纳法
3.3良基归纳法
3.4对推导的归纳
3.5归纳定义
3.6进一步阅读

第4章 归纳定义
4.1规则归纳法
4.2特殊的规则归纳法
4.3操作语义的证明规则
4.3.1 算术表达式的规则归纳法
4.3.2 布尔表达式的规则归纳法
4.3.3 命令的规则归纳法
4.4算子及其最小不动点
4.5进一步阅读

第5章 IMP的指称语义
5.1目的
5.2指称语义
5.3语义的等价性
5.4完全偏序与连续函数
5.5克纳斯特–塔尔斯基定理
5.6进一步阅读

第6章 IMP的公理语义
6.1基本思想
6.2断言语言 Assn
6.2.1 自由变量与约束变量
6.2.2代入
6.3断言的语义
6.4部分正确性的证明规则
6.5可靠性
6.6应用霍尔规则的实例
6.7进一步阅读

第7章 霍尔规则的完备性
7.1哥德尔不完备性定理
7.2最弱前置条件与可表达性
7.3哥德尔定理的证明
7.4验证条件
7.5谓词转换器
7.6进一步阅读

第8章 域论
8.1基本定义
8.2一个例子 —— 流
8.3完全偏序上的构造
8.3.1离散完全偏序
8.3.2有限积
　8.3.3函数空间
　8.3.4提升
8.3.5和
8.4元语言
8.5进一步阅读

第9章 递归方程
9.1 REC语言
9.2 传值调用的操作语义
9.3 传值调用的指称语义
9.4 传值调用的语义等价
9.5 传名调用的操作语义
9.6 传名调用的指称语义
9.7 传名调用的语义等价
9.8 局部声明
9.9 进一步阅读

第10章 递归技术
10.1 贝伊克定理
10.2 不动点归纳法
10.3 良基归纳
10.4 良基递归
10.5 一个练习
10.6 进一步阅读

第11章 高阶类型语言
11.1 活性语言
11.2 活性操作语义
11.3 活性指称语义
11.4 活性语义的一致性
11.5 惰性语言
11.6 惰性操作语义
11.7 惰性指称语义
11.8 惰性语义的一致性
11.9 不动点算子
11.10 观察与完全抽象
11.11 和
11.12 进一步阅读

第12章 信息系统
12.1递归类型
12.2信息系统
12.3闭族与斯科特前域
12.4信息系统的完全偏序
12.5构造
12.5.1 提升
12.5.2 和
12.5.3 积
12.5.4 提升函数空间
12.6进一步阅读

第13章 递归类型
13.1 活性语言
13.2 活性操作语义
13.3 活性指称语义
13.4 活性语义的充分性
13.5　活性λ演算
13.5.1 等价理论
13.5.2 不动点操作
13.6 惰性语言
13.7 惰性操作语义
13.8 惰性指称语义
13.9 惰性语言的充分性
13.10 惰性λ演算
13.10.1 等价理论
13.10.2 不动点操作
13. 11 进一步阅读

第14章 不确定性和并行性
14.1 引言
14.2 卫式命令
14.3 通信进程
14.4 米尔纳的CCS
14.5 纯CCS
14.6 规范语言
14.7 模态υ演算
14.8 局部模型检查
14.9 进一步阅读

附录A 不完备性和不可判定性
参考文献
术语表