文档介绍：COCV 2007
Distilling Programs for Verification
. Hamilton 1 ,2
School puting
Dublin City University
Dublin, IRELAND
Abstract
In this paper, we show how our program transformation algorithm called distillation can not only be used for
the optimisation of programs, but can also be used to facilitate program verification. Using the distillation
algorithm, programs are transformed into a specialised form in which functions are tail recursive, and very
few intermediate structures are created. We then show how properties of this specialised form of program
can be easily verified by the application of inductive proof rules. We therefore argue that the distillation
algorithm is an ideal candidate for inclusion pilers as it facilitates the two goals of program
optimization and verification.
Keywords: transformation, optimization, proof, verification
1 Introduction
In 2004, the puting mittee initiated a number of ‘Grand
Challenges’ aimed at stimulating long term research in key areas puting
science. The sixth challenge which was identified was that of dependable systems
evolution, which was inspired by the idea of a piler [8], which is a
compiler that guarantees the correctness of a program before running it.
In this paper we present a program transformation algorithm called distillation
which we argue provides a major step towards the dream of a piler.
The distillation algorithm [5] was originally devised with the goal of eliminating in-
termediate data structures from functional programs. A number of program trans-
formation techniques have been proposed which can eliminate some of these inter-
mediate data structures; for example partial evaluation [9], deforestation [25] and
pilation [22]. Although pilation is strictly more powerful than
both partial evaluation and deforestation, Sørensen has shown that pila-
tion (and hence also partial evaluation and deforestation) can only produce a linear
speedup in programs [19]. Distillation, however