Function call substitution does not always need to create quantified expressions

[jspam]

This is a nice-to-have feature with very low priority.

Take the following example program:

function Integer double(Integer i)
    _ensures _return = 2 ⋅ i
{
    return 2 ⋅ i
}

_assert double(2) = 4

It validates correctly, but the formula for the assertion seems overly complicated to me:

∀ Integer _double0 : _double0 = 2 ∙ 2 ⇒ _double0 = 4

In this special case, the prover could directly substitute double(2) with the return value from the postcondition, so that the formula would become:

2 ∙ 2 = 4

In a more general way, the prover could substitute the function call with the ensured return value when

• the function contains only one postcondition
• the postcondition's expression is an Equal
• the Equal's left or right hand side is a ReturnValueReference
• the other side of the Equal does not contain a ReturnValueReference

This is especially helpful when dealing with utility functions as in heap.ww. I think this could be a nice thing to show off :)