[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