[Why3-club] why3ml output

Frédéric Besson frederic.besson at inria.fr
Mon Feb 6 12:05:52 CET 2012


On 6 févr. 2012, at 10:48, Jean-Christophe Filliatre wrote:

> 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?
I would like to compute "abstract" weakest preconditions parametrized by abstract pre/post.
Then, I think I could emulate the notion of behaviors by cloning -- maybe I am wrong...
A variant of this, would be to prove a proof principle for the program and have several instances.
Again, this would allow to structure the proof and maybe make it more tractable for provers.



> 
> -- 
> Jean-Christophe
> 
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20120206/3de4fe8a/attachment.htm>


More information about the Why3-club mailing list