Modular Verification of Recursive Programs

TL;DR

This paper proposes a modular reasoning approach to verify recursive programs, simplifying the assertional method of Hoare by establishing properties in stages, demonstrated through a correctness proof of Quicksort.

Contribution

It introduces a modular verification method for recursive programs that enhances the traditional assertional approach, exemplified with Quicksort.

Findings

Modular reasoning simplifies recursive program verification.

Proof of Quicksort correctness using the proposed method.

Enhanced understanding of property establishment in recursive verification.

Abstract

We argue that verification of recursive programs by means of the assertional method of C.A.R. Hoare can be conceptually simplified using a modular reasoning. In this approach some properties of the program are established first and subsequently used to establish other program properties. We illustrate this approach by providing a modular correctness proof of the Quicksort program.