[Why3-club] why3ml output

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Mon Feb 6 10:48:26 CET 2012

Hi Frédéric,

> As JC explained this WE (great lecture!), modules do not (yet) accommodate for cloning -- but theories do.
> Thus, I am trying to run why3ml, generate the theory. Back in the theory world, I could clone again and so on.
> Perhaps, I am doing something wrong, but the theory  generated by why3ml does not seem to compile with why3.
> Is there an option to make it work ?
> (At first view, imports are commented out and there are missing parentheses...)

Indeed, they do not compile. Theories printed by Why3 are not intended 
to be re-parsed. We may consider doing it (we have already discussed 
this several times) but we don't see the need for it currently.

Regarding theories resulting from programs, you should be aware that 
they are purely logical theories that only contain goals for the weakest 
precondition of each program. Programs themselves do not appear anymore. 
So it is likely that it won't be that useful to clone them.

Do you have an example in mind?


More information about the Why3-club mailing list