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

Iago Abal iago.abal at gmail.com
Sat Oct 9 15:44:20 UTC 2010


Hi all,

(Note: Excuse me if my English is not understandable enough.)

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.

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

Note that I'm just talking about analyze a proposal, I know some partners
that could be interested in this kind of project, but it is subject to
discussion.
Bad things for this list: Maybe we could ask "lot of" questions.
Good things for Darcs: We could discover bugs in spec/code.

[1] http://alloy.mit.edu

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


More information about the darcs-users mailing list