team-worthwhile/worthwhile — Issue #106: Function call substitution does not always need to create quantified expressions
Author: jspam
Created: 2012-02-27 21:00:18+00:00
State: open
Labels: feature, prover

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 :)