[Why3-club] WhyML questions: function without body? polymorphic Sum?

Guillaume Melquiond guillaume.melquiond at inria.fr
Tue Nov 27 17:44:58 CET 2012


Le mardi 27 novembre 2012 à 17:17 +0100, David MENTRE a écrit :

> On above code, I have two questions:
> 
>  1. Is it possible to specify behaviour of "get_cont_value" without
> giving its body (i.e. only ensures, requires, ...)? I am currently at
> the specification phase and I am not interested in function bodies
> (and their correctness).

Sure, just stops before "=" and change "let" into "val".

>   2. When defining "type container", is there a way to use a
> polymorphic "continuous_profile_and_location_data", i.e.
> "continuous_profile_and_location_data 'a"? Right now, I am forced to
> precise the type 'a to int (as container in sum.Sum is not
> polymorphic) and thus my function "sum_from_LRBG_before_n" only works
> with "profile" of type "continuous_profile_and_location_data int". My
> objective is to get a sum.Sum function that sums
> "(continuous_profile_and_location_data 'a)[i].cont_distance" elements.

I don't think it is possible currently. I can't see any kind of issue
that would be caused by allowing it, so it might just have been some
shortsightedness when it was implemented; I will let others comment.

Best regards,

Guillaume




More information about the Why3-club mailing list