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)