背景介绍：
形式语义是一种用于描述编程语言的语义的形式化方法。它提供了一种精确的方式来解释程序的含义和行为，而不依赖于具体的实现细节。特别的，如果语法有二义性，但是语义不会。
形式语义通常使用数学符号和逻辑来定义程序的语义。它可以分为几种不同的类型，包括操作语义、语法语义和语义动态系统等。
https://www.zhihu.com/question/23861885
本章节我们定义与第4.1节和5.1节中的符号分析相同的TIP子集的形式语义，这意味着我们忽略了函数调用、指针和记录。在这个过程中，我们澄清了TIP中一些未明确规定的部分，正如在练习2.1中讨论的那样（也就是有歧义的地方）。我们选择了一种基于约束的方法来定义语义，而不是使用传统的语义风格，如操作语义（*operational semantics*）、指称语义（*denotational semantics*）或公理语义（*axiomatic semantics*）。这种方法与我们在前面章节中提出的分析的表述方式相吻合。此外，我们选择基于TIP程序的控制流图（CFG）来定义语义。这些选择使我们能够更简洁地将语义与分析相关联。重要的是，语义捕捉了程序在普通执行中的含义，没有任何近似。语义规定了具体程序执行的工作方式，而我们的分析可以被看作是抽象解释器。
正如上面所示，Tarski的不动点定理确保了收集语义的良好定义，即使它通常是不可计算的。而第4章（第47页）中的Kleene不动点定理的变体不足以确保这个性质，因为格具有无限高度。
对Tarski不动点定理的一个替换是采用Kleene的不动点定理，并且在函数f 是一个complete join morphism的时候，令格具有有限高度。对于一个函数f，它的类型是从一个完全格L1映射到另一个完全格L2，如果对于格L的所有子集， $f(\\sqcup~A) = \\sqcup_{a\\in A}~f(a)$，也就是join之后再计算的结果同计算之后再join的结果一致，那么这个函数具有complete join morphism。（看上去和分配律很像！）如果f具有complete join morphism，那么f一定满足单调性。对于有限格，一个函数如果满足complete join morphism，那么这个函数当且仅当f满足单调性。上述规则定义的收集语义中的所有约束条件，特别是函数cf，不仅是单调的，而且是complete join morphism。
在本章后续章节为了方便表示，我们令{[P]} = lfp(cf)，表示收集语义的具体状态；令[[P]]=lfp(af)，表示抽象状态。其中cf表示收集语义的约束函数，af表示分析的约束函数，P表示目标程序。也就是说，{[P]}表示程序的语义（是非常具体的情况），[[P]]表示我们对P分析的结果。
可以认为程序语义是最真实的程序的情况，分析结果是我们能够计算得到的结果。我们分析的目标就是令分析结果等于真实结果，如果做不到，那么可以不精确，但是一定要”包含“真实结果。举个例子，如果真实结果x=5，那么我们可以得到x=5或者x=6或者x=7，甚至x=Z，但是不能是x=4这种！