Prove the Squaring Program
l
Using assertion-based reasoning
(Òloop invariantÓ)
for PC.
l
Use Òenergy functionÓ or ÒvariantÓ
for termination.
