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