[Why3-club] [Q612-030] adapt SPARK to Why3 1.0.0
dross at adacore.com
Thu Jul 26 09:09:07 CEST 2018
Thanks Andrei for your answers.
Le 25/07/2018 à 21:51, Andrei Paskevich a écrit :
> On 25 July 2018 at 17:31, Claire Dross <dross at adacore.com> wrote:
>> I have been trying to adapt the spark tool to use the new Why3 release. I cannot say how it is going yet, I still have a long way to go, but I already have some questions:
>> - the "no inlining" and "lskept" metas seem to have disappear, did they changed names or are they completely removed?
> No, the polymorphism encoding didn't change at all, so everything
> should still be there, see François' reply.
>> - labels "..." are not accepted anymore. By looking at the parser, I have replaced them with [@...], is this correct?
OK, multiline labels are no longer supported then. On purpose?
>> (BTW, I am really missing the Language Reference section of the LRM, any chance there is a draft I can use somewhere?)
> I'm working on that, albeit slowly. Apart from the Appendix François
> mentioned, you can see the text under construction in
I will look at it, thanks.
>> I also found 2 cases of constructs which were accepted before but are not anymore:
>> - We can no longer ignore a non unit value:
>> let main () = 15; ()
> This is on purpose, OCaml does that same. "let _ = 15 in ()" should work.
Yes it does, but it will require special casing in the code generator...
>>>> Cannot cast an integer literal to type unit
>> - Conversion to int of range types is ghost:
>> type tt = < range 1 5 >
>> let function to_rep (x : tt) : int = (tt'int x)
>>>> Function to_rep must be explicitly marked ghost
> This is also on purpose: the tt'int operation is used for
> specification purposes, if you make it non-ghost, you would need to
> link the extracted code with an arbitrary-precision arithmetic
Then I think we are back to not using range types and defining our own
projections. I will see if we can avoid that.
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
Thanks again for your answers,
More information about the Why3-club