“统一绑定时间分析给出静态变量 S 与动态变量 D，保证静态赋值只读静态变量。本页接收这份二分、原程序 P，以及所有已知输入的具体整数值，输出残余程序 Q。Q 以后只接收原来未知的输入，返回与…”
形式陈述
固定的不是值，而是在哪个阶段保存它
设一个程序接收 n 和 x。今天已经知道 n=3，x 要等明天才收到。我们希望今天把只依赖 n 的工作做好，输出一份仍接收 x 的程序。绑定时间分析先回答一个更小的问题：哪些变量允许在今天的专门化过程中保存具体值，哪些必须留给生成后的程序？它不需要先知道 n 究竟是3还是5。
本页使用显式赋值、标签与跳转组成的有限流图。每个基本块有有限条顺序赋值，最后是 goto、双路 if 或 return。表达式由整数常量、变量、加减乘及比较构成；比较返回0或1，if 以非零为真。整数是数学整数，没有溢出。所有原语纯粹、确定且总定义；没有堆、I/O、调用、异常、除法或在表达式内部递归。唯一可能的无限执行来自块间循环。
程序声明有限变量集 V 及其中的输入变量。开始时每个局部变量为0，再用输入替换对应槽。因此不会读取未初始化值。这个规定属于教学语言，而不是声称 C、LLVM 或任意三地址码默认都这样初始化。实际检查器允许有限嵌套的二元表达式；拆成临时量也能表达同样计算，但要重新对这些临时量分析。
一个统一二分为每个变量指定 S 或 D，在所有源程序点使用同一标签。S 表示专门化器在每个正在处理的变体中保存该变量的具体值；D 表示它保留为残余程序的变量。S 不表示源变量从不赋值，也不表示不同执行路径上的值相同。后续流图专门化会把不同静态存储保存在不同版本中。
输入、约束与输出
输入包括源程序、未知输入集合 U，以及可选的主动动态化集合 F。F 可以含已知输入或局部变量：即使知道某个值，也允许选择在残余程序里计算，以免生成过多代码。动态种子为 D₀=U∪F；其他变量暂标 S。
对每条赋值 x:=e 和 e 中出现的每个变量 y，建立依赖边 y→x。只要 y 是 D，x 就必须是 D。求解
输出为从 D₀ 反复应用 Φ 得到的最小不动点 D*，以及
这个规则不沿条件分支增加“控制依赖边”。它服务于按静态存储分裂版本的专门化器，不能原封不动用来证明无隐式信息流。若未知 p 决定 k:=2 或 k:=5，k 可以为 S，但汇合点必须有 k=2 与 k=5 两个版本。若生成器只能给汇合点保存一份静态值，就不满足本页的使用前提。
工作队列实现
预先为每个变量保存从它发出的赋值依赖边。把种子标为 D 并各入队一次。每次取出 y，检查所有 y→x；尚非 D 的 x 立刻标 D 并入队。队列空时返回。边可以保留重复的变量出现，它们只增加扫描工作，不改变集合。
这是有限单调求解的一种很小的实例：二点序 S≤D 的逐变量积序等价于动态集合的包含序。集合只扩大，每个变量最多从 S 改为 D 一次。实现不靠浮点阈值或固定扫描轮数决定稳定，而靠没有待传播的新事实。
直觉
想象把源码中的工作分成“制作专用工具”与“使用专用工具”两阶段。若一条赋值需要明天才到的 x，它的结果今天就不能直接算出来。这种等待会顺着后续赋值传播。另一方面，循环计数器 i 即使反复变化，只要当前 i 的值在制作阶段可得，就仍能标为 S。
分析给出的是一份可以遵守的分工表，不是完整优化结果。它不发出代码，不判断分支实际走哪边，也不保证制作专用工具的过程会结束。静态值的具体变化和变体数量都要在下一步检查。
例子与边界
三轮仿射更新的完整二分
程序输入 n、x，局部变量 i、a、b、y 初始为0：
text
E: i := 0
a := 2
b := 1
y := x
goto H
H: if i < n goto B else R
B: y := a*y+b
a := a+1
b := b+2
i := i+1
goto H
R: return y已知 n、未知 x，故 D₀={x}。赋值给出七次依赖出现：x→y，a→y，y→y，b→y，a→a，b→b，i→i。H 中的 i<n 决定之后该展开哪条边，但不是对某个变量的赋值，所以没有新增赋值边。
取出 x 时加入 y；取出 y 时只见自环，之后队列为空。结果 D*={x,y}，S*={n,i,a,b}。自环 a→a 并不把 a 变成 D，因为它没有动态来源；相反，从 n=3 出发，我们能依次算出 a=2、3、4、5。把“含有环”误作“必须动态”会丢掉本来可计算的部分。
若把 B 的最后一行改为 i:=i+x，则出现 x→i，结果变为 D*={x,y,i}。循环条件因此动态化，但 a、b 仍可静态变化；不能就此宣称专门化有限。若主动把 a 加入 F，a→y 只确认本来已动态的 y，不会反向把 b 或 i 拉进动态集合。传播是有方向的。
动态控制可以对应多个静态值
考虑 E 按未知 p 分支，T 执行 k:=2，F 执行 k:=5，两边都进入 J；J 计算 y:=kx 并返回 y。输入 p、x 未知，k、y 从0开始。赋值依赖为 k→y 与 x→y，所以 D={p,x,y}，k 为 S。
这不表示 k 与 p 在真实运行中毫无关系。p 为真时 J 的 k=2，为假时 k=5；生成器分别建立 J[2] 和 J[5]，以后由残余分支选择。x=4 时两边结果8与20都被保留。若只按源标签 J 缓存第一次生成的代码，把第二次请求也指向 J[2]，假分支就错误返回8。这里缺的是版本身份，不是常量乘法规则。
因此本分析不等于SCCP。SCCP 在一个 SSA 定义上合流不同路径的可能值，通常会把2和5合成“非常量”；本页的 S 标签只要求各版本能带着各自的具体 k，二者回答的问题不同。
最小不代表语义上最精确
即使 y:=x−x 总为0，语法依赖仍含 x→y。若 x 动态，本规则把 y 标 D，不利用代数抵消。即使某条赋值位于不可达块，也参与统一约束。删除死块或证明等式可能改进结果，但那是额外分析，不能从本工作队列自动得到。
同样，变量先接收未知输入，随后无条件改写为常量，统一二分也可能一直将其标 D；更细的按程序点二分可以区分前后阶段。本页刻意保留统一标签，让读者可以完整复算闭包和残余接口，不把这种保守性藏在“找到所有静态计算”的说法里。
推论与应用
为什么得到最小合法动态集合
终止来自有限 V 与单调加入。稳定时若某条边 y→x 的 y 已动态，y 必已出队，该边也已检查，所以 x 必动态。因而输出包含所有种子并满足每条赋值约束。
再取任意满足约束、包含 D₀ 的集合 C。初始化的所有元素在 C 中；若工作队列因 y→x 新增 x，已有 y∈C，闭合性便迫使 x∈C。按每次加入归纳，整个 D* 都包含于 C。因此结果是最小合法动态集合，而非队列顺序碰巧找出的某个解。这里的“合法”始终指本页的语法约束。
局部可计算性也可直接检查。在块入口给定 S* 的全部具体值后，按赋值顺序处理：静态目标的表达式只含静态变量和总原语，故能算出下一静态值；动态目标不改变静态存储；到块尾，静态条件可以决定单一后继，动态条件则保留两条后继。不同后继各自携带当前静态存储。这项逐块事实是生成器的前提，尚不是整个变换的语义保持证明。
成本、终止边界与交付
设 K 为全部表达式及指令的语法规模，v=|V|，u 为赋值右侧变量出现次数。建邻接表需 O(K+v) 时间与 O(v+u) 空间；每个变量至多出队一次、每条依赖出现至多扫描一次，求闭包需 O(v+u)。这些界按变量名已编号、集合访问均摊常数计；读入名字的字符成本另外计算。算法并不执行大整数运算，因此不因已知输入数值很大而增加传播轮数。
参考器为使 JSON 的种子事件和最终集合次序稳定，另外对变量名排序，故它的实际总时间还包含
有限的二分结果不保证有限专门化。例如 i 从0开始，在未知上界 x 下循环执行 i:=i+1，条件为 i<x。本分析允许 i 为 S，但生成器可能需要 i=0、1、2、……无穷多个版本。将 i 主动标 D 可以把循环留给运行阶段；怎样选择值得动态化的变量是另一个问题，不能把分析的至多 v 次增长误用为代码生成的终止界。
可执行终点要求先交出七条依赖、队列事件和最终二分，再生成九块残余代码。迁移练习包括动态控制下的两个 J、主动动态化已知输入，以及一个每次具体执行都结束却无法有限展开的循环。先预测变化，再运行参考器，对照它实际发出的程序和状态对应证据。
参考资料
- Neil D. Jones、Carsten K. Gomard、Peter Sestoft，Partial Evaluation and Automatic Program Generation，1993，§4.4.1（印刷页77）的统一二分，§4.4.6（印刷页83–84）的赋值约束；§14.2 区分一致性与有限变体。本页限定纯整数流图，另给工作队列、最小性证明和原创数值终点