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

Andrei Paskevich andrei.paskevich at lri.fr
Wed Jul 25 21:51:14 CEST 2018


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.

> (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 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.

> >> 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.

À+,
Andrei


More information about the Why3-club mailing list