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



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


More information about the Why3-club mailing list