Re: [isabelle] Codegen from Hoare logics?



On Monday 26 November 2007, Luke Wagner wrote:
> Hello, I had a code generation question.
>
> I am interested in imperative programs that are [mechanically] correct
> by construction and I happened upon the "Abstract Hoare Logics" work
> in the AFP.  My question is: can code be automatically generated from
> the commands in a Hoare triple?  I am relatively new to Isabelle, but
> from what I have seen, this seems to be a different situation than
> generating code from a function const.

It's definitely possible in theory to do that for a restricted subset of the 
abstract language (restricted, because the "Basic" command can be any 
function, even one that is not computable). 

We did some experiments with this two years ago and it basically worked. We 
did not use the built-in code generator directly, though, but wrote a small 
bit of ML code ourselves. This might not be necessary any more.

Unfortunately (for you ;-)), we ended up going the other way (parsing) in the 
end, because that fit better with what we wanted to do. So I can't give you 
any concrete code to work from.

Cheers,
Gerwin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.