内容简介
本书系统地介绍了程序设计语言的形式语义学理论，涵盖了操作语义、指称语义和公理语义等主要形式化方法。书中从基本概念出发，深入探讨了如何用数学工具精确描述程序的行为和性质，为程序验证、编译器设计和语言设计提供了坚实的理论基础。
内容编排由浅入深，既适合作为计算机科学及相关专业的研究生和高年级本科生的教材，也可供从事程序设计语言理论、软件工程和形式化方法研究的科研人员参考。通过大量的实例和习题，读者可以逐步掌握形式语义的核心思想和技术，并学会将其应用于实际问题的分析和解决。
目录
第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 另一种语义
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.1 基本定义
第8章 域论
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.2 卫式命令
14.3 通信进程
14.4 米尔纳的CCS
14.5 纯CCS
14.6 规范语言
14.7 模态ν演算
14.8 局部模型检查
14.9 进一步阅读资料
附录A 不完备性和不可判定性
参考文献
第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.1 基本定义
第8章 域论
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.2 卫式命令
14.3 通信进程
14.4 米尔纳的CCS
14.5 纯CCS
14.6 规范语言
14.7 模态ν演算
14.8 局部模型检查
14.9 进一步阅读资料
附录A 不完备性和不可判定性
参考文献
重要申明：
本书由书友@锦小书发布分享，仅供学习交流使用，版权归原作者所有。如有侵权，请联系我们删除。
本书由书友@锦小书发布分享，仅供学习交流使用，版权归原作者所有。如有侵权，请联系我们删除。
📖 支持知识自由流动
每一本书的稳定访问，都离不开服务器、存储与带宽的长期维护。
