[Why3-club] inlining functions or explicit predicates

Jean-Jacques Levy jean-jacques.levy at inria.fr
Tue Feb 19 16:02:24 CET 2019


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é <Claude.Marche at inria.fr> a écrit :
> 
> 
> 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 way as you would instantiate the functor Set.Make in OCaml.
> 
> Longer answer, of the previous mail too, should come soon...
> 
> - Claude
> 
> Le 19/02/2019 à 15:33, Jean-Jacques Levy a écrit :
>> 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 components, we could still use ‘Fset’ functions in regular code on non ghost values… Correct ? Is this too simple minded ?
>> Cheers, -JJ-
>> _______________________________________________
>> 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

_______________________________________________
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