基于Frama-C的希尔排序形式化验证

Formal Verification of Shell Sort Based on Frama-C

摘要: 希尔排序是一种基于间隔递减的经典排序算法，其正确性对软件可靠性至关重要。本文采用形式化方法，借助Frama-C平台及其ACSL规范语言，对希尔排序程序进行源代码级别的正确性验证。验证过程中的主要难点在于构造嵌套循环的循环不变式，以描述数组的有序性和元素排列性质。通过设计合适的循环不变式，并借助Alt-Ergo、CVC4、Z3等定理证明器进行验证，最终证明了希尔排序程序的功能正确性与内存安全性。

Abstract: Shell sort is a classic sorting algorithm based on decreasing intervals. Its correctness is crucial for software reliability. This paper uses a formal method and based on the Frama-C platform and its ACSL specification language, conducts source code-level correctness verification of the Shell sort program. The main difficulty in the verification process lies in constructing the loop invariants of nested loops to describe the order of the array and the arrangement properties of elements. By designing appropriate loop invariants and using theorem provers such as Alt-Ergo, CVC4, and Z3 for verification, the functional correctness and memory safety of the Shell sort program are ultimately proved.