Revision control systems (RCS) like cvs, opencvs, subversion and arch are commonly used to develop software projects. Unfortunately, they all tend to suffer from a lack of formal specification, leading to bugs or incoherent behaviour. Recently a new RCS has emerged that is more well specifed, darcs.

Darcs has a powerful ``theory of patches'' underpinning its design, and it is greatly strengthened by this. Its behaviour is easier to understand, and allows sophisticated version control operations beyond that of other systems. However, the darcs model has not been formalised in any way, and there exist no proofs of its soundness. The darcs model can be considered a first draft for a formal model of an RCS based on patches.

The goal of this project is to develop a formal model of patches based on the darcs model. You will develop a model of the theory in the Isabelle theorem prover, and develop various proofs relating to the theory. Once you have a checked model, you will use this to implement a prototype RCS in Haskell.

• Core requirements:
  • At a minimum you should develop a formal model of the basic theory of patches. This should then be used to implement a prototype revision control system.
• Extra tasks for the ambitious:
  • You may be able to produce proofs of the soundness of various darcs operations, or develop new operations.
  • Another option would be to work on darcs itself, and verify that the implementation matches the formal model. This will require a good knowledge of Haskell.
  • A good formal model and an implementation would be of publishable quality
  • Can the model be adapted to other patch/merge systems, for example rsync or unison?

• Darcs theory of patches
• Benjamin Pierce's Unison and Harmony projects on data sychronisation.
• Norman Ramsey's filesystem algebra in: An Algebraic Approach to File Synchronization
• The Isabelle theorem prover
• Rsync, similar idea to unison. Details of the merge algorithm in Andrew Tridgell's PhD thesis