<p> The Haskell programming language uses type classes to deal with overloading. Functions
are overloaded by defining some types to be instances of a class. A meaningful instance should satisfy the invariants of the class.</p> <p> In this thesis we present one method to validate the type instances of classes informally, and another one to verify them in a formal way.</p> <p> The first method uses QuickCheck, which is an automatic testing tool for
Haskell programs. We introduce how to specify the properties of type classes in QuickCheck by some examples, and I also present testing for Haskell standard types and classes.</p> <p> The second method I adopted uses the theorem prover Isabelle/HOL. To facilitate the usage of Isabelle/HOL for Haskell programmers, I define a set of translation rules from Haskell programs to Isabelle/HOL, and design a simple automatic translating tool based on those rules. Logical differences between Haskell and Isabelle/HOL need to be considered in the translation. For example Isabelle/HOL is not suitable to describe the semantics of lazy evaluation and of Haskell functions that are non-terminating. I also prove some type instances to illustrate how the properties are verified in Isabelle/HOL.</p> / Thesis / Master of Applied Science (MASc)
| Identifer | oai:union.ndltd.org:mcmaster.ca/oai:macsphere.mcmaster.ca:11375/21329 |
| Date | 09 1900 |
| Creators | Wang, Feng |
| Contributors | Kahl, Wolfram, Computing and Software |
| Source Sets | McMaster University |
| Language | en_US |
| Detected Language | English |
| Type | Thesis |
Page generated in 0.002 seconds