Department of Computer Science and Technology

Technical reports

Static contract checking for Haskell

Na Xu

December 2008, 175 pages

This technical report is based on a dissertation submitted August 2008 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Churchill College.

DOI: 10.48456/tr-737

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.

Full text

PDF (1.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-737,
  author =	 {Xu, Na},
  title = 	 {{Static contract checking for Haskell}},
  year = 	 2008,
  month = 	 dec,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-737.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-737},
  number = 	 {UCAM-CL-TR-737}
}