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 _______________________________________________ darcs-users mailing list darcs-users@darcs.net http://lists.osuosl.org/mailman/listinfo/darcs-users
