[Why3-club] predicates

Andrei Paskevich andrei.paskevich at lri.fr
Mon Mar 25 09:41:40 CET 2019


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.

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20190325/6b8826e1/attachment.html>


More information about the Why3-club mailing list