算术程序的正确性验证及其实现
该文提出了一个验证有限步终止的算术程序正确性的代数方法。其主要思想是将待验证的程序用实数域上的ＢＳＳ计算模型来模拟，然后将其转化为一个多项式代数方程组，从而把程序的正确性证明问题变为一个方程组零点判定的代数问题。该方法的证明复杂性依赖于程序的执行步骤；其中，对于直线程序，该方法可以给出完全的正确性证明，而对于非直线程序，则可以对任意指定的ｎ，证明程序在ｎ步执行下的正确性。
程序 正确性 验证 算术程序 BSS模型 Groebner基
王继民 李廉
大学计算机科学系
国内会议
浙江金华
中文
69～73
1999-10-01（万方平台首次上网日期，不代表论文的发表时间）