Bug in the proof of Data.FiniteMap and DData.Map

Daan Leijen daanleijen at xs4all.nl
Mon Mar 29 11:14:53 EST 2004

On Fri, 26 Mar 2004 09:46:53 +0100, Robert Will <robertw at stud.tu-ilmenau.de> wrote:

> The precondition-problem is not easy to fix.  However, I ackknowledge that
> your balancing-checks are really good evidence for the correctness of the
> algorithm.  (I didn't notice them first, because you checked via an
> external function, not in a smart constructor.  And I looked only there.)
> Well, having mathematically unproven code is a common thing and should
> indeed be no problem.  It's just that I personnally prefer algorithms that
> I understand, i.e. I know why they are correct.  For Adam's algorithm this
> is not the case, and I think other people would have serious problems,
> too, when explaining "under what (pre)condition does 'balance' produce a
> correctly balanced tree?" and "why does 'join' always observe that
> precondition?".

I agree with this and I will take a close look at your proofs. It would
be good to flesh out the true pre-conditions to Adams' "join" operation
and show that these are fullfilled in DData/Data.FiniteMap.

All the best,

More information about the Libraries mailing list