Program inversion: More than fun!

AbstractWe introduce proof rules for inverting a program. We derive an algorithm to compute the preorder and inorder traversals of a binary tree. Subsequently, we invert this algorithm to arrive at an algorithm to construct a tree from its preorder and inorder traversals. We prove this program correct using the proof rules for inversion rather than directly. Since a proper formulation of a provable invariant of this program appears to be quite awkward, this example reinforces the view that program inversion is a useful technique and more than fun