[Why3-club] [Q612-030] adapt SPARK to Why3 1.0.0
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...
More information about the Why3-club