[Why3-club] inlining functions or explicit predicates

Jean-Jacques Levy jean-jacques.levy at inria.fr
Fri Feb 15 21:51:25 CET 2019


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> 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
>> 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

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20190215/266a2742/attachment.html>


More information about the Why3-club mailing list