Example
lConstruct, and prove correct, a program that squares a number using only addition.

lThis technique goes back to BabbageÕs
ÒDifference EngineÓ, 1832.