<html>
<head>
<style>
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 10pt;
font-family:Verdana
}
</style>
</head>
<body class='hmmessage'>
<br>> From: pocmatos@gmail.com<br>> Date: Sat, 2 May 2009 00:54:27 +0000<br>> Subject: Re: [plt-scheme] Re: Expressivity gap between formal methods and PL's<br>> To: sk@cs.brown.edu<br>> CC: wookiz@hotmail.com; plt-scheme@list.cs.brown.edu; kfisler@gmail.com; dd@cs.wpi.edu<br>> <br><br>> <br>>> The paper shows how to generate an executable directly from an Alloy<br>>> model. It has some nice twists such as automatically maintaining the<br>>> integrity of the models in the run-time heap. And it *even* generates<br>>> ... drum roll, please ... PLT Scheme code!<br>>><br>>> We have a paper in progress that further shows how to formalize the<br>>> relationship between specification and implementation.<br>>><br>> <br>> I will look into the paper more closely but I don't think this is what<br>> wooks had in mind when he asked for an implementation given a<br>> specification. I think he was more thinking along the lines of having<br>> a way to implement his program in Alloy and then compile it into an<br>> executable that can be ran on a clients machine. I don't think the<br>> Alloy language is ready for this.<div><br></div><div>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. </div><div><br></div><div>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.</div><div><br></div><div><br></div><br /><hr />"
Upgrade to Internet Explorer 8 Optimised for MSN.
" <a href='http://extras.uk.msn.com/internet-explorer-8/?ocid=T010MSN07A0716U' target='_new'>Download Now</a></body>
</html>