静态单赋值形式

普通程序反复给变量 $x$ 赋值，读者必须沿路径判断某次读取看到哪一个版本。SSA 把这项路径推理预先编码进名字：$x_0,x_1,x_2$ 各有唯一来源，合流处再明确选择来自哪条边。于是“哪次定义到达这次使用”从集合问题变成直接的定义—使用边，许多稀疏优化只需沿这些边传播。

SSA 没有消除控制流。名字唯一并不意味着值唯一：不同执行可以使同一个定义产生不同运行时值，例如循环中的 $x_2:=x_1+1$ 每轮都会得到新数。SSA 的静态图把可能反复执行的一条指令保留为一个节点，运行轨迹仍由 CFG 决定。

考虑菱形程序：入口给 $x:=0$，条件为真时执行 $x:=x+1$，为假时执行 $x:=x+2$，汇合后返回 $x$。版本化后可写成

沿真边手算得到 $x_3=x_1=1$，沿假边得到 $x_3=x_2=2$。若删掉合流定义而让返回任意使用 $x_1$，假路径上其定义不支配使用，程序便不是合法 SSA；这是一项可由图结构检查的不变量，而非变量名看起来带下标即可。

循环展示“静态”一词的边界。初始化 $i_0:=0$，循环头定义 $i_1:=\varphi (i_0,i_2)$，循环体定义 $i_2:=i_1+1$ 并回跳。$i_1$ 在每次进入循环头时执行，却只出现一个定义点；第一次选入口边的 $i_0$，以后选回边的 $i_2$。若把 φ 当作同时读取两个运行时值的普通函数，第一次迭代会错误地要求尚未执行的 $i_2$。

内存反例也很具体：令 $p$ 与 $q$ 可能别名，先做 $\mathrm{store}(p,1)$，再做 $\mathrm{store}(q,2)$，最后 $\mathrm{load}(p)$。即使 $p,q$ 各只定义一次，结果仍可能是 $2$。标量 SSA 不会凭空证明两次存储独立。

唯一定义使常量传播、复制传播、死代码删除和值编号拥有天然的稀疏工作表。若 $x_4$ 的定义确定为常量，分析只需访问它的使用者；但 φ 的输入边、异常边与隐式内存使用必须包括在定义—使用图中，否则所谓“无使用”会漏掉真实依赖。

SSA 不是目标机器通常直接执行的格式。进入寄存器分配前，编译器往往消解 φ、拆分关键边并安排并行复制。构造与消解必须各自保持语义；仅证明输入和输出都满足某种名字格式，不足以证明它们运行结果相同。

memory SSA 可为每次可能写内存的操作产生新内存版本，并让 load 使用支配它的版本；分支汇合时也需要内存 φ。它能把别名分析结果编码为稀疏依赖，却不会自己证明两个地址不别名。若外部调用的 mod/ref 摘要漏掉一次写入，内存版本链会显得合法但 load 仍可能读错值。