孔夫子旧书网-网上买书卖书、古旧书收藏品交易平台 孔夫子旧书网-网上买书卖书、古旧书收藏品交易平台 占位居中 孔夫子旧书网-网上买书卖书、古旧书收藏品交易平台
商品
拍卖区
在售
已售
搜索历史
搜索
高级搜索

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

高级语言程序变换的机械化证明导论
分享
扫描下方二维码分享到微信
打开微信，点击右上角”+“，
使用”扫一扫“即可将网页分享到朋友圈。
作者: 著 , 著
出版社: 科学出版社
2022-09
版次: 1
ISBN: 9787030731678
装帧: 平装
开本: 16开
纸张: 胶版纸
页数: 223页
正文语种: 简体中文
丛书: 信息科学技术学术著作丛书
分类: 计算机与互联网
1人买过
  • 随着现代社会信息化程度的提高，与计算机相关的各种系统故障足以造成巨大的经济损失。机械化的定理证明能够建立更为严格的正确性，从而奠定系统的高可信性。《高级语言程序变换的机械化证明导论》阐述机械化定理证明的逻辑基础和关键技术，分析比较各类主流证明助手的设计特点，重点讨论在编译器验证领域取得的重要研究成果，并以实例详述验证编译器的开发和实现。 目录 

    《信息科学技术学术著作丛书》序 

    前言 

    第1章 机械化定理证明的原理和逻辑基础 1 

    1.1 基于消解的一阶逻辑自动定理证明 2 

    1.1.1 消解规则和证明 2 

    1.1.2 置换和合一 5 

    1.1.3 可满足性 6 

    1.1.4 消解证明技术的影响 6 

    1.2 自然演绎和Curry-Howard同构 7 

    1.2.1 自然演绎 7 

    1.2.2 类型化的？ 演算 10 

    1.2.3 Curry-Howard同构 13 

    1.2.4 Curry-Howard同构的扩展 14 

    1.3 编程逻辑 15 

    1.3.1 编程语言的语义 16 

    1.3.2 一阶编程逻辑及变体 21 

    1.3.3 弗洛伊德-霍尔逻辑 25 

    1.3.4 可计算函数逻辑 26 

    1.4 基于高阶逻辑的硬件设计验证 27 

    1.4.1 高阶逻辑的硬件设计 29 

    1.4.2 高阶逻辑的硬件设计验证机制 31 

    1.5 程序构造和求精 32 

    1.5.1 算法和数据求精及基于不变式的程序构造 32 

    1.5.2 求精映射和行为时序逻辑 35 

    1.6 本章小结 36 

    参考文献 37 

    第2章 证明助手的开发和实现 46 

    2.1 证明助手的设计特点比较 47 

    2.2 Isabelle的开发和实现 49 

    2.2.1 Isabelle开发背景 50 

    2.2.2 Isabelle/Pure启动 51 

    2.2.3 Isabelle/Pure元逻辑 52 

    2.2.4 内部语法分析和变换 59 

    2.2.5 外部语法分析和Isar/VM解释器 66 

    2.3 Isabelle/HOL的开发和实现 73 

    2.3.1 Isabelle/HOL核心逻辑 73 

    2.3.2 Isabelle/HOL推理规则 76 

    2.3.3 Isabelle/HOL高级定义性机制 77 

    2.3.4 Isabelle/HOL证明工具 82 

    2.4 其他证明助手的设计和开发 84 

    2.4.1 Coq 84 

    2.4.2 NuPRL 85 

    2.4.3 ACL2 85 

    2.4.4 PVS 86 

    2.5 本章小结 86 

    参考文献 87 

    第3章 机械化定理证明的应用研究 89 

    3.1 数学证明的机械化 89 

    3.1.1 开普勒猜想 91 

    3.1.2 四色定理 92 

    3.1.3 质数定理 92 

    3.2 编译器验证 93 

    3.2.1 可信编译概述 93 

    3.2.2 编译器自身的正确性验证 95 

    3.2.3 编译后代码的正确性验证 101 

    3.2.4 Jinja编译器分析 103 

    3.2.5 CompCert编译器后端分析 133 

    3.3 操作系统微内核验证 143 

    3.3.1 安全的操作系统微内核源程序 144 

    3.3.2 微内核源程序到ARM机器码的翻译确认 145 

    3.4 硬件设计验证 147 

    3.4.1 基于Boyer-Moore计算逻辑的硬件设计验证 148 

    3.4.2 基于高阶逻辑的硬件设计验证 148 

    3.5 本章小结 149 

    参考文献 149 

    第4章 验证编译器的开发和实现 155 

    4.1 简单算术表达式编译器的正确性 155 

    4.1.1 单遍编译算术表达式 155 

    4.1.2 两遍编译算术表达式 158 

    4.2 简单命令式语言IMP的验证编译器 160 

    4.2.1 IMP的抽象语法 160 

    4.2.2 IMP的大步操作语义 161 

    4.2.3 IMP的编译目标语言 163 

    4.2.4 编译及正确性证明 165 

    4.3 IMP程序优化变换的正确性 172 

    4.3.1 等同和条件等同 172 

    4.3.2 常量折叠和传播 173 

    4.3.3 改进的常量折叠和传播 178 

    4.3.4 活性分析和消除冗余赋值语句 181 

    4.3.5 改进的活性分析 185 

    4.4 基于寄存器传输语言优化变换的正确性 187 

    4.4.1 构建控制流图 187 

    4.4.2 常量传播 197 

    4.4.3 公共子表达式消除 202 

    4.5 本章小结 207 

    参考文献 207 

    第5章 总结和展望 208 

    5.1 总结 208 

    5.2 展望 209 

    5.2.1 编程语言的设计和实现 209 

    5.2.2 并发程序的机械化证明 214 

    5.2.3 面向对象语言的编译器验证 217 

    5.2.4 更加强大的证明助手的开发 218 

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

    《信息科学技术学术著作丛书》序 

    前言 

    第1章 机械化定理证明的原理和逻辑基础 1 

    1.1 基于消解的一阶逻辑自动定理证明 2 

    1.1.1 消解规则和证明 2 

    1.1.2 置换和合一 5 

    1.1.3 可满足性 6 

    1.1.4 消解证明技术的影响 6 

    1.2 自然演绎和Curry-Howard同构 7 

    1.2.1 自然演绎 7 

    1.2.2 类型化的？ 演算 10 

    1.2.3 Curry-Howard同构 13 

    1.2.4 Curry-Howard同构的扩展 14 

    1.3 编程逻辑 15 

    1.3.1 编程语言的语义 16 

    1.3.2 一阶编程逻辑及变体 21 

    1.3.3 弗洛伊德-霍尔逻辑 25 

    1.3.4 可计算函数逻辑 26 

    1.4 基于高阶逻辑的硬件设计验证 27 

    1.4.1 高阶逻辑的硬件设计 29 

    1.4.2 高阶逻辑的硬件设计验证机制 31 

    1.5 程序构造和求精 32 

    1.5.1 算法和数据求精及基于不变式的程序构造 32 

    1.5.2 求精映射和行为时序逻辑 35 

    1.6 本章小结 36 

    参考文献 37 

    第2章 证明助手的开发和实现 46 

    2.1 证明助手的设计特点比较 47 

    2.2 Isabelle的开发和实现 49 

    2.2.1 Isabelle开发背景 50 

    2.2.2 Isabelle/Pure启动 51 

    2.2.3 Isabelle/Pure元逻辑 52 

    2.2.4 内部语法分析和变换 59 

    2.2.5 外部语法分析和Isar/VM解释器 66 

    2.3 Isabelle/HOL的开发和实现 73 

    2.3.1 Isabelle/HOL核心逻辑 73 

    2.3.2 Isabelle/HOL推理规则 76 

    2.3.3 Isabelle/HOL高级定义性机制 77 

    2.3.4 Isabelle/HOL证明工具 82 

    2.4 其他证明助手的设计和开发 84 

    2.4.1 Coq 84 

    2.4.2 NuPRL 85 

    2.4.3 ACL2 85 

    2.4.4 PVS 86 

    2.5 本章小结 86 

    参考文献 87 

    第3章 机械化定理证明的应用研究 89 

    3.1 数学证明的机械化 89 

    3.1.1 开普勒猜想 91 

    3.1.2 四色定理 92 

    3.1.3 质数定理 92 

    3.2 编译器验证 93 

    3.2.1 可信编译概述 93 

    3.2.2 编译器自身的正确性验证 95 

    3.2.3 编译后代码的正确性验证 101 

    3.2.4 Jinja编译器分析 103 

    3.2.5 CompCert编译器后端分析 133 

    3.3 操作系统微内核验证 143 

    3.3.1 安全的操作系统微内核源程序 144 

    3.3.2 微内核源程序到ARM机器码的翻译确认 145 

    3.4 硬件设计验证 147 

    3.4.1 基于Boyer-Moore计算逻辑的硬件设计验证 148 

    3.4.2 基于高阶逻辑的硬件设计验证 148 

    3.5 本章小结 149 

    参考文献 149 

    第4章 验证编译器的开发和实现 155 

    4.1 简单算术表达式编译器的正确性 155 

    4.1.1 单遍编译算术表达式 155 

    4.1.2 两遍编译算术表达式 158 

    4.2 简单命令式语言IMP的验证编译器 160 

    4.2.1 IMP的抽象语法 160 

    4.2.2 IMP的大步操作语义 161 

    4.2.3 IMP的编译目标语言 163 

    4.2.4 编译及正确性证明 165 

    4.3 IMP程序优化变换的正确性 172 

    4.3.1 等同和条件等同 172 

    4.3.2 常量折叠和传播 173 

    4.3.3 改进的常量折叠和传播 178 

    4.3.4 活性分析和消除冗余赋值语句 181 

    4.3.5 改进的活性分析 185 

    4.4 基于寄存器传输语言优化变换的正确性 187 

    4.4.1 构建控制流图 187 

    4.4.2 常量传播 197 

    4.4.3 公共子表达式消除 202 

    4.5 本章小结 207 

    参考文献 207 

    第5章 总结和展望 208 

    5.1 总结 208 

    5.2 展望 209 

    5.2.1 编程语言的设计和实现 209 

    5.2.2 并发程序的机械化证明 214 

    5.2.3 面向对象语言的编译器验证 217 

    5.2.4 更加强大的证明助手的开发 218 

    参考文献 219
查看详情
相关分类
计算机理论 编程与开发 操作系统 大数据与云计算 图形图像/多媒体 网站设计与网页开发 网络与通讯 硬件、嵌入式开发 办公软件 信息安全 辅助设计与工程计算 软件工程/开发项目管理
12
系列丛书 / 更多
高级语言程序变换的机械化证明导论
信息科学技术学术著作丛书：大数据搜索与挖掘
高凯、黄河燕、赵燕平 著
￥1.50 起
高级语言程序变换的机械化证明导论
张量投票方法及其在机器视觉中的应用
邵晓芳、孙即祥、田素芬 著
￥26.40 起
高级语言程序变换的机械化证明导论
信息科学技术学术著作丛书：量子光学
张智明 著
￥28.00 起
高级语言程序变换的机械化证明导论
面向认知物联网的自律协同管理机制
郑瑞娟 著
￥15.00 起
高级语言程序变换的机械化证明导论
信息科学技术学术著作丛书：硅通孔3D集成技术
[美]刘汉诚（John H.Lau） 著
￥35.00 起
高级语言程序变换的机械化证明导论
数字水印技术及其应用
蒋天发 著
￥20.00 起
高级语言程序变换的机械化证明导论
查询推荐理论与方法
蔡飞、陈洪辉、蒋丹阳、陈皖玉 著
￥18.00 起
高级语言程序变换的机械化证明导论
微结构光纤设计、制备及应用
娄淑琴、李曙光 著
￥45.00 起
高级语言程序变换的机械化证明导论
开放式遥感数据处理软件平台OpenRS的设计与实现
江万寿、呙维、张靖 著
￥30.00 起
高级语言程序变换的机械化证明导论
移动通信系统中广播多播技术与应用
田霖、周一青、石晶林 著
￥40.00 起
高级语言程序变换的机械化证明导论
时空编码脉冲耦合神经网络理论及应用
顾晓东 著
￥57.00 起
高级语言程序变换的机械化证明导论
时滞动力学系统的分岔与混沌（下册）
廖晓峰、李传东、郭松涛 著
￥30.00 起
相关图书 / 更多
高级语言程序变换的机械化证明导论
高级财务会计学习指导与习题集（第三版）
黄中生、路国平 著
￥0.35 起
高级语言程序变换的机械化证明导论
高级英语1(第四版)同步测试
编者:王俊菊//王颖|责编:张阳
￥11.37 起
高级语言程序变换的机械化证明导论
高级项目经理手册——融合传统和敏捷的项目管理方法
许江林
￥36.50 起
高级语言程序变换的机械化证明导论
高级会计实务--2024年《会考》高级教材
财政部会计财务评价中心
￥51.00 起
高级语言程序变换的机械化证明导论
高级无线网络——技术及商业模式（第三版）
[芬兰]Savo G. Glisic( 萨沃 · G. 格里希奇
￥111.40 起
高级语言程序变换的机械化证明导论
高级会计实务全真模拟试题--2024年《会考》高级辅导
上海国家会计学院
￥15.49 起
高级语言程序变换的机械化证明导论
高级会计实务过关一本通--2024年《会考》高级辅导
上海国家会计学院
￥32.08 起
高级语言程序变换的机械化证明导论
高级会计实务知识点速查手册--2024年《会考》高级辅导
上海国家会计学院
￥11.95 起
高级语言程序变换的机械化证明导论
高级会计实务案例--2024年《会考》高级教材
财政部会计财务评价中心
￥19.00 起
高级语言程序变换的机械化证明导论
高级区域经济学（第五版）
安虎森
￥26.90 起
高级语言程序变换的机械化证明导论
高级法语教程（理工类）
周蕾 著
￥33.84 起
高级语言程序变换的机械化证明导论
高级哈萨克语（1）
张辉
￥11.00 起
您可能感兴趣 / 更多
高级语言程序变换的机械化证明导论
面向片上缓存子系统的功耗优化方法
何炎祥、沈凡凡 著
￥57.41 起
高级语言程序变换的机械化证明导论
信息科学技术学术著作丛书：面向嵌入式系统的绿色编译理论与方法研究
何炎祥、陈勇 著
￥37.50 起
高级语言程序变换的机械化证明导论
可信编译构造理论与关键技术
何炎祥；吴伟
￥45.00 起
高级语言程序变换的机械化证明导论
计算机操作系统（第2版）/普通高等教育“十一五”国家级规划教材·21世纪大学本科计算机专业系列教材
何炎祥 著
￥0.10 起
高级语言程序变换的机械化证明导论
计算机科学与技术学科研究生系列教材（中文版）：动态Web服务组合关键技术与性能分析
何炎祥 著
￥5.00 起
高级语言程序变换的机械化证明导论
编译原理（第3版）
何炎祥 编
￥0.50 起
高级语言程序变换的机械化证明导论
程序设计基础
何炎祥、石莹、王娜 编著
￥2.53 起
高级语言程序变换的机械化证明导论
高等学校研究生系列教材：分布式操作系统
何炎祥 编
￥15.00 起
高级语言程序变换的机械化证明导论
编译原理
何炎祥 著
￥0.10 起
高级语言程序变换的机械化证明导论
操作系统原理/新世纪计算机专业系列教材
何炎祥 编
￥12.00 起
高级语言程序变换的机械化证明导论
Agent和多Agent系统的设计与应用
何炎祥、陈莘萌 编著
￥3.00 起
高级语言程序变换的机械化证明导论
操作系统原理——上海“九五”重点图书出版规划项目全国名校计算机专业核心课程教材
何炎祥 编
￥8.00 起
© 2002-2024 Kongfz.com 孔夫子旧书网 版权所有
关于孔网 联系我们 帮助中心 版权隐私 广告业务 工作机会 移动版 图书目录 图书标签 热搜书籍 作家大全