基于时序逻辑证明编译优化程序变换的保义性

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