CSE230 Fa16 - Assert



Assertions

As a warm up, first lets recall how we can specify and verify assertions with Refinement Types.

Dead Code

Recall from lecture, that we can define a function that should never be called.

> {-@ die :: {v:String | false} -> a @-}
> die str = error ("Oops, I died!" ++ str)

We can use this function in all those places where we need to handle some case that we can know (and want to prove) will never happen at run-time.

Here’s a variant of die that we will use for those places where you need to fill in code: 
> {-@ fixme :: {v:String | false} -> a @-}
> fixme str = error ("Oops, you didn't fill in the code for: "++ str)

Assertions

Lets define a refined type for the Bool that is always true:

> {-@ type TRUE = {v:Bool | Prop v} @-}

Notice that we can now assign the type TRUE to any Bool expression that is guaranteed to evaluate to True:

> {-@ one_plus_one_eq_two :: TRUE @-}
> one_plus_one_eq_two = (1 + 1 == 2)

But of course, not to expressions that are False:

> {-@ one_plus_one_eq_three :: TRUE @-}
> one_plus_one_eq_three = (1 + 1 == 3)  -- TYPE ERROR

We can now use TRUE to define a lAssert function:

> {-@ lAssert :: TRUE -> TRUE @-}
> lAssert True  = True
> lAssert False = die "Assert Fails!"

Now, we can call lAssert only on expressions that we want to prove always hold, for example:

> propOk   = lAssert (1 + 1 == 2)

But if we try to lAssert bogus facts then they are rejected:

> propFail = lAssert (1 + 1 == 3) -- TYPE ERROR

Divide By Zero

Finally, lets write a safe divide by zero operator (that we will use later)

> {-@ divide :: Double -> {v:Int | v /= 0}-> Double @-}
> divide n 0 = die "oops divide by zero"
> divide n d = n / (fromIntegral d)