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 <[email protected]> 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
