[Why3-club] fighting with non polymorphic equality

Andrei Paskevich andrei.paskevich at lri.fr
Tue Feb 26 17:40:50 CET 2019


Dear Jean-Jacques,

On Tue, 26 Feb 2019 at 13:50, Jean-Jacques Levy <jean-jacques.levy at inria.fr>
wrote:

> Dear Friends,
>
> in Why3.1.2.0, it looks that functions got an implicit ‘ghost' tag :
>

Logical functions are not assumed to be exectuable and therefore have to
stay in the ghost part of the code (and in the annotations, of course). To
have a pure executable function accessible both in the non-ghost code and
in annotations, you should either define it with "let function" or declare
it with "val function", with the same syntax for contracts and definitions
as in usual "let" or "val".


> ------------------------------------
> 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! :-(
>

You do not have to write an explicit postcondition : if the function body
is pure, Why3 should be able to deduce the post-condition all by itself.
Does your proof break if you write "let function infty () : int = 10000"?


> Correct? I also do not understand the ‘let function’ definition.. same as
> ‘function’ ??
>

"let" means "this program function is executable, but I do not care about
using it as a logical function in the annotations".
"let function" means "this program function is pure and state-independent,
and I want to be able to use it both in the code and in the annotations".
"function" means "this logical function is to be used in the annotations
and, if need be, in ghost code, but it may have no executable semantics,
and therefore is not usable in non-ghost code".


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

You can declare a dedicated equality for your abstract type "vertex":

  val (=) (x y: vertex) : bool ensures { result <-> x = y }

just as it is done for integers. Polymorphic logical equality can be
unsound when used in the non-ghost code, and therefore equality operators
need to be defined/declared by the user separately for each type.

Best,
Andrei
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20190226/ed2685a1/attachment-0001.html>


More information about the Why3-club mailing list