[Why3-club] fighting with non polymorphic equality

Jean-Jacques Levy jean-jacques.levy at inria.fr
Tue Feb 26 13:50:00 CET 2019


Dear Friends,

in Why3.1.2.0, it looks that functions got an implicit ‘ghost' tag :
------------------------------------
module DDD
  use int.Int
  use list.List
  use map.Map

type vertex = int
function infty (): int = 1000

let function myset (f: map vertex int) (x: vertex) (v: int) : map vertex int =
    fun y -> if y = x then v else f y

let function ([<-]) f x v = myset f x v

let rec set_infty (s : list vertex)(f : map vertex int) =
variant {s}
  match s with
  | Nil -> f
  | Cons x s' -> (set_infty s' f) [x <- infty()]
  end

end
------------------------------------
File "ddd.mlw", line 37, characters 40-45:
Logical symbol infty is used in a non-ghost context
------------------------------------
whereas it’s fine with ‘function infty' changed into ‘let infty’ . This implies extra post-conditions on new auxiliary functions! :-(
Correct? I also do not understand the ‘let function’ definition.. same as ‘function’ ??

For the sake of equality, I also needed to define the abstract type ‘vertex' as integer :-( !

Cheers, -JJ-



More information about the Why3-club mailing list