Guided Practice 7.2 (Solution)

A valid invariant for a function has the following property:

If the function is called with an argument that satisfies the invariant, then each recursive call of that function satisfies the invariant.

We say that the function preserves the invariant.

Consider the following function definition:

;; f : Integer -> Integer
;; GIVEN/RETURNS: omitted
;; INVARIANT: to be filled in
(define (f n)
  (cond
    [(zero? n) 1]
    [else (* 2 (f (- n 3)))]))

Which of the following possible invariants does this function preserve?

1. n is a non-negative integer. ANSWER: No. If n is 1 or 2, then n-3 is not a non-negative integer.
2. n is of the form 3k for some non-negative integer k. ANSWER: Yes. If k = 0, then the function does not make any recursive calls. If k is greater than 0, then 3k-3 is still a non-negative multiple of 3.
3. n is of the form 3k+1 for some non-negative integer k. ANSWER: No. If k is 0, then n = 1, so the function makes the recursive call, and n-3 is not of the form 3k+1 for any non-negative k.

[Solution]

---

Last modified: Mon Nov 13 20:00:12 Eastern Standard Time 2017