[darcs-devel] Combining Verification Methods for Darcs

[David Roundy]

On Tue, Apr 26, 2005 at 05:18:57PM +0200, Patrik Jansson wrote:
> I work at Chalmers in the Cover project (COVERproject.org) and we have 
> recently started to use the Darcs source code as a case study for our 
> verification tools. Darcs already contains some QuickCheck properties 
> and we will try to use first order logic theorem proving as well (with 
> automatic translation from Haskell using CoverTranslator). So far we 
> have only got to the point of being able to run the CoverTranslator on 
> some of the Patch* modules, without actually proving anything 
> interesting. But we will continue to improve the tool with the aim to 
> proving (or disproving;-) a few properties of the Patch algebra.
> 
> (I just thought you might be interested in knowing that the code you 
> write is used for more than its primary purpose;-)

:)

> So far we have been finding CoverTranslator bugs but if all goes well we 
> could actually help shaking out a few bugs from Darcs itself.

This sounds great!

If you'd like help in providing simplified bits for CoverTranslator to
prove, that would be great.  You might also be interested in the
darcs-conflicts mailing list, which is devoted to the next generation
conflict-handling patch type, which will (crossing fingers) have a number
of commute properties that the current one lacks.

I'd certainly appreciate testing of the new code, and the increased number
of properties that patches are requires to obey may give you smaller bites
to prove at a time.  You could check out the archives for my long email
(maybe the third on the list) discussing commutation properties.  The new
idea is that the commute function will be made as an msum of several
commute functions applied to the pair of patches, in a Maybe-like monad,
which has a third possibility "Failed".  Anyhow, the idea is that each of
these functions would satisfy all the properties for any pair of patches,
with "Unknown" being the result if that particular function doesn't have
anything to say about their commutation.  So (for example) the
trivial_filepatch_commute algorithm says that if two patches are
filepatches and don't affect the same file, they commute trivially.

And if you have any test-related code you'd like to send back (e.g. new
QuickTest tests or other annotations that might help CoverTranslator run),
patches would certainly be welcome.
-- 
David Roundy
http://www.darcs.net