Le 19/02/2019 à 16:02, Jean-Jacques Levy a écrit :
Dear Claude,
(* me again *) I did not notice the appset module.. oh so thanks, I’ll try to
use it. But seems to be many sets:
Fset, appset, impset….
See http://why3.lri.fr/stdlib/
set.Set: theory of mathematical sets
set.Fset: theory
Dear Claude,
(* me again *) I did not notice the appset module.. oh so thanks, I’ll try to
use it. But seems to be many sets:
Fset, appset, impset….
Thanks, -JJ-
> Le 19 févr. 2019 à 15:50, Claude Marché a écrit :
>
>
> Hello JJ,
>
> Short answer: with Why3 1.x you should use one of the
Hello JJ,
Short answer: with Why3 1.x you should use one of the modules
appset.Appset or impset.Impset to program with finite sets (depending on
whether you want a mutable data structure or not). More precisely you
should clone one of these, giving the value of type 'elt', in a very
similar
Dear Jean-Christophe + Friends,
me again (* sorry *) .. a quick view about polymorphic equality:
Equality in logic should be distinct from Equality in regular code, where the
ghost attribute is prohibited. So if the problem with the ghost values is only
about aggregated data with ghost
Dear Jean-Christophe + Friends,
many many functions turned to be ghost functions in Why3.1.2.0. They can no
longer be used in regular code.. which means programs have to be rewritten with
effective implementations of many functions. Gosh !! where is abstraction ?
Why ‘add’, ‘remove’, ‘union’,
> 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).
Basically, the "pure" construct lifts a logic term (or predicate) to the
program
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).
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
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
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) =
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
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
12 matches
Mail list logo
