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

David MENTRE dmentre at linux-france.org
Tue Nov 27 17:17:27 CET 2012

```Hello,

I have following WhyML module (Why3 0.80):
"""
module Section_3_6_3_2
use import int.Int
use import array.Array

(* §3.6.3.2.1 *)
type cont_entry 'a = { cont_distance : int;
cont_value : 'a }
type continuous_profile_and_location_data 'a = array (cont_entry 'a)

(* WARNING: non continuous profile data not formalized *)

(* §3.6.3.2.2 *)
type container = continuous_profile_and_location_data int
function f (c : container) (i : int) : int = c[i].cont_distance
clone sum.Sum with type container = container, function f = f

function sum_from_LRBG_before_n
(profile : continuous_profile_and_location_data int)
(n : int) : int =
Sum.sum profile 0 n

predicate valid_continuous_profile
(profile : continuous_profile_and_location_data 'a) =
length profile >= 1
(* c) *)
/\ (forall i:int. 0 <= i < length profile
-> profile[i].cont_distance >= 0)
(* c) *)
/\ (forall i:int. 0 <= i < (length profile - 1)
-> profile[i].cont_distance <= profile[i+1].cont_distance)

let get_cont_value (profile : continuous_profile_and_location_data 'a)
(distance : int) (previous_data : 'a) : 'a
requires { valid_continuous_profile profile }
ensures
{ (* a) *)
(forall i:int. 0 <= i < length profile
-> (result = profile[i].cont_value <->
profile[i].cont_distance < distance <= profile[i+1].cont_distance))
(* b) *)
/\ distance <= profile.cont_distance <-> result = previous_data
(* d *)
/\ distance > profile[length profile - 1].cont_distance <->
result = profile[length profile - 1].cont_value } =
profile.cont_value
end
"""

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

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.

Best regards,
david

```

More information about the Why3-club mailing list