[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[0].cont_distance <-> result = previous_data
          (* d *)
          /\ distance > profile[length profile - 1].cont_distance <->
               result = profile[length profile - 1].cont_value } =
     profile[0].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