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

> 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.
http://clk.atdmt.com/UKM/go/134665338/direct/01/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20090502/58bb45f3/attachment.html>