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

Claire Dross dross at adacore.com
Thu Jul 26 09:48:52 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.

I don't see his reply, were is it? On Why3 list?

>>>>    - 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?
> No, there is no hard reason for that AFAIK. Can be added back. What is
> your use case for multiline labels?

They are for information to be printed back for manual proof I think.

>>>> 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...
> Why so? There is no dedicated sequence constructor anyway, sequences
> are just "let-in" chains.
> And even if you need a special case for that, it does not seem like a
> complicated one.

Not so complicated. We have to check for the type of the expression when 
printing a sequence, and I am forseeing troubles with cases where the 
expression does not have a type. To be seen. What is sure, is that this 
check does not bring us anything.

>>>>>> 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.
> I fail to see your logic here. The range types in WhyML were, in large
> part, motivated by Spark use. As I've said earlier, it is easy to add
> non-ghost range-to-int converter. What is the problem?

No problem, just yet another special case where we cannot use the same 
function for the conversion when the conversion is done in the logic or 
in the program domain. And yet again, for a check which does not bring 
anything for us.

>> 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 would be unfortunate indeed, and very far from our intention.
> However, I do not understand why you think it is the case. The
> questions you've raised so far do not seem to require complicated
> changes in the code generator.
The code generator is very complicated in itself, and every special case 
making it more so is a concern. But indeed, these are minor problems. 
Maybe I am pessimistic, but I expect to encounter more of them, due to 
this distinction between ghost and non-ghost code, and these features 
for code extraction. They are yet another set of constraints that we 
need to cope with for no gain, and I am concerned that it will make 
things more complicated.
More serious problems I am expecting involve in particular equality. 
Even if we don't provide logical equality at the level of SPARK, I am 
pretty sure we use it at the level of Why3 and working around not having 
it will be a pain, that's for sure...


More information about the Why3-club mailing list