[Why3-club] [Q612-030] adapt SPARK to Why3 1.0.0

Yannick Moy moy at adacore.com
Thu Jul 26 09:17:42 CEST 2018


-- Claire Dross (2018-07-26)
> Unfortunately, it seems that the modifications, if they make whyml better for code extraction, and probably a better language to program with directly, seem to make it more complicated to use as an intermediate language...


That's not desirable. If indeed Why3 as a source language benefits from different choices than Why3 as an intermediate language, I suggest the introduction of a "mode" to switch between these two ways to use Why3.
--
Yannick Moy, Senior Software Engineer, AdaCore




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


More information about the Why3-club mailing list