[plt-scheme] Schemebelle?

On Mon, Apr 27, 2009 at 7:15 PM, Paulo J. Matos <pocmatos at gmail.com> wrote:
> 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.

I suspect you will find this approach very difficult.  If ACL2 fails
to verify the property you generate for the code you generate, you
will get a large volume of output, and you will need to change some
part potentially in the middle of your code.  A GUI gives you a lot of
tools to inspect that output and change that code.  With a
command-line utility, you'll be kind of stuck.

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

The Dracula documentation will help with that, especially because
Dracula does not support everything in ACL2 (and the documentation
will help clarify which parts).  Most of the programming tools
(built-in functions, macros, etc.) are supported, but some of the
theorem proving tools and the (unhygienic, non-phase-respecting)
macro-writing tools are unsupported.

-- 
Carl Eastlund