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

On Fri, May 1, 2009 at 8:54 PM, Shriram Krishnamurthi <sk at cs.brown.edu> wrote:
> Sorry I've dozed through most of this thread, but:
>
>> Alloy is relational logic without an execution model.  It's
>> declarative. You write your model declarative, write a couple of
>> facts and that's it. FAR, FAAAAAAAAR, away from an 'executable' and
>> generating an executable directly from an Alloy mode wouldn't even
>> make sense.
>
> In that case, it is just as well that we named our system Alchemy:
>
> http://www.cs.brown.edu/~sk/Publications/Papers/Published/kdfy-alchemy-trans-alloy-spec-impl/
>

I skimmed the paper... very nice.

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

My paragraph regarding that Alloy is a declarative language with no
execution model is still true and it is far from an executable (as in
a program ready to be deployed). Just the lack of output and input
primitives turn the language into an environment where this couldn't
happen.

You can always implement in alloy a specific execution model but it
will never be what the original poster asked for. I did this to model
check event-b by encoding into alloy in:
http://dx.doi.org/10.1007/978-3-540-87603-8_34

I will however read your paper carefully, so I am sorry if I made any
incorrect assumption about it.
> Since this is pretty off-topic for this list, perhaps direct questions
> about Alchemy should be addressed to Dan and Kathi (CCed) and me.
>
> Shriram
>



-- 
Paulo Jorge Matos - pocmatos at gmail.com
Webpage: http://www.personal.soton.ac.uk/pocm