[Why3-club] [Fwd: Why3 AST (abstract syntax tree) generator]

mtkhan at risc.uni-linz.ac.at mtkhan at risc.uni-linz.ac.at
Fri Sep 14 15:58:29 CEST 2012


Hi Christophe,

Thanks for your recommendation; just wondering that if you
already have a Why3 AST generator in Ocaml then don't you
think ocamljava.x9c.fr kind of integration is helpful.

Of course writing pretty printer is what I am planned to
do but still is far better and almost error free if already
have the developed AST generator for Why3.

Thanks.

regards,
taimoor



---------------------------- Original Message ----------------------------
Subject: Why3 AST (abstract syntax tree) generator
From:    mtkhan at risc.uni-linz.ac.at
Date:    Fri, September 14, 2012 11:54 am
To:      why3-club at lists.gforge.inria.fr
--------------------------------------------------------------------------

Hi All,

I need to translate into a AST for Why3. Is there some AST component of
Why3 available which can be integrated with Java?

Anticipated thanks.

regards,
taimoor





More information about the Why3-club mailing list