基于扩展逻辑变换系统_μTS证明循环优化正确性

循环优化对于提高Cache性能、发掘程序的并行性以及减少执行循环的开销都有着重要的作用,证明带循环优化功能的现代编译器的正确性已成为可信编译的一个挑战性的问题.形式化证明一个羽翼丰满的优化编译器本质上是不可行的,可以使用替代的方法,即不是证明优化编译器本身,而是形式化证明每一次循环变换前后编译对象的正确性.提出一种新颖的基于扩展逻辑变换系统μTS来证明循环优化正确性的方法.系统μTS在逻辑变换系统TS的基础上扩展了若干条派生规则,经谓词抽象将源程序与目标程序转换为形式化Radl语言后,使用μTS的派生规则能证明常见循环变换的正确性,如循环融合、循环分配、循环交换、循环反转、循环分裂、循环脱皮、循环调整、循环展开、循环铺盖、循环判断外提、循环不变代码外提等.循环优化可以看作一系列循环变换的组合,从而系统μTS能证明循环优化的正确性.为了支持自动化证明循环优化的正确性并出示证据,进一步提出了一个辅助证明算法.最后通过一个典型实例对这一方法进行了详细的阐述,实际效果表明了该方法的有效性.该方法对设计高可信优化编译器具有重要的指导意义.

Radl形式规格说明相对正确性研究

在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题.提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明Si等价来实现,而Si使用PAR方法和PAR平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法.使用Radl语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值.