While Loops in Coq

TL;DR

This paper introduces a method for integrating while loops into a Coq-embedded imperative language, addressing the challenge of termination proofs for non-terminating or partial programs.

Contribution

It presents a novel approach for defining possibly non-terminating recursive functions in Coq, enabling the verification of while loops.

Findings

Successfully proved termination and correctness of linked list programs.

Provided a general method for defining non-terminating recursive functions in Coq.

Enhanced the expressiveness of Coq for imperative programming.

Abstract

While loops are present in virtually all imperative programming languages. They are important both for practical reasons (performing a number of iterations not known in advance) and theoretical reasons (achieving Turing completeness). In this paper we propose an approach for incorporating while loops in an imperative language shallowly embedded in the Coq proof assistant. The main difficulty is that proving the termination of while loops is nontrivial, or impossible in the case of non-termination, whereas Coq only accepts programs endowed with termination proofs. Our solution is based on a new, general method for defining possibly non-terminating recursive functions in Coq. We illustrate the approach by proving termination and partial correctness of a program on linked lists.