[Why3-club] Building Why3 programs with the Why3 API (other examples ?)

Denis Cousineau D.Cousineau at fr.merce.mee.com
Tue Oct 25 16:16:17 CEST 2016


Dear Why3-mailing-list users,
I'm currently working on generating Why3 programs from another language.
For that purpose I use the Why3 API.
I saw the manual and the two example files it refers to.
And I was wondering if there exists some more complete examples than mlw.ml and mlw_tree.ml.
Thanks for any help,

Denis

---
Denis Cousineau, Ph.D - Researcher
Formal Methods: Theory, Methodology and Tools
Mitsubishi Electric R&D Centre Europe (MERCE)
Tel: +33 (0)2 23 45 58 36  Fax: +33 (0)2 23 45 58 59
http://www.fr.mitsubishielectric-rce.eu

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20161025/f37e3e7d/attachment.html>


More information about the Why3-club mailing list