[plt-scheme] Schemebelle?

On Mon, Apr 27, 2009 at 11:22 PM, Carl Eastlund <carl.eastlund at gmail.com> wrote:
>
> 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.
>

hummmf, that makes it hard to proceed since the model checker should
be able to run in terminal only PCs. Anyway, I guess that by
integrating this I may say that the prover tool requires GUI access.
Lets see how it goes. It's not the main part of the PhD anyway. Just
thought that if it were simple it could be interesting.

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

OK, thanks!

> --
> Carl Eastlund
>



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