MIME-Version: 1.0 Server: CERN/3.0 Date: Sunday, 24-Nov-96 22:48:43 GMT Content-Type: text/html Content-Length: 9677 Last-Modified: Sunday, 22-Sep-96 21:08:03 GMT tt4

CS100

Lecture 4

CONCEPTS --- last lecture

types, user-defined functions, applicative-order substitution, recursion

CONCEPTS --- this lecture

specifications

READING

Teitelbaum, Section 2.10

Specifications

Software specifications

/* exp(x,n) == x^n, for n >= 0. */

int exp(int x, int n)

{

return (n == 0) ? 1 : exp(x, n-1) * x;

}

signature: a function taking two int's and returning an int

correctness specification: if n >= 0, then exp(x,n) will yield xn

Signatures


exp(5, 3, 1) is wrongexp("Hello", 1) is wrongprintf(exp(5, 1)) is wrong

Correctness Specifications

/* == x^n, for n >= 0. */

If the arguments in a function application satisfy the precondition, then the application will yield a value that satisfies the postcondition.
e.g., if n >= 0, then exp(x,n) will yield xn.

exp(5, -1)(-1 == 0) ? 1 : exp(5, -1 - 1) * 50 ? 1 : exp(5, -1 - 1) * 5exp(5, -1 - 1) * 5exp(5, -2) * 5((-2 == 0) ? 1 : exp(5, -2 - 1) * 5) * 5(0 ? 1 : exp(5, -2 - 1) * 5) * 5exp(5, -2 - 1) * 5 * 5exp(5, -3) * 5 * 5...

exp(5, 0)(0 == 0) ? 1 : exp(5, 0 - 1)1 ? 1 : exp(5, 0 - 1)1

Implementations

/* == x^4. */
int fourth(int x) { return (x * x * x * x); }

/* == x^4. */
int fourth(int x) { return (square(square(x))); }

/* == x^4. */
int fourth(int x) { return (exp(x, 4)); }

E.g., a minor flaw in
/* == x^n, for n >= 0. */
because xn is not defined for x = 0 and n = 0.

/* == x^n, for n >= 0, and x and n not both 0. */

or
/* == x^n, for n >= 0 and x != 0, and == 1, for n == 0 and x == 0. */

Counting
/* == id. */
int count(int lo, int hi, int id) {
return lo > hi ? id : count(lo + 1, hi, id);
}

For example
count(1, 2, 0)1 > 2 ? 0 : count(1 + 1, 2, 0)0 ? 0 : count(1 + 1, 2, 0)count(1 + 1, 2, 0)count(2, 2, 0)2 > 2 ? 0 : count(2 + 1, 2, 0)0 ? 0 : count(2 + 1, 2, 0)count(2 + 1, 2, 0)count(3, 2, 0)3 > 2 ? 0 : count(3 + 1, 2, 0)1 ? 0 : count(3 + 1, 2, 0)0

Sum of squares
/* == lo^2 + (lo+1)^2 + ... + hi^2. */
int sumSquares(int lo, int hi){
return lo > hi ? 0 : square(lo) + sumSquares(lo + 1, hi);
}

For example, sumSquares(1,2) -> 1*1+2*2 -> 5.

Factorial
/* == lo * (lo+1) *... * hi. */
int multIntegers(int lo, int hi){
return lo > hi ? 1 : lo * multIntegers(lo + 1, hi);
}

For example, multIntegers(1,4) -> 1*2*3*4 -> 24.

/* == n!, n >= 0. */
int factorial(int n) {
return multIntegers(1,n);
}