“当重复的是不变条件的控制选择时，循环不变分支外提给出独立接口：复制完整循环并在运行时选一份，保留每轮赋值与事件次序。条件须在入口有值且体内不写；零轮会多求值一次，仍依靠纯总与无事件条件。它改…”
形式陈述
先把次数与条件分开
某段循环每轮都检查 mode>0，但 mode 在整个循环中没有写入。无论这次运行会走哪一支，所有轮都走同一支。循环不变分支外提把循环复制成真、假两个版本，进入时检查一次 mode>0，随后只执行选中的版本。这是运行时选择，不要求编译时知道 mode 的值。[1]
循环不变代码外提已区分操作数不变和提前求值安全。本页复用这两个条件，但移动的是控制选择：目标包含两份循环，循环中的对应 if 被所选分支替代。没有把两分支的赋值都提前执行，也没有把它们都执行一遍。
共同语言使用数学整数。表达式由整数常量、局部变量、加减乘、比较组成，比较结果为0或1；另允许除以正整数字面量的向下取整商与余数。所有表达式纯粹、确定、总定义，没有调用、随机性、内存读取、溢出、异常或表达式内事件。if 将非零视为真。
程序先执行有限赋值初始化，随后有一个 repeat E { B }，最后返回若干表达式。进入 repeat 时求值 E 一次，得到非负整数 N，再将有限体 B 顺序执行恰 N 次。体内允许赋值、嵌套 if 和 emit(tag,e)；emit 求值 e 后向观察迹尾部追加一个标签—整数对，不改变变量。体内没有循环、break、continue、提前返回或外部交互。因此每个合法输入都有限结束，观察为全部事件的有序列表和返回元组。
N 非负是输入执行的前提，不是把负数默默截断成零。参考器遇到负次数会报告输入不属于模型。体内可以修改 E 读取的变量：因为次数已经捕获，这不会改变本次 repeat 的轮数。比如以 n=10 进入后每轮令 n:=0，仍须完成十轮。
哪个条件可以搬出去
在 B 中选定一个具体 if，其谓词为 p、真体为 T、假体为 F。它可以直接位于 B，也可以嵌在其他 if 的某条分支中。选择依据是语法路径，只处理这个出现，不把别处相似的条件自动一并替换。
接受条件有两条。第一，p 读取的每个变量都在循环入口确定有值。第二，B 的全部语法分支中都没有对这些变量的赋值。不可达分支中的赋值也会触发这项保守拒绝；本算法不另行证明那条路径不可达。
所有源程序读取还须通过确定赋值检查。顺序赋值先查右侧再加入目标；if 后取两支已定义集合的交集；repeat 后不加入仅在体内定义的变量，因为它可能执行零轮。这允许 t:=3; if t>0 ... 出现在体内，却不允许由此认为 t 在循环入口已定义。这样的源程序可以良构，而该 if 仍不满足外提条件。
实际产生的两个版本
设 B[p←真] 表示仅把选中的 if 替换成 T，其他语句、条件和次序都不变；B[p←假] 同理。选取从未在源程序中出现的新鲜名字 n₀，生成
text
n₀ := E
if p:
repeat n₀ { B[p←真] }
else:
repeat n₀ { B[p←假] }原初始化和返回表达式原封保留。次数捕获放在新分支之前，且只做一次；两份循环使用同一个捕获值。n₀ 不向源变量冒名写入，即使用户原本就有名为 __trip_0 的变量，也要换用未占用的名字。
变换成功后，对每个合法输入，源与目标产生相同事件列表、相同返回元组，并在结束时对全部源变量取相同值。新增捕获变量不属于源观察。若条件读了循环内写入的变量，或入口尚未定义的变量，参考器返回 refused 而不产生目标；代码预算不够则另报 size_limit，不能把它解释成语义不合法。
直觉
可以把循环理解成一次选择工序、然后重复加工一批零件。若选择依据在这批加工期间不变，先选好一条加工线，就不用每件再问同一个问题。但选中的加工线仍须包含该轮原有的所有前后步骤。
尤其不能只把 if 的两条赋值拿到外层而丢掉周围语句。每轮的记录、累积和计数器更新仍各执行一次；它们还可能相互依赖。复制整个体并在其中删去已经确定的选择，才保留这些相对位置。
例子与边界
带有外部记录的十轮递推
取 N=10、mode=1，初始化 s=1、i=2。循环体为
text
emit("before", i)
if mode > 0:
s := 2*s+i
else:
s := s-i
emit("after", s)
i := i+1每轮先记录当前 i，再更新 s，记录新 s，最后递增 i。正分支的十个 s 依次是4、11、26、57、120、247、502、1013、2036、4083，返回 (4083,12)。事件迹开头为 (before,2),(after,4),(before,3),(after,11)，结尾为 (before,11),(after,4083)，共20项。
mode 在体中从未赋值，所以目标在循环前检查 mode>0 一次，只运行含 s:=2*s+i 的循环。before、after 和 i 更新仍留在每轮原位置。分支测试由10次变1次，计数循环测试仍是11次，包括最后一次确认已完成十轮的失败测试。
若 mode=0，则源与目标都选择负分支。十个 s 为−1、−4、−8、−13、−19、−26、−34、−43、−53、−64，返回 (−64,12)。目标中真版本虽然存在，却不执行其中任何赋值或事件。代码中有两个循环不等于运行时把两循环相接。
变量在体内变化时不能冻结选择
在每轮末尾追加 mode:=mode−1，取 N=3、mode=2。三次源条件依次真、真、假；前三轮 s 是4、11、7，返回 (7,5)。如果只看第一次 mode>0 就永远用真版本，会得到4、11、26，错误返回 (26,5)。这不是少算一次条件的问题，而是删除了后续本来应该发生的控制变化。
即使某条写入看起来“没改变值”，如 mode:=mode，参考器仍拒绝。它检查的是简单、可核验的无写条件。要接受这种程序，可以先证明写入无效并删除它，或者为外提算法加入更强的不变量证明；不能拿一次测试中恰好相等充当通用证明。
零轮多算一次，为什么仍然正确
把 N 改为0，源不执行体内条件、赋值或事件，返回 (1,2)。目标仍计算 mode>0 一次，然后所选 repeat 立即结束，也返回 (1,2)。源条件测试0次，目标1次；零轮并不节省条件工作。
这项新增求值只有在纯总前提下才不可观察。若把条件改成 1/d>0 并允许除零异常，N=0、d=0 时源正常返回，直接外提却异常。若条件在读取时向设备发事件，源零事件而目标多一个事件，即使它的数值每次一样也不合法。[2]
在允许部分表达式的另一种语言中，先检查 N>0 可以阻止零轮新增异常，但这还不是完整修补。如果每轮在条件前先 emit 一个事件，而条件随后异常，把条件移到这些事件之前仍会改迹。因此还要证明提前路径上的观察与异常时机相容。本页参考器直接不接受这类表达式，没有宣称一层零轮护卫解决所有情况。
条件嵌套时，外层分支仍要保留
例如 B 内是 if i<3: if mode>0: s:=s+1 else: s:=s−1，后面递增 i。mode>0 可以外提，但 i<3 不能因此消失。正版本仍只有满足 i<3 的轮才加一；负版本也仍受同一个外层条件约束。若 i 从0开始而 N=5，正确正版本只增加3，不是5。
推论与应用
对每一轮建立状态和事件对应
记进入循环时的源环境为 ρ₀。对 p 的任一读取变量 x，无写条件保证任意轮、任意体内位置都有 ρ(x)=ρ₀(x)。表达式纯确定，因此 p 的真值始终等于入口求得的真值 b。
先证明一个体的替换引理。给定与源变量相同的输入环境，对语法结构归纳：普通赋值和 emit 未改，产生相同值和事件；未选中的 if 条件未改，双方走同一支并用归纳假设；到达选中的 if 时，源必选 b 分支，目标恰保留该分支。若选中的 if 所在外层路径没走到，两边都不执行它。故一轮结束后的源变量状态和追加事件完全相同。
再对完成轮数 t 归纳。t=0 时目标只多一个新鲜捕获变量及无事件的条件求值，源状态不变。若完成 t 轮后对应，下一轮用替换引理仍对应。两边的固定次数同为 N，所以恰完成 N 轮后退出，返回表达式也在同一源变量环境中求值。N=0 直接使用基础情形。
这里的观察包含事件顺序，因此证明强于“最后的和一样”。闭合模型的有限次数与有限无环体已保证终止；解释器的预算耗尽只是没有跑完，不是源程序发散的证据。
编译时和运行时分别计账
一次外提至多生成两份体，语法体积为输入大小的线性量级，但公共前后代码被复制，绝不是免费移动。本例按语句节点计，源 code 为7个节点：一个 repeat、两个 emit、一个 if、两支各一条赋值、一个 i 更新。目标为12个节点：捕获、外层 if、两个 repeat，以及两份各4节点的专用体。初始化不计在这份 code 节点统计中。
令 S 为输入语法树节点数，v 为源变量数，d 为所选路径经过的 if 层数加一。理想的一次遍历构造可在线性输出成本内完成；下载参考器为便于检查，沿选定路径递归复制，保守工作界为 O(Sd+Sv+1)。Sv 项支付递归变量集合与确定赋值检查，并非硬件执行成本。其不追求紧界的工作空间上界为 O(S(d+v+1)+1)。名字和集合查找按通常散列模型计，整数和字符串长度成本另计。
原条件若动态执行 m 次，目标执行一次。所选 if 可嵌在偶尔才走的分支中，因此 m 未必等于 N；m=0 时目标反而新增一次计算。长体被复制会增加代码缓存压力，运行时是否更快需要测量。本文只报告语法节点、表达式和控制测试次数，不由它们推断机器耗时。
共同终点任务继续将两个版本分别做计数循环展开。这两个变换可以组合，因为外提后的每一支仍是同一有限计数模型；组合不会许可跨轮重排事件，也不能免掉展开后的剩余轮。
参考资料
[1] Frances E. Allen、John Cocke，A Catalogue of Optimizing Transformations，载于 Design and Optimization of Compilers，1971，pp.1–30；实际所链原扫描pp.11–12，Unswitching。其给出循环不变测试选择两份循环的变换及代码空间代价；本文受限语言、事件归纳和数值例独立编写。
[2] David F. Bacon、Susan L. Graham、Oliver J. Sharp，Compiler Transformations for High-Performance Computing，ACM Computing Surveys26(4)，1994，§2.1及§6.1.4（印刷361页）：正确性观察、循环不变条件和零次执行的异常边界。这里不声称实现其一般数组语言或并行化后续步骤。