Assignment 4 (Axiomatic Semantics; QuickCheck)

Due 8 March

Email me your solution

References

The assignment refers to the axiomatic semantics of the language IMP. In particular we refer to the proof rules in Section 6.4 on p.89 of Winskel's book.

We will experimentally validate these rules using QuickCheck.

Example I

Save the following in a file Test.hs. 

{-# -set -package QuickCheck #-}

module Test () where

import Debug.QuickCheck
import Debug.QuickCheck.Batch
import Debug.QuickCheck.Poly
import Debug.QuickCheck.Utils

prop_RevRev xs = reverse (reverse xs) == xs
  where types = xs::[Int]

prop_Rev xs = reverse xs == xs
  where types = xs::[Int]

The first property asserts that for any list of integers, reversing the list twice results in the original list. The second property asserts every list of integers is identical to its reverse. Here is a sample session in which I tried to use quickCheck to verify these assertions: 

*Test> quickCheck prop_RevRev
quickCheck prop_RevRev
OK, passed 100 tests.
*Test> quickCheck prop_Rev
quickCheck prop_Rev
Falsifiable, after 2 tests:
[-1,-4,-4]

Example II

Here is an example that is more relevant to the assignment. 

{-# -set -package QuickCheck #-}

module ImpQC () where

import Debug.QuickCheck
import Debug.QuickCheck.Batch
import Debug.QuickCheck.Poly
import Debug.QuickCheck.Utils

import Imp

factSpec n = product [1..n]

data Size = Small | Medium | Large deriving Show

size n | n < 3 = Small
       | n < 10 = Medium
       | otherwise = Large

prop_fact n = n >= 0 ==> collect (size n)$
                         factSpec n == factRun n 
  where factRun n = 
            case lookup "result" (runState [("n",n)] (cexec factc)) of
              Just v -> v
              Nothing -> error "fact implementation gives an error"

The code refers to the file Imp.hs developed earlier in the semester. We start by writing a specification for factorial in Haskell. Next we classify the inputs into three categories: Small, Medium, and Large. The property we are trying to prove is a conditional property that requires the condition n >= 0. It asserts that the implementation of factorial in IMP and its evaluation using our evaluation rules is consistent with the specification. Try experiment with changes to the specification or changes to the implementation and see if the errors are detected.

Assignment

The actual assignment is to write properties for the proof rules of the axiomatic semantics and to test them.
sabry ... cs indiana edu