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

Jean-Christophe Filliâtre 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.

-- 
Jean-Christophe



More information about the Why3-club mailing list