Chasing Bottoms: A Case Study in Program Verification in the Presence of Partial and Infinite Values

Chasing Bottoms: A Case Study in Program Verification in the Presence of Partial and Infinite Values
Nils Anders Danielsson and Patrik Jansson
Proceedings of the 7th International Conference on Mathematics of Program Construction, MPC 2004, LNCS 3125, 2004. Copyright © Springer-Verlag. Accompanying library: Chasing Bottoms. Extended version with most proofs available, see the first part of my licentiate thesis. [ps.gz, pdf]

Abstract

This work is a case study in program verification: We have written a simple parser and a corresponding pretty-printer in a non-strict functional programming language with lifted pairs and functions (Haskell). A natural aim is to prove that the programs are, in some sense, each other's inverses. The presence of partial and infinite values in the domains makes this exercise interesting, and having lifted types adds an extra spice to the task. We have tackled the problem in different ways, and this is a report on the merits of those approaches. More specifically, we first describe a method for testing properties of programs in the presence of partial and infinite values. By testing before proving we avoid wasting time trying to prove statements that are not valid. Then we prove that the programs we have written are in fact (more or less) inverses using first fixpoint induction and then the approximation lemma.

Errata

Section 6: The third and fifth occurrences of the word "total" should be replaced by "total and finite", and the two occurrences of the text "not total" should be replaced by "partial or infinite".