在第12.1节中介绍的TIP语义被称为可达状态收集语义，因为它对于每个程序点收集了在某些输入下程序执行到达该点时可能的状态集合。正如我们所见，这种方式准确地捕捉了TIP程序的含义，使我们能够证明例如符号分析的正确性。然而，对于其他分析而言，可达状态收集语义是不够的，因为它无法捕捉有关TIP程序如何执行的所有信息。例如下面的程序：

main(x) {
	return x;
}

可达状态收集语义只会告诉我们函数入口处的状态集合和函数出口处的状态集合都是$\{[x \mapsto z] | z \in \mathbb{Z}\}$，但它并不告诉我们返回值总是与输入值相同。换句话说，可达状态收集语义不提供有关程序点上的一个状态与其他程序点上的状态之间关系的信息。为了捕捉TIP程序执行的这些方面，我们可以使用跟踪语义(trace semantics)，它将TIP程序的含义表示为程序运行时可能出现的跟踪集合。

之前的收集语义都是独立的点！现在是一条完整的执行轨迹！

一条trace是一个有限序列，其中每个元素是一个二元组合（程序点-CFG的节点，程序的抽象状态）：

$$ Traces = (Nodes \times ConcreteStates) ^ * $$

    我们首先将单个控制流图（CFG）节点的语义定义为从具体状态到具体状态集合的函数（作为第5.10节中传递函数的具体对应）：$ct_v：ConcreteStates \\rightarrow \\mathcal{P}(ConcreteStates)$。

• 对于赋值的节点，ct_v可以被定义为：【也就是说，在一个trace上，求解E得到的所有结果，讲当前trace里面的X的结果替换为这个“所有结果”】

$$ ct_{X=E}(\rho) = \{ \rho[ X \mapsto z] | z \in ceval(\rho, E) \} $$

• 对于变量声明，同上

• 其他节点，因为没有修改状态所以

  $$ ct(\rho) = \{ \rho \} $$

    那么一个程序P的跟踪语义，就是一系列的trace的组合，写作 $\\langle [P] \\rangle \\in \\mathcal{P}(Traces)$。我们可以将$\\langle [P] \\rangle$ 定义为从程序入口点开始，并在每一步按照控制流图（CFG）进行的有限跟踪的集合。（我们不要求跟踪达到程序出口。）更正式地说，我们将$\\langle [P] \\rangle$  定义为以下两个约束的最小解：
  

第一个约束说明程序入口点在空状态下始终可达。第二个约束说明如果程序有一个以状态 $\rho$ 结束于节点 $v$ 的trace，其中 $v'$ 是可能的后继节点，而$\rho'$是我们从状态 $\rho$ 执行 $v'$ 可能得到的状态，那么扩展了额外的一对 ($v'$, $\rho'$ ) 的跟踪也是有意的。

    举个例子：对于最开始的例子，我们有如下跟踪语义：【是一个一个二元组的连接，每个二元组是程序点和程序状态的抽象。因为x是input，所以ceval的结果是所有整数，所以是无限多这种traces】

这个结果就能够表示x的值在进入程序和出程序一致。

    有趣的一点是，基于可达状态的收集语义和跟踪语义之前也可以通过Galois连接进行描述，我们需要引入下述抽象函数，讲Traces的幂集合映射到具体状态的幂集合的多元组合上：