[Why3-club] [Fwd: Why3 AST (abstract syntax tree) generator]
Jean-Christophe.Filliatre at lri.fr
Fri Sep 14 21:13:15 CEST 2012
> Thanks for your recommendation; just wondering that if you
> already have a Why3 AST generator in Ocaml
We don't really have ``a Why3 AST generator in OCaml''. Instead, Why3
provides an OCaml API that allows you to build terms, formulas,
theories, and tasks (in a type-safe way).
Indeed you could make a Java layer on top of that API if you manage to
link this OCaml library into a Java program.
> then don't you
> think ocamljava.x9c.fr kind of integration is helpful.
I don't know that project.
More information about the Why3-club