收集语义

收集所有可能状态 ​

设程序点集合为 $V$，具体状态集合为 $\mathrm{\Sigma }$。收集语义是映射

其中 $C(v)$ 包含从允许初始输入出发、沿某条合法执行到达程序点 $v$ 时可能出现的全部具体状态。值域是幂集公理库幂集Power set集合 A 的所有子集组成的集合，记作 P(A)。，所以它保存的是行为集合，而非某次运行的单个内存快照。

若控制边 $e=(u,v)$ 的具体变换为 ${\tau }_e:\mathcal{P}(\mathrm{\Sigma })\to \mathcal{P}(\mathrm{\Sigma })$，收集语义满足包含方程

入口还要加入初始状态集合 ${\mathrm{\Sigma }}_0$。精确收集语义取满足全部约束的最小解；较大的任意解仍可能是可靠上界，却不再精确描述恰好可达的状态。

与操作语义的关系 ​

操作语义公理库操作语义Operational semantics用执行判断、转移规则或抽象机定义程序如何运行。定义一个具体配置怎样一步变成下一个配置。把配置写成 $(v,\sigma )$，就得到一个状态机公理库状态机State machine · Transition system用状态集合、初始状态和转移关系描述系统可能执行轨迹的模型。；收集语义对其全部有限执行取可达闭包，再按程序点 $v$ 投影。

因此两者回答不同问题。小步语义可以展示

这一条执行怎样推进；收集语义则把所有可能到达 $v_2$ 的 ${\sigma }_2$ 放进同一个集合。它不会保留哪个状态来自哪条路径，除非把路径历史也编码进具体状态。

大步语义若只关联程序入口与最终结果，通常不足以直接给出中间程序点的集合。静态分析需要循环头、分支汇合等位置的信息，因而常以小步或控制流边语义为基础。

循环例子的固定点轨迹 ​

考虑

x := 0
while x < 3:
    x := x + 1
return x

假设整数算术无溢出。初始化后到达循环头的状态集合从 $H_0=\{0\}$ 开始。沿真分支和循环体回到头部，一轮加入 $1$，再一轮加入 $2$，再一轮加入 $3$：

此后再应用方程不产生新状态，故循环头的精确集合为 $\{0,1,2,3\}$。循环体入口由 guard $x<3$ 筛成 $\{0,1,2\}$，退出点由 $x\ge 3$ 筛成 $\{3\}$。

若只记录一次样例运行，仍会看到 $0,1,2,3$，但那是因为该程序确定且输入固定。加入未知初值、输入分支或非确定调度后，收集语义要同时包含全部可能性，测试轨迹不能代替这个全称闭包。

汇合会遗忘路径关系 ​

考虑分支 if b then x:=0 else x:=1。汇合点的收集集合包含两类状态：一类满足 $b$ 且 $x=0$，另一类满足 $\mathrm{\neg }b$ 且 $x=1$。若只把各变量可能值分别投影成 $b\in \{0,1\}$、$x\in \{0,1\}$，就会额外允许 $b$ 与 $x$ 不匹配的组合。

精确收集语义本身仍保留完整状态元组，因此没有丢掉相关性；丢失发生在后续选择的非关系抽象表示。把精确 concrete set 已经产生的路径汇合，与区间、符号等抽象域造成的精度损失混为一谈，会误判假警报来源。

另一方面，按程序点合并确实遗忘了到达路径的身份。若性质依赖“先经过认证节点才可访问资源”，可以把认证位加入状态，或采用 path-sensitive 分析；不在状态中的历史不会由集合收集自动恢复。

为何通常不可直接计算 ​

即使程序语句有限，整数、堆、栈或队列也可让 $\mathrm{\Sigma }$ 无限，$C(v)$ 因而是无限集合。循环和递归还要求求解递归集合方程；一般程序可达性受停机不可判定性公理库停机问题不可判定性Halting problem · Undecidability of halting不存在一个对任意程序和输入都能正确判断程序是否停机的算法。限制，不存在对所有程序都返回精确有限表示的算法。

有限状态程序也可能有指数多状态。逐项枚举精确集合在理论上可行，在工程上仍会遭遇组合爆炸。收集语义的作用不是承诺一个高效表示，而是提供“静态分析究竟要包住什么”的语义标尺。

抽象域公理库抽象域Abstract domain · Domain of abstract properties用带精度次序和合流运算的抽象元素表示具体状态集合，为可靠静态近似提供语义空间。用可计算元素代表这些具体集合，抽象转移函数给出可靠外包络。可靠性要求不漏掉 $C(v)$ 中状态；精度则衡量额外加入多少不可达状态。终止、可靠与精确是三项不同目标，不能用一句“近似分析”全部带过。