[Why3-club] predicates

Julia Lawall julia.lawall at lip6.fr
Mon Mar 25 10:35:32 CET 2019

On Mon, 25 Mar 2019, Andrei Paskevich wrote:

> Hi Julia,
> would it help to label such predicates explicitly in order to always inline them when passing the task to a prover (as you suggested in an earlier mail)? I am inclined to add this functionality to the "inline_trivial" transformation.
> One downside of this is that the predicate is not inlined while you are in the interactive phase, so, for example, "split_goal" will not work on it, unless you call inline on it.

I would be completely happy to label the predicates with inline.  I know
up front that they only exist to collect information and reduce code size.
The split_goal limitation is not a problem.

Could this be done quickly, or would it have to wait for the next release?


> Best,
> Andrei
> On Mon, 25 Mar 2019 at 08:57, Julia Lawall <julia.lawall at lip6.fr> wrote:
>       My natural inclination is to make predicates that combine other
>       predicates, in order to avoid massive code duplication.  But it seems that
>       doing so makes it very hard for why3 to find the information it needs.  So
>       to get the proof to go through, I have to manually inline the predicates,
>       which clutters the code and is quite unsatisfying.
>       These predicates are not in the goal, but rather in the hypotheses, eg in
>       the ensures of a function I am calling.  Inline goal is thus of no use,
>       and Inline all inlines far too much, and seems to make it impossible to
>       get the proof to go through for other reasons.
>       Is there some intuition about when it is possible to define predicates
>       that wrap other predicates and when it is not?  Is there some level of
>       nesting that one should not exceed, or is there a distinction between
>       predicates defined in the current module or some other module?
>       I have tried meta rewrite_def predicate XXX but it doesn't seem to give
>       much benefit.
>       thanks,
>       julia
>       _______________________________________________
>       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