程序逻辑中的迹语义 我们先从程序执行的基本概念开始。迹（trace）是指程序在运行时产生的一系列状态变化记录。例如，一个简单的赋值语句 x := x + 1 ，若初始状态中 x 的值为 0，执行后状态中 x 的值变为 1，那么这次状态转换 (x=0) → (x=1) 就构成了一条长度为 1 的迹。迹语义的核心思想是：一个程序的意义可以由其所有可能的执行迹的集合来定义。 接下来，我们形式化迹的概念。令 Σ 表示程序状态的集合。一个 有限迹 是一个有限的状态序列 σ₀ σ₁ ... σₙ ，其中每个 σᵢ ∈ Σ ，并且存在一个合法的程序执行步骤使得状态从 σᵢ 转换到 σᵢ₊₁ 。一个 无限迹 则是一个无限的状态序列 σ₀ σ₁ σ₂ ... 。程序的完整迹语义，通常表示为 [[P]] ，就是该程序所有可能的有限迹和无限迹的集合。 对于包含不同控制结构的程序，我们需要定义其迹的生成方式。对于顺序复合 S1; S2 ，其迹是由 S1 的一个有限迹（以某个状态 σ_m 结束）与 S2 的一个迹（以 σ_m 开始）连接而成。对于条件语句 if b then S1 else S2 ，其迹首先检查布尔条件 b 在当前状态下的真假值，然后接着执行 S1 或 S2 的迹。循环语句 while b do S 的迹则更为复杂：它由零次或多次执行循环体 S 的有限迹拼接而成，每次执行前都满足条件 b ，最终以一个状态转换结束，该转换发生时条件 b 不再成立，或者它可能是一个无限迹（即无限循环）。 迹语义的一个主要优势在于它能自然地描述并发程序的行为。考虑两个并行执行的进程 P || Q 。它们的交错执行（interleaving）会产生丰富的迹集合。一条迹可能来自 P 执行一个原子步骤，然后 Q 执行一个原子步骤，如此交替进行。迹语义通过枚举所有可能的交错序列，为并发程序的非确定性行为提供了精确的模型。 基于迹语义，我们可以定义程序的各种性质。 安全性性质 （safety properties）指的是"坏的事情永远不会发生"。在迹的层面上，这表现为：如果一个坏的事件（bad event）在某个迹中发生，那么它必然在某个有限前缀中就已经发生。 活性性质 （liveness properties）指的是"好的事情终将发生"。这表现为：对于任何一个有限的迹前缀，总存在一个后续的迹扩展能使该好的事件发生。迹语义是线性时态逻辑（LTL）等程序规约语言的天然模型。 最后，迹语义与其他程序语义之间存在着深刻的联系。它与 指称语义 密切相关，指称语义通常将程序定义为状态空间上的一个函数，而这个函数可以从程序的迹集合中推导出来。它也是 操作语义 的一种抽象，操作语义描述了程序具体的计算步骤，而迹语义则抽取了这些步骤产生的状态序列。在 模型检测 中，系统的迹语义模型可以直接与时态逻辑公式进行验证，以判断所有迹是否都满足规约。