Blog articles/Testing

< Blog articles

Contents 1 Type system enforcement 2 Testing, correctness and proofs 2.1 QuickCheck 2.2 HUnit 2.3 Catch 3 Proofs 3.1 GADTs 3.2 Coq 3.3 Isabelle 3.4 Related work 4 Further reading

1 Type system enforcement

• A bright future: security and modern type systems
• Can your type checking system do this?

2 Testing, correctness and proofs

2.1 QuickCheck

• Introduction to QuickCheck
• QuickChecking a window manager
• Robustness and QuickCheck
• Parsec Parser Testing with QuickCheck
• QuickCheck : Why Testing code should be Laissez-faire
• Calculating the reflect-rotate-translate normal form for an isometry of the plane in Haskell, and verifying it with QuickCheck.
• "Testing Haskell with QuickCheck"

2.2 HUnit

• On Unit Testing and Type Safety
• Getting started with HUnit
• Unit testing with HUnit

2.3 Catch

• Does XMonad crash? On proving pattern coverage with Catch
• Preconditions on XMonad
• Equational Reasoning in Haskell

3 Proofs

3.1 GADTs

• Developing Programs and Proofs Spontaneously using GADT

3.2 Coq

• Strong specifications in Coq: the type says everything
• Proving the monad laws in Coq
  • Introduction
  • The First and Second Laws
  • The Third Law
• Strongly Specified Functions

3.3 Isabelle

• Proving Haskell correct with Isabelle/HOL

3.4 Related work

• See the section on theorem provers

4 Further reading

• Research papers on testing, proofs and correctness

Recent content is available under a simple permissive license.