[plt-scheme] Schemebelle?

On Mon, Apr 27, 2009 at 10:55 PM, Carl Eastlund <carl.eastlund at gmail.com> wrote:
> On Mon, Apr 27, 2009 at 6:31 PM, Paulo J. Matos <pocmatos at gmail.com> wrote:
>>
>> However, this comes in interesting times. I have been studying the
>> implementation of efficient model checkers for a specific formal
>> language in my PhD. I am doing this in Scheme so I have the models
>> represented as an AST  in Scheme. It is straightforward to dump a
>> scheme/lisp program that 'executes' this specification. How hard is it
>> to integrate it with dracula, I mean, run dracula automatically and
>> interact with it? I guess I could integrate it with ACL2 [unless
>> dracula adds features to ACL2, does it?] but since dracula is scheme
>> already, sending models to acl2, and interacting with it for proofs
>> requiring user intervention might be easier if I reuse parts of
>> dracula code, right?
>>
>> This would allow me 'as a bonus' to perform theorem proving on models
>> besides model checking.
>
> Hmm... depending on exactly what you mean by that, it might not be
> hard at all.  There is an internal API I use to set up new Dracula
> languages; for instance, the ACL2 and Modular ACL2 language levels use
> different languages but the same GUI and the same mechanism for
> communicating with ACL2.  If you had a new language and a new way of
> generating ACL2 code, in theory it shouldn't be too hard to hook it up
> to Dracula's tools.
>

My model checker is a command line tool so I was basically interesting
in using the part of dracula that interfaces with ACL, without using
GUI stuff.

> However, to get started I think you may be best off using Dracula
> as-is: generate an ACL2 implementation of your model however you like,
> save it as a .lisp file, then use Dracula to try to add some proofs to
> it manually.  Once you get some hands-on experience with Dracula and
> ACL2, you'll be in a much better position to decide how to automate
> the process.
>

I can easily generate the lisp file, so after that I will look into
the automation then. Thanks for the suggestion.
I will look into ACL2 page to check out which parts of lisp I can use then.

Cheers,

Paulo Matos

> --
> Carl Eastlund
>



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