Contract Checking for Feldspar

Abstract

"Contracts play an important role in the construction of robust software" [13]. Program invariants are expressed in familiar notation with known semantics by using contracts. Assertions based on contracts has been widely used in procedural and object-oriented languages. Findler and Felleisen presented contracts to higher-order functional languages and Hinze, Jeuring et al. implemented contracts for Haskell as a library.<br><br> In this thesis, a contract language is introduced and implemented for three libraries of the functional language Feldspar. Feldspar is a domain speci c language (DSL) for Digital Signal Processing, embedded in Haskell, and generating C code. Contracts are written for functions of the Core Array, Vector and Matrix libraries and also for some practical Feldspar functions.<br><br> A contract language should create an informative error message to report the violation and the violator when a contract fails. In this thesis, an error message speci es the cause of violation by reporting the le name, line number and if an argument of a function is to blame, this argument is also mentioned in the error message.<br><br> Contract checking can be done statically or dynamically. Static checking concentrates on complete checking of limited speci cations at compile time. Dynamic checking focuses on incomplete checking of expressive speci cations, and detects errors during run time. Contracts that are written in this thesis are checked with a dynamic contract checker. Furthermore, they are tested with QuickCheck, to ensure that contracts satisfy given properties. The result of these tests shows that the contracts hold their properties and we cannot nd any bugs in the contracts written; so we conclude that all of the contracts written satisfy their properties.<br><br> The assert function is implemented for the Feldspar language to have contracts in the language. This assert function is translated to the C assert function which suggests the opportunity for verifying C program properties with contracts too. When a contract fails, Feldspar programmers can narrow down the cause of the violation with the help of a precise error message generated by the contract checker. During work on this thesis, we found several bugs in the Feldspar implementation by using the contract checker.