[Why3-club] inlining functions or explicit predicates

Jean-Jacques Levy jean-jacques.levy at inria.fr
Tue Feb 19 15:58:40 CET 2019


Dear Claude,

thanks for your answer. I think that my problem is more with ghost values than with imperative features.

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



More information about the Why3-club mailing list