Energy Function Principle
for Proving Termination
for Proving Termination
lAn energy function
(also called a ÒvariantÓ) is a function that
one fabricates:
f:States ¨ Natural Numbers
(therefore always non-negative)
lIf the same point in the program is visited with state s1 after state s2, then necessarily:
f(s2) < f(s1)
f:States ¨ Natural Numbers
(therefore always non-negative)
lIf the same point in the program is visited with state s1 after state s2, then necessarily:
f(s2) < f(s1)