[Why3-club] why3ml output
Jean-Christophe.Filliatre at lri.fr
Mon Feb 6 10:48:26 CET 2012
> 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