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

Claire Dross 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?
> Yes.

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
> doc/syntaxref.tex

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
> library.
>
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 
intermediate language...

Thanks again for your answers,

-- 
Claire



More information about the Why3-club mailing list