New Handles on Program Correctness

软件工程的主要挑战之一是验证软件的正确性。在八十年代，引入了程序“结果检查”和“结果修正”的方法论。该方法关注的是每输入代码的正确性，而不是完整的程序验证。当前的研究将重新审视结果检查和纠正方法，强调一般的复杂性理论方法，而不是前面追求的特定函数方法。该项目的智力优势在于，它将拓宽我们对如何设计通用程序检查器和校正器的理解，传授在不牺牲正确性的情况下利用快速启发式算法的方法，并深入研究属性测试领域与程序检查和纠正之间的关系。该项目有望对软件的可靠性产生广泛的影响。本研究涉及以下方向：1.刻画具有有效检查器和校正器的一般函数类。提出了一种新的程序检查和纠正模型，在该模型中，检验者和纠正者除了要检查和纠正的程序外，还可以访问一个短的建议字符串。建议字符串在程序的在线检查之前离线计算。这种模型允许处理比以前更一般的函数族。特别是，它允许为许多功能设计单个检查器和校正器，其中每个单独的功能与不同的建议字符串相关联。为程序检查员和校正员寻求新的效率衡量标准，这将绕过现场出现的一些挑战。在建议模型中，建议的长度将被合并到检查过程的复杂性中，并可以与检查者对被检查程序的在线调用次数进行交换。利用性能测试领域取得的显著进展，对程序进行测试和更正。探索程序测试员和校正者的概念如何能够将快速启发式程序转换为正确的程序，并改善平均用例运行时间。

One of the main challenges of software engineering is verifying the correctness of software. In the eighties the methodology of program `result checking' and `result correcting' was introduced. This approach focuses on correctness of the code per input rather than full program verification.The current investigation will revisit the result checking and correcting methodology, emphasizing a general complexity theoretic approach rather than the function specific approach pursued earlier.The intellectual merit of the project is that it will broaden our understanding of how to design general purpose program checkers and correctors, teach methods to exploit fast heuristics without sacrificing correctness, and study, in depth, the relation between the property testing field and program checking and correcting. The project promises to have broad impact on the reliability ofsoftware.This research involves, the following directions:1. Characterize general {\it classes} of functions which posses efficient checkers and correctors.2. Introduce a new model for program checking and correcting in which the checker and correctorhave access to a short advice string in addition to the program to be checked and corrected. The advice-string is computed off-line ahead of on-line checking of programs. Such model allows treating more general function families than previously done. In particular, it allows the design of a single checker and corrector for many functions, where each individual function is associated with a different advice string.3. Pursue new measures of efficiency for program checkers and correctors which will circumvent some of the challenges which arise in the field. In the advice model, the length of the advice will be incorporated into the complexity of the checking procedure and may be traded with the number of on-line calls of the checker to the program to be checked.4. Harness the remarkable progress made in the field of property testing to the testing and correcting of programs.5. Explore how the notions of program testers and correctors may enable the convertion of fast heuristics into correct programs with improved average case running time.