软件学报

作者：江南，汪吕蒙，张晓瞳，何炎祥

单位：江南，湖北工业大学 计算机学院, 湖北 武汉 43006811,汪吕蒙，武汉大学计算机学院, 湖北 武汉 43007202,张晓瞳，武汉大学计算机学院, 湖北 武汉 43007203,何炎祥，武汉大学计算机学院, 湖北 武汉 43007204

关键词：机械化验证;高效迭代算法;支配节点

基金：国家自然科学基金(61972293);国家留学基金委地方合作项目(201808420414)

迭代计算数据流等式的解,是数据流分析的常用方法.计算支配节点,从而识别自然循环,是许多现代编译器优化分析的重要组成部分.机械化验证高效的求解支配节点的算法通常是获得一个实际的“验证编译器”不可或缺的一部分.为了形式化证明一个高效的迭代求解严格支配节点的算法(CHK),首先建立了值域是逆序列表集合的半格结构,逆序列表中的元素是控制流图中节点的逆后序遍历次序,并证明了它是一个半格,其偏序满足上升链条件.然后使用半格结构,实现了一个基于工作表的Kildall迭代算法,计算严格支配节点.接下来,首先给出了控制流图中支配节点的定义性规范和相关性质定理,然后构造并证明了迭代求解算法所满足的重要性质.利用这些性质定理,相对于定义性规范,证明了该迭代求解算法的正确性和完备性.最后进行总结,并讨论未来工作.整个形式化开发使用的是定理证明助手Isabelle/HOL.

来源：2022年第6期

《软件学报》期刊编辑部

查看软件学报杂志2022年第6期