CSE 127w02 TA: Greg Hamerly Solutions Goal: work through some loop invariants, preconditions, and postconditions. Problem 1: ---------- int max(int *arr, int nelt) { int k, indexMax; indexMax = 0; for(k = 0; k < nelt; k++) { // LOOP INVARIANTS HOLD HERE if (arr[k] > arr[indexMax]) indexMax = k; } return indexMax; } PRECONDITIONS: arr is an integer array of size nelt nelt > 0 POSTCONDITIONS: for all i: 0 <= i < nelt --> arr[indexMax] >= arr[i] LOOP INVARIANT: for all i: 0 <= i < k --> arr[indexMax] >= arr[i] Problem 2: ---------- int square(int n) { int i, sum; sum = 0; for (i = 0; i < n; i++) { //LOOP INVARIANTS HOLD HERE sum = sum + n; } return sum; } PRECONDITIONS: n >= 0 POSTCONDITIONS: sum = n * n LOOP INVARIANTS: 0 <= i < n sum = i * n Problem 3: ---------- int pow(int x, int y) { int i, p = 1; for (i = 0; i < y; i++) { // LOOP INVARIANTS HOLD HERE p = p * x; } return p; } PRECONDITIONS: x is any integer y >= 0 ! (y == 0 && x == 0) POSTCONDITIONS: p = x^y LOOP INVARIANTS: 0 <= i < y p = x^i Problem 4: ---------- int factorial(int n) { int i, F = 1; for (i = 1; i <= n; i++) { // LOOP INVARIANTS HOLD HERE F = F * i; } return F; } PRECONDITIONS: n >= 0 POSTCONDITIONS: F = n! LOOP INVARIANTS: 1 <= i <= n F = (i-1)!