Pre-update / post-update

[Calvin-L]

The query synthesizer should have visibility into whether it is performing its work before or after a change has been made to its underlying state.

Currently Cozy performs state maintenance for an update method by (1) inserting a hardcoded snippet and (2) generating some subgoals for the query synthesizer to optimize. These subgoals are always in terms of the original abstract state of the data structure---before the update has taken place. However, sometimes it is useful to perform the update afterwards. Consider this state:

theMin = min xs

and this update:

xs.remove(x)

We might desire an implementation such as:

heap.remove(x)
theMin = heap.peek()

However, Cozy cannot discover this, since the synthesizer will always see the original heap, before the removal has taken place.