[Why3-club] predicates

Julia Lawall julia.lawall at lip6.fr
Mon Mar 25 08:57:01 CET 2019


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


More information about the Why3-club mailing list