[Why3-club] inlining functions or explicit predicates

Julia Lawall julia.lawall at lip6.fr
Mon Feb 18 13:56:02 CET 2019



On Mon, 18 Feb 2019, Jean-Jacques Levy wrote:

> Dear Jean-Christophe and Friends,
> thanks for your answer. So you avoid inconsistent use of equality for records with ghost fields by preventing its usage in regular code. (I have still to understand the meaning of the ‘pure’ attribute). But in my case, ‘set_1000' was
> used in regular code, with mappings on an abstract type, which I thnk you do not like too !! (since that abstract type could be a record with ghost fields).
>
> Therefore :
>
> 1- I should use mappings on concrete scalar types (int, bool) [btw I have also a strange error - see below with bool]
>
> 2- I cannot use the ’set’ function of the mappings library when my ‘set_1000’ is used in regular code :-( !
>
> Cheers, -JJ-
>
> ps/ similar problem with equality in why3.1.2.0 ?
> --------------------------------
> module BBB
>
>   use int.Int
>   use list.List
>
> type abc = bool
>
> let rec split (x : abc) (s: list abc) : (list abc, list abc) =
> variant {s}
>   match s with
>   | Nil -> (Nil, Nil)
>   | Cons y s' -> if x = y then (Cons x Nil, s') else 
>        let (s1', s2) = split x s' in
>         ((Cons y s1'), s2) 
>   end
>
> end
> --------------------------------
> hos $ why3 execute bbb.mlw 
> File "bbb.mlw", line 12, characters 20-21:
> This expression has type bool, but is expected to have type int

In code, = is only defined on int.  So you would need:

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

julia


> --------------------------------
>
>       Le 18 févr. 2019 à 08:21, Jean-Christophe Filliatre <Jean-Christophe.Filliatre at lri.fr> a écrit :
>
> Dear Jean-Jacques,
>
> You are making use of a ghost function to define set_1000, namely
> function ([<-]) from library map.Map. Consequently, your function
> set_1000 must be declared ghost. You can do this by inserting the
> "ghost" keyword immediately after "let rec":
>
>  let rec ghost set_1000 (s : list 'a)(f : map 'a int) : map 'a int =
>    ...
>
> Now why3 is going to complain that you must prove termination of
> function set_1000, as ghost code must terminate. Here, this is easy, as
> parameter "s" decreases:
>
>  let rec ghost set_1000 (s : list 'a)(f : map 'a int) : map 'a int =
>    variant { s }
>    ...
>
> The definition is now accepted.
>
> You may wonder why function ([<-]) was declared ghost in the first
> place. This is because polymorphic equality is hidden behind this
> function. Function ([<-]) is actually syntactic sugar for this function
>
>  let ghost function set (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b =
>    fun y -> if pure {y = x} then v else f y
>
> where you can see that polymorphic equality is used to compare y and x.
> Since we don't know how to provide a polymorphic equality in programs
> (think of the comparison of records with possible ghost fields that
> would be erased at runtime), we have no other choice than forbidding its
> use in regular (i.e. non-ghost) code.
>
> As for your question "where to insert the ghost keyword", you can find
> the answer on page 87 in the PDF manual, Fig. 6.5.
> http://why3.lri.fr/manual.pdf
>
> Cheers
> --
> Jean-Christophe
>
> On 2/15/19 9:51 PM, Jean-Jacques Levy wrote:
>       Dear Claude,
>
>       thanks for your answer. So I upgraded (with opam) why3 to release 1.1.1.
>       (couldn’t find opam upgrade to 1.2.0!)
>
>       Now I’m facing a new problem with strange ‘ghost’ error.
>       -----------------
>       module AAA
>
>         use list.List
>         use map.Map
>
>       let rec set_1000 (s : list 'a)(f : map 'a int) =
>         match s with
>         | Nil -> f
>         | Cons x s' -> (set_1000 s' f)[x <- 1000] 
>         end  
>
>       end
>       -----------------
>       why3 execute aaa.mlw    
>       File "aaa.mlw", line 6, characters 8-16:
>       Function set_1000 must be explicitly marked ghost
>       -----------------
>       So why that message + where to insert the ghost keyword (couldn’t find!) ??
>
>       Cheers, -JJ-
>
>             Le 15 févr. 2019 à 17:08, Claude Marche <Claude.Marche at inria.fr
>             <mailto:Claude.Marche at inria.fr>> a écrit :
>
>
>             Dear JJ,
>
>             As you remark, Why3 0.88 is now quite outdated and my answer may not
>             be very accurate. As far as I remember, the former "Inline" button was
>             applying the transformation "inline_goal" which has the effect of
>             inlining the defined function symbols appearing in an outermost
>             position in the goal.
>
>             The doc for the transformations are obtained when typing `why3
>             --list-transforms', and some of them are documented in a bit more
>             details in the manual : "inline_*" are documented at the beginning of
>             http://why3.lri.fr/doc/technical.html#sec128
>
>             In Why3 1.x, the user interface for applying transformations is much
>             more powerful, in your case you would probably want to type "unfold
>             foo" where "foo" is your function symbol. The documentation is also
>             visible interactively.
>
>             I don't know how to help more without seeing the exact example you have.
>
>             - Claude
>
>
>
>             Le 14/02/2019 à 16:20, Jean-Jacques Levy a écrit :
>                   Dear Why3 Friends,
>                   is there any doc about the functionality of the  "Inline"  button in
>                   the Why3 IDE ?
>                   Same for inline_all, inline_goal, inline_trivial..
>                   My current problem is that the inlined version of a trivial function
>                   works with automatic provers, but I cannot find a way of forcing that
>                   inlining.
>                   Many many thanks for you help!
>                   -JJ-
>                   ps/ I’m using old release 0.88.3 :-(
>                   _______________________________________________
>                   Why3-club mailing list
>                   Why3-club at lists.gforge.inria.fr <mailto:Why3-club at lists.gforge.inria.fr>
>                   https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
>             _______________________________________________
>             Why3-club mailing list
>             Why3-club at lists.gforge.inria.fr <mailto:Why3-club at lists.gforge.inria.fr>
>             https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
>
>
>       _______________________________________________
>       Why3-club mailing list
>       Why3-club at lists.gforge.inria.fr
>       https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
>
>
>
-------------- next part --------------
_______________________________________________
Why3-club mailing list
Why3-club at lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club


More information about the Why3-club mailing list