机读格式显示(MARC)

• 000 01211nam 22002891 450

• 001 0000446562

• 005 20231212162700.0

• 010 __ |a 978-7-03-073167-8 |d CNY120.00

• 100 __ |a 20231120d2022 em y0chiy50 ea

• 101 0_ |a chi

• 102 __ |a CN |b 110000

• 105 __ |a a a 000yy

• 106 __ |a r

• 200 1_ |a 高级语言程序变换的机械化证明导论 |A gao ji yu yan cheng xu bian huan de ji xie hua zheng ming dao lun |f 何炎祥, 江南著

• 210 __ |a 北京 |c 科学出版社 |d 2022.09

• 215 __ |a 223页 |c 图 |d 24cm

• 225 2_ |a 信息科学技术学术著作丛书 |A xin xi ke xue ji shu xue shu zhu zuo cong shu

• 320 __ |a 有书目

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

• 410 _0 |1 2001 |a 信息科学技术学术著作丛书

• 606 0_ |a 高级语言 |A gao ji yu yan |x 程序设计

• 690 __ |a TP311.1 |v 5

• 690 __ |a TP312.8 |v 5

• 701 _0 |a 何炎祥 |A he yan xiang |4 著

• 701 _0 |a 江南 |A jiang nan |4 著

• 801 _0 |a CN |b 辽批 |c 20231120

• 905 __ |a AUSTL |d TP311.1/H936