书籍详情
![《高级语言程序变换的机械化证明导论何炎祥技出版传媒股份有限公司计算机与互联》[44M]百度网盘|亲测有效|pdf下载](/uploads/2024-01-20/b371e41d0118c55a.jpg)
高级语言程序变换的机械化证明导论何炎祥技出版传媒股份有限公司计算机与互联
- 出版社:青草书店专营店
- 出版时间:2021-03
- 热度:12511
- 上架时间:2024-06-30 09:38:03
- 价格:0.0
书籍下载
书籍预览
免责声明
本站支持尊重有效期内的版权/著作权,所有的资源均来自于互联网网友分享或网盘资源，一旦发现资源涉及侵权，将立即删除。希望所有用户一同监督并反馈问题，如有侵权请联系站长或发送邮件到ebook666@outlook.com,本站将立马改正
内容介绍
| 商品基本信息，请以下列介绍为准 | |
| 商品名称： | 高级语言程序变换的机械化证明导论 |
| 作者： | 何炎祥,江南 |
| 定价： | 1.0 |
| 出版社： | 技出版传媒股份有限公司 |
| 出版日期： | 21-03-01 |
| ISBN： | 9787030731678 |
| 印次： | |
| 版次： | 1 |
| 装帧： | 平装 |
| 开本： | B5 |
| 内容简介 |
| 随着现代社会信息化程度的提高，与计算机相关的各种系统故障足以造成巨大的经济损失。机械化的定理证明能够建立更为严格的正确性，从而奠定系统的高可信性。本书阐述机械化定理证明的逻辑基础和关键技术，分析比较各类主流证明助手的设计特点，讨论在编译器验证领域取得的重要研究成果，并以实例详述验证编译器的开发和实现。本书可供计算机科学与技术、信息、软件工程、计算机应用技术等相关专业的高年级本科生和研究生学可供从事机械化定理证明、可信软件及相关领域的研究人员参考。 |
| 目录 |
| 《信息科学技术学术著作丛书》序 前言 第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 Ielle的开发和实现 2.2.abelle开发背景 2.2.2 Ielle/Pure启动 2.2.3 Ielle/Pure元逻辑 2.2.4 内部语法分析和变换 2.2.5 外部语法分析和Isar/VM解释器 2.3 Ielle/HOL的开发和实现 2.3.abelle/HOL核心逻辑 2.3.2 Ielle/HOL推理规则 2.3.3 Ielle/HOL高级定义性机制 2.3.4 Ielle/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 四色定理 3.1.3 质数定理 3.2 编译器验证 3.2.1 可信编译概述 3.2.2 编译器自身的正确性验证 3.2.3 编译后代码的正确性验证 3.2.4 Jinja编译器分析 3.2.5 CompCert编译器后端分析 3.3 操作系统微内核验证 3.3.1 的操作系统微内核源程序 3.3.2 微内核源程序到ARM机器码的翻译确认 3.4 硬件设计验证 3.4.1 基于Boyer-Moore计算逻辑的硬件设计验证 3.4.2 基于高阶逻辑的硬件设计验证 3.5 本章小结 参考文献 第4章 验证编译器的开发和实现 4.1 简单算术表达式编译器的正确性 4.1.1 单遍编译算术表达式 4.1.2 两遍编译算术表达式 4.2 简单命令式语言IMP的验证编译器 4.2.1 IMP的抽象语法 4.2.2 IMP的大步操作语义 4.2.3 IMP的编译目言 4.2.4 编译及正确性证明 4.3 IMP程序优化变换的正确性 4.3.1 等同和条件等同 4.3.2 常量折叠和传播 4.3.3 的常量折叠和传播 4.3.4 活性分析和消除冗余赋值语句 4.3.5 的活性分析 4.4 基于寄存器传输语言优化变换的正确性 4.4.1 构建控制流图 4.4.2 常量传播 4.4.3 公共子表达式消除 4.5 本章小结 参考文献 第5章结和展望 5.1结 5.2 展望 5.2.1 编程语言的设计和实现 5.2.2 并发程序的机械化证明 5.2.3 面向对象语言的编译器验证 5.2.4 更加强大的证明助手的开发 参考文献 |