[Xmonad] Proofs of StackSet

[Spencer Janssen]

On Tue, 8 May 2007 15:03:16 +0100
"Neil Mitchell" <ndmitchell at gmail.com> wrote:

> 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

I've applied patches that should fix all of these.

> 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'd like to get this in the main repository.  Can you send a patch (or
some instructions)?


Thanks,
Spencer Janssen