登入帳戶　 |　訂單查詢　 |　購物車/收銀台(0)　|　在線留言板　 |　付款方式　 |　聯絡我們　 |　運費計算　 |　幫助中心　|　 加入書簽
	全部範圍 - 圖書 - 　- 中文簡體書(大陸書) - 　- 英文書（原版） - - 音碟 - 　- 音樂 - 　- 影視 - - 雜誌 - 全文 精確	會員登入   新用戶註冊

HOME新書上架暢銷書架好書推介特價區會員書架精選月讀2023年度TOP分類閱讀雜誌

香港／國際用戶

最新/最熱/最齊全的簡體書網

品種：超過100萬種書，正品正价，放心網購，悭钱省心

送貨：速遞 / 物流，時效：出貨後2-4日

新書推薦： 《 汉匈战争全史 》 售價：NT$ 454.0 《 恶的哲学研究（社会思想丛书） 》 售價：NT$ 500.0 《 当你沉默时（悬疑推理 反PUA 反家暴 女性独立小说，揭秘情感PUA的真相，女性自我救赎的文学典范） 》 售價：NT$ 255.0 《 不止江湖 》 售價：NT$ 449.0 《 天才留步！——从文艺复兴到新艺术运动（一本关于艺术天才的鲜活故事集，聚焦艺术史的高光时刻！） 》 售價：NT$ 704.0 《 双城史 》 售價：NT$ 505.0 《 冯友兰和青年谈心系列：不是问题的问题（哲学大师冯友兰和年轻人谈心，命运解读） 》 售價：NT$ 254.0 《 月与蟹（青鲤文库）荣获第144届直木奖，天才推理作家经典作品全新译本。一部青春狂想曲，带你登上心理悬疑之巅。 》 售價：NT$ 230.0

建議一齊購買： + NT$ 384 《 区块链基础知识25讲 》 + NT$ 153 《 大学计算机基础实验与习题 》 + NT$ 1219 《 软件研发效能权威指南 》 + NT$ 281 《 伽罗瓦理论之源流--群论建立者的故事、风格、作用 》 + NT$ 413 《 区块链技术及应用（第二版） 》 + NT$ 954 《 目标跟踪前沿理论与应用 》 內容簡介： 随着现代社会信息化程度的提高，与计算机相关的各种系统故障足以造成巨大的经济损失。机械化的定理证明能够建立更为严格的正确性，从而奠定系统的高可信性。《高级语言程序变换的机械化证明导论》阐述机械化定理证明的逻辑基础和关键技术，分析比较各类主流证明助手的设计特点，重点讨论在编译器验证领域取得的重要研究成果，并以实例详述验证编译器的开发和实现。 目錄： 目录《信息科学技术学术著作丛书》序前言第1章　机械化定理证明的原理和逻辑基础　11.1　基于消解的一阶逻辑自动定理证明　21.1.1　消解规则和证明　21.1.2　置换和合一　51.1.3　可满足性　61.1.4　消解证明技术的影响　61.2　自然演绎和Curry-Howard同构　71.2.1　自然演绎　71.2.2　类型化的？　演算　101.2.3　Curry-Howard同构　131.2.4　Curry-Howard同构的扩展　141.3　编程逻辑　151.3.1　编程语言的语义　161.3.2　一阶编程逻辑及变体　211.3.3　弗洛伊德-霍尔逻辑　251.3.4　可计算函数逻辑　261.4　基于高阶逻辑的硬件设计验证　271.4.1　高阶逻辑的硬件设计　291.4.2　高阶逻辑的硬件设计验证机制　311.5　程序构造和求精　321.5.1　算法和数据求精及基于不变式的程序构造　321.5.2　求精映射和行为时序逻辑　351.6　本章小结　36参考文献　37第2章　证明助手的开发和实现　462.1　证明助手的设计特点比较　472.2　Isabelle的开发和实现　492.2.1　Isabelle开发背景　502.2.2　Isabelle/Pure启动　512.2.3　Isabelle/Pure元逻辑　522.2.4　内部语法分析和变换　592.2.5　外部语法分析和Isar/VM解释器　662.3　Isabelle/HOL的开发和实现　732.3.1　Isabelle/HOL核心逻辑　732.3.2　Isabelle/HOL推理规则　762.3.3　Isabelle/HOL高级定义性机制　772.3.4　Isabelle/HOL证明工具　822.4　其他证明助手的设计和开发　842.4.1　Coq　842.4.2　NuPRL　852.4.3　ACL2　852.4.4　PVS　862.5　本章小结　86参考文献　87第3章　机械化定理证明的应用研究　893.1　数学证明的机械化　893.1.1　开普勒猜想　913.1.2　四色定理　923.1.3　质数定理　923.2　编译器验证　933.2.1　可信编译概述　933.2.2　编译器自身的正确性验证　953.2.3　编译后代码的正确性验证　1013.2.4　Jinja编译器分析　1033.2.5　CompCert编译器后端分析　1333.3　操作系统微内核验证　1433.3.1　安全的操作系统微内核源程序　1443.3.2　微内核源程序到ARM机器码的翻译确认　1453.4　硬件设计验证　1473.4.1　基于Boyer-Moore计算逻辑的硬件设计验证　1483.4.2　基于高阶逻辑的硬件设计验证　1483.5　本章小结　149参考文献　149第4章　验证编译器的开发和实现　1554.1　简单算术表达式编译器的正确性　1554.1.1　单遍编译算术表达式　1554.1.2　两遍编译算术表达式　1584.2　简单命令式语言IMP的验证编译器　1604.2.1　IMP的抽象语法　1604.2.2　IMP的大步操作语义　1614.2.3　IMP的编译目标语言　1634.2.4　编译及正确性证明　1654.3　IMP程序优化变换的正确性　1724.3.1　等同和条件等同　1724.3.2　常量折叠和传播　1734.3.3　改进的常量折叠和传播　1784.3.4　活性分析和消除冗余赋值语句　1814.3.5　改进的活性分析　1854.4　基于寄存器传输语言优化变换的正确性　1874.4.1　构建控制流图　1874.4.2　常量传播　1974.4.3　公共子表达式消除　2024.5　本章小结　207参考文献　207第5章　总结和展望　2085.1　总结　2085.2　展望　2095.2.1　编程语言的设计和实现　2095.2.2　并发程序的机械化证明　2145.2.3　面向对象语言的编译器验证　2175.2.4　更加强大的证明助手的开发　218参考文献　219

書城介紹　 |　合作申請　|　索要書目　 |　新手入門　|　聯絡方式　 |　幫助中心　|　找書說明　 |　送貨方式　|　付款方式	台灣用户　|　香港/海外用户
megBook.com.tw
Copyright (C) 2013 - 2024 （香港）大書城有限公司　All Rights Reserved.