"Folding" expressions

[viper-admin]

Created by @fpoli on 2018-08-15 15:29
Last updated on 2018-08-15 15:35

Why there is no folding ... in ... expression?

• It's the dual of unfolding, which exists;
• With folding it would be always possible to massage an old state to obtain the wanted predicates, which may be handy for Viper frontends;
• Syntax highlighting shows it as a keyword.

[viper-admin]

@alexanderjsummers commented on 2018-08-15 15:31

I would be open to having such a feature.

Just quickly w.r.t. your third point, it was a keyword used in the old support for magic wands. That's outdated now.

[viper-admin]

@fpoli on 2018-08-15 15:35:

• edited the description

[alexanderjsummers]

A minor wrinkle, but only added here for the sake of completeness of the discussion:

Right now, under certain slightly fiddly conditions, one can syntactically check that a heap-dependent function only recurses under at least one unfolding expression and (provided that there are no quantified permissions involved, which give a different source of unboundedness; one also has to take care of permission amounts / fractions in general), know for sure that the function terminates. However, this is mostly old thinking (e.g. how some things worked in Chalice, if I recall correctly); now we have the termination plugin this is a more robust approach to proving function termination when one wants it.