《形式语义学引论（第二版）》为形式语义学入门参考书，简单介绍程序的操作语义、指称语义和公理语义。《形式语义学引论（第二版）》共7章：第1章介绍操作语义，第2章介绍指称语义，第3章介绍公理语义，第4介绍过程调用的形式语义，第5章介绍非确定程序的形式语义，第6章介绍并发程序的形式语义，第7章介绍程序的时态语义。

　　《形式语义学引论（第二版）》：
　　亦写作
　　这里（L→R）表示南集合L至集合R的全体函数组成的函数空问。在语义学中，通常采用花体字表示语言成分的语义函数，而将语言成分用双重括号括起，故给定一个布尔表达式B，有
　　对给定的状态s，又有
　　即对给定的布尔表达式B和状态s，由可得到B在状态s下所取的布尔值。
　　以上这些记号法在《形式语义学引论（第二版）》中将不断使用，不再一一说明。使用语义函数历及上述记号布尔表达式求值的转移规则可定义如下：
　　即抽象机按照对给定B及s求出布尔值，并将其存入栈区。
　　由于FLOW语言中没有算术表达式，故算术表达式的求值规则不必在此讨论。
　　C．执行
　　下列各规则中或者（表示空序列，在不致引起混淆时，《形式语义学引论（第二版）》中亦用来表示空集合）。
　　（1）
　　即执行skip不导致st和s的改变，但导致抽象机转向执行其后继部分c’。当c中内容非空时，c应以顺序算子“；”为起始跟以后继部分c’，故；当c中内容为空时，其后继部分亦为空，故。
　　（2）
　　这里。名代表原子语句的语义函数，如一样，此处作为预先假定的。原子语句设想为赋值语句，它按照程序变元的当前值求出表达式值，再改变被赋程序变元的值。故假定其语义为状态空间至状态空间的一个函数，即
　　（3）
　　（4）
　　这两条规则是说，在求出布尔表达式值后条件语句的执行导致抽象机选择相应的分语句，并转向执行该分语句。对于循环语句亦有两条类似的规则。
　　（5）
　　（6）
　　其中，S2为skip，S1为S；（while B do S）。
　　至此，我们定义了解释执行FLOW程序的一个抽象机，也就给出了FLOW语言的一种操作语义。而以AFLOW中的一个程序为例，在假定，和通常理解一致的前提下，看其操作语义是否与通常理解亦一致。
　　例 计算x！的程序FAC。
　　FAC中只有程序变元x，y和z，设State为非负整数二元组的集合。在x，y和z的初始值分别为2，0，0时解释执行FAC程序形成的大状态转移序列如下，其中转移号上标以此转移所依据的规则号，而用到的函数假设为：
　　这里为非负减，即
　　上述转移序列表明，只要符合通常的理解，在x的初值为2时执行FAC，程序可以终止，终止时变元y处存有所求的阶乘值2。
　　……

目录
再版说明
前言
第1章 操作语义学 1
1.1 引言 1
1.2 FLOW语言 2
1.3 栈-状态-控制机器 3
1.4 程序的计算 7
1.5 归约关系 9
1.6 Com=com 13
1.7 AFLOW的操作语义 14
1.8 操作语义发展动态 15
参考文献 16
第2章 指称语义学 17
2.1 引言 17
2.2 FLOW的指称语义 18
2.3 完全偏序集和连续函数 20
2.4连续算子 25
2.5 不动点 29
2.6 例 33
2.7 FLOW的指称语义（续） 37
2.8 操作语义与指称语义的一致性 38
2.9 AFLOW的指称语义 41
2.10 指称语义发展动态 42
参考文献 43
第3章 公理语义学 45
3.1 引言 45
3.2 霍尔系统 45
3.3 形的可靠性(Soundness) 51
3.4 男的完备性(Completeness) 52
3.5 可表达性(Expressiveness) 54
3.6 彩的相对完备性 58
3.7 公理语义发展动态 60
参考文献 61
第4章 过程调用 63
4.1 引言 63
4.2 PFLOW的操作语义 64
4.3 PFLOW的指称语义 69
4.4 PFLOW的公理语义 76
第5章 非确定性 82
5.1 引言 82
5.2 GCL的操作语义 84
5.3 GCL的指称语义 89
5.4 最弱前置条件 96
参考文献 105
第6章 并发性 106
6.1 引言 106
6.2 CSP语言 106
6.3 CSP的操作语义 111
6.4 CSP向指称语义 120
6.5 CSP陶公理语义 124
6.6 并发理论发展动态 129
参考文献 130
第7章 时态语义 132
7.1 引言 132
7.2 时态逻辑 133
7.3 时态语义 136
7.4 基本性质 139
7.5 程序描述 141
7.6 程序推理 143
7.7 时态语义发展动态 148
参考文献 149