Email Gateway (Aug 18 2022 at 11:03): Email Gateway (Aug 18 2022 at 11:03):From: Luke Wagner <andhow@gmail.com>
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.
Thank you,
Luke
Email Gateway (Aug 18 2022 at 11:03):From: Tobias Nipkow <nipkow@in.tum.de>
Isabelle let's you generate code from inductive definitions (in certain
cases). But it will still be functional code, not imperative. And it is
unclear to me why you would need Hoare logic to generate the code. The
program already is the code (modulo unparsing it).
Tobias
Luke Wagner wrote:
Email Gateway (Aug 18 2022 at 11:03):From: Gerwin Klein <gerwin.klein@nicta.com.au>
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
Last updated: May 03 2024 at 12:27 UTC