Potential Function Basics

The basic idea is that we define a function $\Phi(D)$ over the space of program states that measures the amount of ``work'' left to be squeezed out (potential energy). Properties:

• $\Phi(D)\ge 0$

We'll think of the program as performing a series of k operations starting on the initial state $D_0, D_1, D_2, \ldots, D_k$.