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

[Iago Abal]

Thanks for your (really quick) replies, I'm very pleased to see that this
project is of interest for some of you.

On Sat, Oct 9, 2010 at 6:52 PM, Jason Dagit <dagitj at gmail.com> wrote:

> 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.
>
Exactly. As I said, Alloy is a lightweight approach, so we will prove things
about a *model* of the real system and not about the real system itself. But
contracts and testing will let us to *believe* that the real system
corresponds to our model and satisfies its properties (produce code refining
specification is not part of the project goals).

One of our "problems" is the lack of good support for design-by-contract in
Haskell. The "standard way" will be ".NET + Contracts" though course-teacher
said to be interested on modeling Darcs and he accepts to work with Haskell
using "something" for contracts, and QuickCheck/SmallCheck for testing.

>
>
>>
>> > 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/<http://www.math.ucla.edu/%7Ejjacobson/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.
>
>
Thanks for the resources links! I will take a look this days to get the big
picture and have some idea of the complexity of formalizing all the patch
stuff.

Answering Ganesh:

> I'm not entirely sure what kind of specification you want
>
A Darcs repository is consistent iff P holds, commuting patches A and B
under conditions C is a valid operation, etc. I don't know a lot about Darcs
theory, but I think that patch commutation is an important thing and it
could be the center of the verification effort.


>
>> 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.
>
> Yes, right, the idea is to start small and work, at least, until get a
model with enough complexity for the course goals. I hope to be able to get
something interesting for Darcs too -- I know last year there was a project
related to model Subversion but it was not completed (so, it was
something-like-subversion).


> 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
>
Yeah, that helps, thanks!


-- 
Iago Abal Rivas
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.osuosl.org/pipermail/darcs-users/attachments/20101009/a3298619/attachment.html>