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.