一维数组程序的形式验证

Formal Verification of One-dimensional Array Programs

在一个类C小语言Pointer C的程序验证器原型的实现中,设计并实现了对一维数组元素进行赋值的语句的推理规则.该推理规则是Hoare逻辑推理规则的扩展,保证了断言演算中全称量词的合法性,适用于操作数组的程序断言中使用全称量词的情况.然后以冒泡排序程序和用数组实现二叉堆删除程序等操作一维数组的程序的验证为例,展示了该规则设计和实现的正确性,该规则的运用以及循环不变式的书写经验.

This paper proposes a series of inference rules for assignment statement of array elements, which is an expansion of Hoare logaic, guarantee the legality of universal quantifier and can be used on assertions with universal quantifier. And this paper presents the correctness of the inference rules, the application of the rules and the experience of writing invadants, with examples such as bubblesort and array-based binary heap.