形式语义学基础与形式说明
2010-3
科学出版社
屈延文
496
无
本书是计算机专业人员和大学软件、计算机科学和信息化科学专业高年级学生以及硕士研究生或博士研究生了解计算机科学理论在软件工程应用的专门书籍。作者站在软件的立场上来讨论计算机科学（尤其是形式语义学）的理论及其应用。虽然，我们比较详细地介绍了形式语义学基本理论框架，但它不是一本纯理论的书籍，而是一本理论联系实际的书籍；因此，在叙述中不苛求理论上的严密性。 作者在1980年，由于准备Ada语言的编译程序和环境工作以及对软件工程理论的关注，开始对形式语义学理论与实践进行研究。当时出版本书的目标是全面提高软件重用、软件自动生成和软件智能化的理论和技术水平。目前看来，这个目标现在仍然没有过时。在20世纪80年代初，作者用三册油印的讲义，经过多年在北京大学、北京航空学院（北京航空航天大学）、中国科学院研究生院、北京信息工程学院和华北计算技术研究所为研究生讲授此课；北京之外，在国防科技大学、武汉大学和其他大学也讲授过此课程。在多年研究和讲课的基础上，本书的内容更加完善。20世纪80年代后期科学出版社正式出版了《形式语义学基础与形式说明》一书。作为第一版，该书正式出版已经有20多年了，曾经两次印刷，多年来一直有人不断向作者寻求本书。在21世纪，信息化发展带来了科学发展的强大新动力，尤其是信息化科学学科的提出，冲破了经典计算机科学研究的范围，其中信息化和网络世界的安全是最突出的领域。信息安全不仅需要实施更加严格的产品保证计划，同时要求信息安全测评事业具有逐步达到高级别的安全测评能力，尤其是提高结构性和形式化验证能力，依此来推动我国信息系统产品质量的全面提升。所以，必须对信息化与安全产业和测评机构进行结构性和形式化验证方法的培训。再版本书是实施这种高素质培训的教材建设，再版工作被列为中国信息安全测评中心的自然科学基金项目内容之一。 本书再版还有更广泛和深刻的意义。在20世纪90年代，作者开始特别关注信息化体系结构和信息安全的理论问题。显然，信息化与网络世界中的大量问题，例如互操作性和安全性问题，已经不可能从经典的计算机科学理论中得到帮助和指导。信息化的体系结构已经不是计算机的体系结构，不是软件的体系结构，也不是应用系统的体系结构。信息化的体系结构概念要比这些方面的体系结构复杂得多。信息化体系结构的实践告诉我们，要划分运营、系统和技术三个视图来研究体系结构。经过多年研究，作者认为，运营体系结构，从理论的高度看，其核心的概念范畴是主体和行为，包括人类信息化行为和网络世界中的虚拟主体和行为。
本书第一版是20世纪80年代国家教委计算机软件专业教材编委会推荐教材之一。本书详细地给出了形式语义学的基础理论框架，但它并不是一本纯理论的教材，而是一本理论与软件实践相结合的教材。 全书共分十章。介绍了指称语义学、代数语义学、操作语义学与公理语义学的基本内容及其应用，并介绍了并发程序设计语言各流派的语义模型和新一代计算机计算模型的理论问题。例如curry的组合逻辑，Martin-Lof的直觉主义数学的讨论都是近代计算机理论较重要的基础内容。 本书内容丰富，重点突出，并配有大量习题，可作为高等院校电子信息、计算机科学专业本科高年级学生、研究生的教材，也可供信息技术人员和计算机软件设计、工程人员参考。
屈延文，现任中国信息安全产业商会机构常务副理事长，中国信息安全测评中心顾问和北京大学、武汉大学、华中科技大学等兼职教授，是信息化与安全总体咨询机构QNS工作室的主要成员之一。是中国CAD事业、软件工程与计算机科学和信息化科学的开拓者与主要的推动者之一，是我国计算机程序设计语言、操作系统和软件工程专家和中国著名计算机科学学者，参与并主持国家信息化多项重大工程建设工作。目前，他是信息化与安全的总体设计师，是中国信息安全产业标准化联盟总体组组长，主持可信网络世界体系结构框架（TCAF）标准体系的研究、制定和推动工作。同时，长期为国家培养了数量众多的计算机科学和信息化科学的高水平的科学与技术人才。
软件行为学、网络世界行为学科（形式行为学）的开创者。曾著有《形式语义学基础与形式说明》、《实用类型程序设计》、《软件行为学》、《信息化行为学理论基础与形式化方法》，主笔《银行行为监管》和《银行行为控制》等著作。
第1章 引论 1.1 形式语义学 1.2 指称语义学 1.3 代数语义学 1.4 操作语义学 1.5 公理语义方法 1.6 形式说明语言第2章 指称语义学基础 2.1 论域问题引子 2.2 域的构造 2.3 偏序与完全偏序 2.4 单调函数与连续函数 2.5 连续泛函 2.6 泛函不动点及递归程序 2.7 抽象及-演算 2.8 指称语义定义初步 习题 参考文献第3章 程序设计语言的指称语义 3.1 程序设计语言的基本概念 3.2 存储语义 3.3 环境(声明)语义 3.4 命令语义 3.5 表达式语义 3.6 连续 3.7 证明技术 3.8 小结 习题 参考文献第4章 指称语义的一些例子 4.1 例子1 4.2 例子2 4.3 例子3 4.4 例子4 习题 参考文献第5章 代数语义学基础 5.1 概述 5.2 范畴论 5.3 图范畴及图文法 5.4 类别代数理论 5.5 抽象数据类型 5.6 等式理论与项重写系统 5.7 实例 习题 参考文献第6章 操作语义学与属性文法 6.1 操作语义概述 6.2 施用表达式(AE)的机器计算 6.3 属性文法概述 6.4 属性文法分类 6.5 用属性文法进行编译程序设计 6.6 属性文法定义语言 6.7 实例：AGDL的语法 习题 参考文献第7章 组合逻辑 7.1 概述 7.2 组合子 7.3 组合逻辑的语法理论 7.4 组合逻辑的逻辑基础 7.5 函数性基本理论 7.6 范畴组合逻辑 7.7 小结 习题 参考文献第8章 公理语义方法 8.1 概述 8.2 程序正确性验证的基本概念 8.3 程序正确性验证技术 8.4 Hoare公理系统 8.5 Dijkstra的最弱前置条件 8.6 Martin-lof类型论 习题 参考文献第9章 维也纳发展方法：Meta-Lallguage 9.1 概况 9.2 在VDM中的逻辑注释 9.3 抽象数据类型 9.4 抽象文法 9.5 组合算子 9.6 VDM与程序设计语言 习题 参考文献第10章 并发程序设计语言的语义与说明 10.1 并行系统概述 10.2 并发程序设计语言概述 10.3 幂域及不确定性 10.4 通讯顺序进程(CSP) 10.5 并发程序设计语言的指称语义 10.6 通讯顺序进程的操作语义 10.7 进程与通讯网络的抽象数据类型 10.8 并发程序设计语言的公理语义 习题 参考文献
声明范畴的成分在于建立及改变环境；命令范畴的成分（即语句世界的成分）在于执行并改变状态；而表达式范畴的成分在于计算产生值。在语言的声明范畴中，又主要包括作用域及可见性两个概念。在命令范畴中的原子成分是赋值语句，GOTO语句的存在主要用于改变程序的执行顺序，也就是说，具有GOTO语句的语言程序，其书写顺序与执行顺序是不同的。在表达式范畴中，函数定义（或称函数抽象）与函数施用是两个基本概念。如果一个表达式不仅计算产生值，而且还改变状态，我们称这个表达式有副作用（side-effect）。 在Von Neumann计算机体系中，程序设计语言还引入了地址概念，致使表达式计算产生的值与地址联系起来。如果使用这个值，则必须引用置有该值的内存的地址，我们称这样的程序是依赖于环境的，因为计算的结果与所在存储器的位置有关。 如果一个语言没有命令范畴，它只有表达式范畴及表示类型与对象的声明范畴，而且这种语言中的每一个函数都不依赖于环境而存在，那么它所计算的结果与所在存储器的位置无关，只要满足了函数定义域则可以处处施用，绝无副作用，那么称这样的语言为施用型语言（applicative language）。 为什么要研究形式语义学呢？ 理论研究的最强大的动力是发展生产，促进社会的进步。软件生产长期停留在手工劳动的状态，生产力很低。像所有其他工业发展那样，软件产业也要追求自动化生产，大规模生成，高效率及高质量生产的目标。 为了发展软件生产力及保证软件生产的质量，软件工程方法被广泛地研究并得到普遍的应用。软件工程方法一般化分为如下几个阶段：
中国信息安全测评中心自然科学基金项目内容组成之一 站在软件立场上讨论计算机科学的理论及其应用 详细给出形式语义学的基础理论框架 理论与软件实践相结合
无
不错~推荐购买，这个相当不错~！基本上看不懂
书还没仔细看 印刷质量和正版性不用担心了
还可以，目前只是翻了翻，比较系统的书