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