高级语言程序变换的机械化证明导论

基本信息

• 商品名称： 语言程序变换的机械化证明导论
• 作者：何炎祥，江南
• 定价：120
• 出版社：科学
• 书号：9787030731678

其他参考信息（以实物为准）

• 出版时间：2022-10-01
• 印刷时间：2022-10-19
• 版次：31
• 印次：1
• 开本：
• 页数：236

内容提要

随着现代社会信息化程度的提高，与计算机相关的各种系统故障足以造成巨大的经济损失。机械化的定理证明能够建立 为严格的正确性，从而奠定系统的高可信性。本书阐述机械化定理证明的逻辑基础和关键技术，分析比较各类主流证明助手的设计特点，重点讨论在编译器验证领域取得的重要研究成果，并以实例详述验证编译器的开发和实现。

目录

《信息科学技术学术著作丛书》序
前言
第1章 机械化定理证明的原理和逻辑基础
1.1 基于消解的一阶逻辑自动定理证明
1.1.1 消解规则和证明
1.1.2 置换和合一
1.1.3 可满足性
1.1.4 消解证明技术的影响
1.2 自然演绎和Curry-Howard同构
1.2.1 自然演绎
1.2.2 类型化的□（数学字符）演算
1.2.3 Curry-Howard同构
1.2.4 Curry-Howard同构的扩展
1.3 编程逻辑
1.3.1 编程语言的语义
1.3.2 一阶编程逻辑及变体
1.3.3 弗洛伊德-霍尔逻辑
1.3.4 可计算函数逻辑
1.4 基于高阶逻辑的硬件设计验证
1.4.1 高阶逻辑的硬件设计
1.4.2 高阶逻辑的硬件设计验证机制
1.5 程序构造和求精
1.5.1 算法和数据求精及基于不变式的程序构造
1.5.2 求精映射和行为时序逻辑
1.6 本章小结
参考文献
第2章 证明助手的开发和实现
2.1 证明助手的设计特点比较
2.2 Isabelle的开发和实现
2.2.1 Isabelle开发背景
2.2.2 Isabelle/Pure启动
2.2.3 Isabelle/Pure元逻辑
2.2.4 内部语法分析和变换
2.2.5 外部语法分析和Isar/VM解释器
2.3 Isabelle/HOL的开发和实现
2.3.1 Isabelle/HOL核心逻辑
2.3.2 Isabelle/HOL推理规则
2.3.3 Isabelle/HOL 定义性机制
2.3.4 Isabelle/HOL证明工具
2.4 其他证明助手的设计和开发
2.4.1 Coq
2.4.2 NuPRL
2.4.3 ACL2
2.4.4 PVS
2.5 本章小结
参考文献
第3章 机械化定理证明的应用研究
3.1 数学证明的机械化
3.1.1 开普勒猜想
3.1.2 四色定理