论文标题
QuickSort的转型验证
Transformational Verification of Quicksort
论文作者
论文摘要
许多用于约束逻辑程序（也称为约束角子句（CHC））开发的转换技术在程序验证领域中发现了新的有用应用。在本文中，我们通过基于转换的验证方法来制定非平凡的案例研究。我们考虑使用功能编程语言编写的熟悉的QuickSort程序，并验证了指定程序中定义的函数的预期正确性属性的PRE/-postConditions。我们通过：（1）将它们转换为CHC，（2）通过删除所有列表出现来转换CHC，以及（3）通过使用Booleans和Integers使用Eldarica求解器来检查转换后的CHC的满足性。第（2）点提到的转换需要扩展算法，以消除先前工作中提出的归纳定义的数据结构，因为在转换的一个阶段，我们用作引理的某些特性，这些属性已在先前的阶段证明。
Many transformation techniques developed for constraint logic programs, also known as constrained Horn clauses (CHCs), have found new useful applications in the field of program verification. In this paper, we work out a nontrivial case study through the transformation-based verification approach. We consider the familiar Quicksort program for sorting lists, written in a functional programming language, and we verify the pre/-postconditions that specify the intended correctness properties of the functions defined in the program. We verify these properties by: (1) translating them into CHCs, (2) transforming the CHCs by removing all list occurrences, and (3) checking the satisfiability of the transformed CHCs by using the Eldarica solver over booleans and integers. The transformation mentioned at Point (2) requires an extension of the algorithms for the elimination of inductively defined data structures presented in previous work, because during one stage of the transformation we use as lemmas some properties that have been proved at previous stages.
