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

Ganesh Sittampalam ganesh at earth.li
Sat Oct 9 17:36:07 UTC 2010


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?

> 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.

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.

Cheers,

Ganesh


More information about the darcs-users mailing list