一种交互式的不变量动态发现编配工具

摘要

发现程序中隐含程序不变量是实现高层次行为合约、提高程序质量的关键.重点研究了不变量的动态发现方法与程序编配原理,并在传统的编配方法基础上实现了交互式的石鼓编配工具.该工具具有预设观测点和观测变量等功能,并通过将运行轨迹收集到数据库中来实现不变量分析.并详细说明了采用内嵌法的编配工具的总体结构及实现过程.实验证明石鼓编配工具能更方便有效地发现不变量.