[plt-scheme] Schemebelle?

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.

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.

-- 
Carl Eastlund