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

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Fri Sep 14 12:53:17 CEST 2012


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

Not that I know.

Actually, I doubt there are many integrations of OCaml APIs with Java 
(though this is technically possible).

I would strongly advise that you simply use intermediate text files i.e. 
that you write a Why3 pretty-printer in Java.

Hope this helps,

More information about the Why3-club mailing list