Thanks David for sharing your experience.
I don't know what is the overall goal of Gian Pietro, but there's a good
chance that producing a text file would be a good approach.
- Claude
Le 08/05/2018 à 22:21, David MENTRÉ a écrit :
Hello,
Le 2018-05-08 à 18:58, Gian Pietro Farina a écrit :
Sorry for bothering, I am still having troubles in building tasks with
formulas including expressions of the array theory.
My own recommendation would be to avoid Wy3 API to build formulas, but
to use text file instead. It is much more simpler to produce a text file
with Why3 content in it and then just load it and apply provers using
the API (file examples/use_api/creation_session.ml is a good start for
that). In case of error in the text file, you'll get regular syntax and
type checking errors. And you can use your usual editor to try to fix
the error before fixing it in your program.
At work we have used extensively the API to build Why3 programs for
months and producing a Why3 program in text format is simply the easiest
approach. AdaCore people are also using this approach for GNATprove.
Best regards,
D. Mentré
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
