0去购物车结算
购物车中还没有商品，赶紧选购吧！
当前位置: 图书分类 > 信息技术 > 计算机理论 > 高级语言程序变换的机械化证明导论

相同语种的商品

销售排行榜

浏览历史

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


联系编辑
 
标题：
 
内容：
 
联系方式：
 
  
高级语言程序变换的机械化证明导论
  • 书号：9787030731678
    作者：何炎祥,江南
  • 外文书名：
  • 装帧：平装
    开本：B5
  • 页数：223
    字数：293000
    语种：zh-Hans
  • 出版社：科学出版社
    出版时间：2022-09-01
  • 所属分类：
  • 定价： ￥120.00元
    售价： ￥94.80元
  • 图书介质:
    纸质书

  • 购买数量： 件  可供
  • 商品总价：

相同系列
全选

内容介绍

样章试读

用户评论

全部咨询

随着现代社会信息化程度的提高，与计算机相关的各种系统故障足以造成巨大的经济损失。机械化的定理证明能够建立更为严格的正确性，从而奠定系统的高可信性。本书阐述机械化定理证明的逻辑基础和关键技术，分析比较各类主流证明助手的设计特点，重点讨论在编译器验证领域取得的重要研究成果，并以实例详述验证编译器的开发和实现。
样章试读
  • 暂时还没有任何用户评论
总计 0 个记录，共 1 页。 第一页 上一页 下一页 最末页

全部咨询(共0条问答)

  • 暂时还没有任何用户咨询内容
总计 0 个记录，共 1 页。 第一页 上一页 下一页 最末页
用户名： 匿名用户
E-mail：
咨询内容：

目录

  • 目录
    《信息科学技术学术著作丛书》序
    前言
    第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
帮助中心
公司简介
联系我们
常见问题
新手上路
发票制度
积分说明
购物指南
配送方式
配送时间及费用
配送查询说明
配送范围
快递查询
售后服务
退换货说明
退换货流程
投诉或建议
版权声明
经营资质
营业执照
出版社经营许可证

中国科技出版传媒股份有限公司　版权所有

　

京ICP备14028887号-5　 京ICP证150976号 京公网安备 11010102004214号

北京东黄城根北街16号 邮编：100717 Email:webmaster@mail.sciencep.com