本书以作者在剑桥大学和Aarhus大学的讲座内容为基础，主要针对计算机科学专业和数学专业的本科生和研究生而编写，可作为开始学习形式化和推导程序设计语言的方法的教材。本书介绍了必要的数学背景知识，读者可以运用它们去创造、形式化和证明一些规则，使用这些规则可推导各种各样的程序设计语言。本书的内容是基础的，但其中有一些主题来自于最近的研究。书中包含了丰富的从简单到复杂的练习。本书首先介绍集合论基础，接着是结构化操作语义，并将其作为定义程序设计语言含义的一种方式，同时也介绍了一些基本的证明技术。对指称语义和公理语义是以一个简单的while程序语言为例进行说明的，并给出了操作语义和指称语义之间等价的完整证明，以及公理语义的可靠性和相对完备性，也包括哥德尔不完备性定理的一个证明。该定理强调公理语义不可能达到绝对的完备性，这一结论可以从附录中得到支持，附录基于while程序介绍了可计算性理论。在域论之后，介绍了指称语义的基础，论述了几种函数式语言的语义和证明方法。最简单的函数式语言是既可以传值调用也可以传名调用求值的递归方程。这些研究工作可以进一步扩展到含有高阶类型和递归类型的语言，其中包括对活性和惰性入演算的论述。本书始终强调指称语义和操作语义的联系，并给出它们的一致性证。本书较高深的部分之一是递归，类型的论述，它要利用信息系统来表示域。在最后一章里介绍了并行程序设计语言，并讨论了不确定性和并行程序的验证方法。
鄂公网安备 42010302001612号 