UCAM-CL-TR-737: Static contract checking for Haskell
tech-r...@cl.cam.ac.uk
Static contract checking for Haskell
Na Xu
Technical report UCAM-CL-TR-737, University of Cambridge,
Computer Laboratory, PhD thesis, December 2008, 175 pages.
This document is now available at
http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-737.html
Abstract:
Program errors are hard to detect and are costly, to both programmers
who spend significant efforts in debugging, and for systems that are
guarded by runtime checks. Static verification techniques have been
applied to imperative and object-oriented languages, like Java and C#,
for checking basic safety properties such as memory leaks. In a pure
functional language, many of these basic properties are guaranteed by
design, which suggests the opportunity for verifying more sophisticated
program properties. Nevertheless, few automatic systems for doing so
exist. In this thesis, we show the challenges and solutions to verifying
advanced properties of a pure functional language, Haskell. We describe
a sound and automatic static verification framework for Haskell, that is
based on contracts and symbolic execution. Our approach gives precise
blame assignments at compile-time in the presence of higher-order
functions and laziness.
First, we give a formal definition of contract satisfaction which can be
viewed as a denotational semantics for contracts. We then construct two
contract checking wrappers, which are dual to each other, for checking
the contract satisfaction. We prove the soundness and completeness of
the construction of the contract checking wrappers with respect to the
definition of the contract satisfaction. This part of my research shows
that the two wrappers are projections with respect to a partial ordering
crashes-more-often and furthermore, they form a projection pair and a
closure pair. These properties give contract checking a strong
theoretical foundation.
As the goal is to detect bugs during compile time, we symbolically
execute the code constructed by the contract checking wrappers and prove
the soundness of this approach. We also develop a technique named
counter-example-guided (CEG) unrolling which only unroll function calls
on demand. This technique speeds up the checking process.
Finally, our verification approach makes error tracing much easier
compared with the existing set-based analysis. Thus equipped, we are
able to tell programmers during compile-time which function to blame and
why if there is a bug in their program. This is a breakthrough for lazy
languages because it is known to be difficult to report such informative
messages either at compile-time or run-time.
--
University of Cambridge, Computer Laboratory,
Technical Reports (ISSN 1476-2986)
http://www.cl.cam.ac.uk/techreports/