论文部分内容阅读
基于时序逻辑CTL（computation tree logic）的一种扩展CTL-FV对优化编译中的语句交换和变量替换这两种常见变换的保义性条件给出了形式刻画，采用含条件重写规则定义了保义语句交换 Texch和保义变量替换 Texch并基于一种归纳证明框架对它们的保义性进行了证明．此外，基于变换‰对程序基本块内保依赖语句重排的保义性也给出了一种构造性的证明．