trace

definition

assume a fixed set of statements Σ. A trace τ is a sequence of statements, i.e.

$\tau =s{t}_1\cdots s{t}_n$

for $n\ge 0$ and $s{t}_i\in \Sigma$

如果将$\Sigma$视作字母表，语句st视作letter，则trace就是这个字母表上的word，即$\tau \in {\Sigma }^{\ast }$

trace的定义和状态无关，两者是独立的。当然，对程序而言，其接受的trace集合需要满足语法上一些约束（严格的说是控制流），但和其语义没有关系。只有在进行验证，考虑trace的正确性时时，才考虑trace的语义。

correctness of a trace

trace的正确性是语义性质，这需要额外的定义。既然trace是语句的序列，一般用Hoare三元组来定义。

假设有一个预知的三元组的集合，这样的三元组定义了一个单独的语句的正确性。此外，有一对固定的公式${\varphi }_{pre}$和${\varphi }_{post}$（取决于具体的验证问题）。一个trace $\tau$是正确的，即$\{{\varphi }_{pre}\}\tau \{{\varphi }_{post}\}$是成立的。

infeasibility

a trace is infeasible iff {true}$\tau${false}

in other words:

in whatever valuation of the program variables the execution starts, one of the assume statements in the sequence cannot be executed

Thus, infeasibility implies (any) correctness. 这个性质的重要性在于，一般来说，一个程 序 如果的确是正确的，那么其正确的、feasible的control flow trace不是regular的。但是，其所有正确的control flow trace（包括infeasible的）是regular的。因此，将infeasible的trace考虑为正确的trace，是验证能够进行的条件。

另外，如果程序本身不是正确的，那么即使是其正确的那部份control flow trace也不一定是regular的。

关于以上事实可以这么理解：程序被当作自动机的情况下，本身就是有限状态的。所以，如果程序的确是正确的，那么其接受的当然是正规语言，而且其接受的trace里当然也包括了那些infeasible的。

特别的，如果选择${\varphi }_{pre}$和${\varphi }_{post}$分别为true和false，则infeasibility和正确性是等价的。比如说，要证明某个error location不可达，则将其设置为程序的终止状态。