Guided Practice 7.2

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.
2. n is of the form 3k for some non-negative integer k.
3. n is of the form 3k+1 for some non-negative integer k.

[Solution]

---

Last modified: Mon Oct 2 12:33:29 Eastern Daylight Time 2017