[plt-scheme] Re: Expressivity gap between formal methods and PL's

From: wooks . (wookiz at hotmail.com)
Date: Sat May 2 07:06:46 EDT 2009

> From: pocmatos at gmail.com
> Date: Sat, 2 May 2009 00:54:27 +0000
> Subject: Re: [plt-scheme] Re: Expressivity gap between formal methods and PL's
> To: sk at cs.brown.edu
> CC: wookiz at hotmail.com; plt-scheme at list.cs.brown.edu; kfisler at gmail.com; dd at cs.wpi.edu

>> The paper shows how to generate an executable directly from an Alloy
>> model.  It has some nice twists such as automatically maintaining the
>> integrity of the models in the run-time heap.  And it *even* generates
>> ... drum roll, please ... PLT Scheme code!
>> We have a paper in progress that further shows how to formalize the
>> relationship between specification and implementation.
> I will look into the paper more closely but I don't think this is what
> wooks had in mind when he asked for an implementation given a
> specification. I think he was more thinking along the lines of having
> a way to implement his program in Alloy and then compile it into an
> executable that can be ran on a clients machine. I don't think the
> Alloy language is ready for this.
It is what I had in mind. I'm looking at intelligent ways of doing test design and arguing against attempting to derive tests automatically from formal specifications. 
Instead I suggest using the formal specification to generate a test oracle. That argument is strengthened if it is feasible to generate an executable system from the formal specification.

Share your photos with Windows Live Photos – Free.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20090502/58bb45f3/attachment.html>

Posted on the users mailing list.