[darcs-users] Feedback please, Darcs subsystem for lightweight formal verification

Jason Dagit dagitj at gmail.com
Sat Oct 9 17:52:01 UTC 2010


Iago,

Thanks for your interest.  I think this sounds like a really exciting
project.  It's exciting that you're interested in using model checking on
darcs!  I hope you pick this project and make progress.


> Hi Iago,


> On Sat, 9 Oct 2010, Iago Abal wrote:


> > I will try to be brief but concise. I'm a MSc student doing a
> formal-methods

> course about "analysis, modeling and testing". This course has a project

> component which consists on modeling a problem using Alloy[1], verify

> (lightweight approach) properties about the problem using that model, code

> the problem (if there is no available code) annotating the code with

> contracts and, finally, test it. Of course, the final goal is to ensure
> that

> the real code actually meets its specification.


> One thing I'm confused about here - can Alloy actually model check

Haskell? If not, how would you be able to ensure anything about the real

code?


If I understand Iago correctly, the goal is to check the specification
abstractly and then later check the code against tests derived from the
specification / model checking.


>
> > Ok so... the project is done by groups and we are collecting proposals
> for

> this project, and, I was thinking in something related to Darcs. I have to

> take more serious look for this, but currently I think that model

> patch-theory and test Darcs.Patch.* code could be a choice. My question
> is,

> if someone could propose Darcs subsystems that 1) have a well-documented

> specification complex enough to be of interest modeling and verifying it,
> 2)

> have small/medium-size implementation understandable just with few weeks
> of

> work 3) it is of interest for the Darcs community (I think this point is

> important if we want to get some help from you like answering "boring

> questions").


> I think that some of the internals of Darcs.Patch would be a reasonable

candidate, if you start small and work your way up as time permits.


> I'm not entirely sure what kind of specification you want, but darcs

patches satisfy various equational laws, and also have the higher-level

property that commuting two patches in a sequence doesn't affect the final

result of that sequence.


Resources to help you get started with this include:
  * My MS thesis about darcs: http://files.codersbase.com/thesis.pdf
  * My thesis talk slides: http://files.codersbase.com/thesistalk.pdf
  * Judah Jacobson's formalized patch theory:
http://www.math.ucla.edu/~jjacobson/patch-theory/
  * Ian Lynagh's Camp: http://projects.haskell.org/camp/

Camp is interesting as it has almost the same underlying theory as darcs but
there have been more efforts to formalize it.  In this case, using the
theorem proving language Coq.  Just check around on the camp site and you
should find links to the proofs.


>
> I think if you started with "hunk" patches on a single file, then you

would have a tractable problem to begin with which you could then build

on. I'd be happy to help with understanding the code and how it's meant to

behave.


Some things of interest that you might be able to check:
  * Are token replace patches well behaved when commuting with hunk patches?
  * Are there cases where darcs algorithms go exponential in run-time?
  * Interaction between setpref patches and normal patches
  * Not patch theory related: Exception handling, cleaning up, and
transactional properties

I think Ganesh is right about starting small.  For example start with
hunk-hunk commutes and see what you get.  Even simpler might be file
add/remove patches.  I noticed that the Alloy tutorial models a unix file
system.  That may actually be a great place to start with your work.  Then
build up to transformations on the file system objects, and so on.  I've
been thinking about starting from that point in a language such as Agda.  If
only I had more spare time.

You should not feel shy about asking us questions on the list.  Rigorously
verifying darcs is of great interest to quite a few of us and the
discussions are very helpful to everyone.

I hope that helps.
Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.osuosl.org/pipermail/darcs-users/attachments/20101009/a356e684/attachment-0001.html>


More information about the darcs-users mailing list