Specification Examples
lA greatest-common-divisor program:
lInput assertion: x == x0, y == y0, x0 > 0, y0 > 0
lOutput assertion: x is the greatest common divisor of x0 and y0 [notated x == gcd(x0 , y0)].
Implicit here is that
all quantities are integers.
lValues x0 and y0 are not
program variables, but serve to anchor
the original values for later reference.