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

Static Contract Checking for Haskell

D. N. Xu ; S. P. Jones ; Koen Claessen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
ACM Sigplan Notices (0362-1340). Vol. 44 (2009), 1, p. 41-52.
[Artikel, refereegranskad vetenskaplig]

Program errors are hard to detect and are costly both to 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#, but few have been applied to a higher-order lazy functional language, like Haskell. In this paper, we describe a sound and automatic static verification framework for Haskell, that is based on contracts and symbolic execution. Our approach is modular and gives precise blame assignments at compile-time in the presence of higher-order functions and laziness.

Nyckelord: verification, functional language, contract satisfaction, static, contract checking



Denna post skapades 2010-02-25. Senast ändrad 2016-07-01.
CPL Pubid: 114912

 

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers) (2008-2010)

Ämnesområden

Information Technology

Chalmers infrastruktur