A QUANTIFIER-ELIMINATION BASED HEURISTIC FOR AUTOMATICALLY GENERATING INDUCTIVE ASSERTIONS FOR PROGRAMS

用量词消除的一个方法为自动地产生程序 invariants/inductive 断言被建议。给一个程序，引入的断言，在一个理论作为 parameterized 假设了公式，与程序地点被联系。在引入的断言的参数被由保证引入的断言被导致程序的联系地点的所有实行路径确实保存在参数上产生限制发现。方法能被用来发现在一个环的入口仍然保持不变的变量不变性质的循环。parameterized 公式能被一个一个地考虑实行路径连续地精制；启发规则能为决定路径在被考虑的顺序被开发。如果可得到，象前提和帖子一样的变量调节的节目的初始化，能也被用来进一步精制假设不变。方法不取决于一个程序的前提 andpostcondition 的可获得性。这样产生的参数上的限制为参数的可能的价值被解决。如果没有解决方案是可能的，这意味着那一假设形式不变不是可能的在做产生联系确认条件的假设 / 近似下面为循环存在。不同如果参量的限制是可解决的，那么在为产生这些限制的方法上的某些条件下面，最强壮可能假设形式不变能从参量的限制的很一般的答案被产生。途径为表示断言象 Presburger 算术一样用多项式方程的连词的逻辑语言被说明。