[Xmonad] Proofs of StackSet

[Neil Mitchell]

Hi,

{- ICFP referees look away now -}

Dons asked me to check some of the StackSet code for potential pattern
match errors, and indeed, there are some. I used Catch
(http://www-users.cs.york.ac.uk/~ndm/catch/) to do all the testing.

The first thing I had to do was apply a 2 line patch to get that
module building with Yhc/nhc, to do with defaulting. Next I ran the
program and found:

1) view related:

* view calls error, this clearly makes it possible to crash.

* raiseFocus calls view

2) head related:

* promote calls head, in a potentially unsafe manner

3) tail related:

* swap calls tail, again potentially unsafe. This one is easy to fix,
simply use drop 1. This also means that promote could crash due to
swap.

4) fromJust related:

index calls fromJust, which means that it may crash. This means that
all functions calling index are potentially unsafe, including: delete,
insert, promote, push, shift, view, raiseFocus

I took a look at delete, and it looks like the safety depends on the
stacks and the cache all agreeing - plus possibly some other
invariants. You could probably rewrite some of this code to be more
rebust, and gain a proof of safety.

5) everything else:

Everything else is safe, apart from (potentially) the Ord instances
passed around - I abstracted them away for the testing of Data.Map.
Realistically, I think you are fine on this point. This means you have
a proof of pattern match safety for:

screen, peekStack, empty, peek, member, rotate, workspace, visibleWorkspaces


No changes were required for testing (other than the 2 line one for
Yhc) - the test sits in a separate module and is very simple:

main =
    screen ||| peekStack ||| index ||| empty ||| peek ||| push |||
delete ||| member |||
    raiseFocus ||| rotate ||| promote ||| shift ||| view ||| workspace
||| insert |||
    visibleWorkspaces ||| swap

I hope some of that is useful to you. The testing is 100% automatic
and pretty easy to run, once you have Yhc and Catch installed and
configured. You have two choices related to pattern match failure:

1) Ignore it, guard against with QuickCheck
2) Prove it, using Catch

You also have three options regarding Catch use:

1) Integrate the 2 line change, add the Catch module testing framework
in so anyone with Catch installed can replicate these tests - and
check you don't get worse.
2) Have a catch branch, which has the library driver and the patch.
This would be a really small branch :-)
3) Don't do anything, I can continue to check things occasionally.

I'm on #haskell as ndm, so let me know if you want any help running any of this.

Thanks

Neil