CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

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

Nils Anders Danielsson (Institutionen för datavetenskap, Funktionell programmering) ; Patrik Jansson (Institutionen för datavetenskap, Funktionell programmering ; Institutionen för datavetenskap, Programmeringslogik)
Proceedings of the 7th International Conference on Mathematics of Program Construction, MPC 2004, LNCS 3125 p. 85-109. (2004)
[Konferensbidrag, refereegranskat]

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 others' 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.

Denna post skapades 2006-10-09. Senast ändrad 2014-09-02.
CPL Pubid: 8908


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för datavetenskap, Funktionell programmering (2002-2004)
Institutionen för datavetenskap, Programmeringslogik (2002-2004)


Information Technology

Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:

Precise Reasoning About Non-strict Functional Programs; How to Chase Bottoms, and How to Ignore Them