Homework 8: Program Correctness

Due 05.Mar.29 (Tue)

Before you tackle the homework, remind yourself of our general hw policies (now includes proof-by-induction tips). In particular, you don't need to show your work when only a short answer is required (though doing so might garner more partial credit if the answer is wrong).

Reading: Rosen 3.6, plus some helpful common hw errors from previous years.

1. (2pts) Convert the following binary numerals into numbers (express your answers using conventional base-10 numerals). Observe how each numeral relates to the one before it.
   1. [ 1101 ]₂
   2. [ 11010 ]₂
   3. [ 110101 ]₂
2. (1pt) Section 2.5, #6 (p. 179): hex→bin([BADFACED]₁₆)
   (Cf. Rosen's Example 6.)
3. (8pts extra-credit) Section 2.5, #12 (p. 180): hex→bin.
   
   • (1pt) Write code for the numeral-translation function hex→bin, complete with data description, contract, and test cases which it passes. (You can use either java or scheme.)
   • As the problem describes, your function should convert directly between numerals, without calculating the represented number. It's fine to have leading zeros in your resulting numeral.
   • (1pt) How would you capture the notion that the function hex->bin is correct? (You may abbreviate ``hex→bin'' as ``h2b''.)
   • (4pts) Prove your hex->bin is correct.
     Clearly state what form of proof you use.
   • Of course, you'll need a helper function hexdig→bits to translate individual hex digits. (Abbreviation: ``hd2bs''.)
   • Note that your proof is reasoning about program statements. It accomplishes this with two sorts of steps: those steps which translate between program domain and math domain, and those steps which reason entirely within the math domain (where we can talk about sets, functions, arithemetic, etc.).
     Being aware of which domain you're working in at any given step is crucial to being able to write the proof.
   • Compared to Rosen's answer for #11, your answer should clearly distinguish between numerals and numbers, and not be riddled with ``…''s (since his explanation comes before he's discussed induction).
   • (2pts) Write a function to convert from any hex numeral to a binary numeral w/o excess leading 0s. Prove that this new function is also correct (in the sense that it doesn't return a numeral with a different meaning).
4. (5pts) (Repeated squaring, functional)
   Prove that the following program¹ computes xn
   (where 0⁰ is taken to be 1; a better answer would be +NaN.0, but that just adds an odd corner-case to the proof and code, so we omit it for simplicity).

   ;; pow: real, natnum → real
   ;; Return xn  (where we interpret 00 as 1).
   ;; 
   (define (pow x n) (pow-help x n 1))
   
   ;; pow-help: real, natNum, real → real
   ;; Return xn ⋅ soFar  (where we interpret 00 as 1).
   ;;
   (define (pow-help x n soFar)
     (cond [(zero? n) soFar]
           [(odd?  n) (pow-help (sqr x) (quotient n 2) (* soFar x))]
           [(even? n) (pow-help (sqr x) (quotient n 2) soFar)]))
   

   Be sure to clearly state which proof method you are using.

   sqr is a function which squares its input. You may take as given, that (quotient n 2) returns n/2 if n even, and (n-1)/2 if n odd.

   The above procedure is called ``repeated squaring'', and is based on the fact that to compute (for example) 504²², you don't need to do 22 multiplications, but rather just compute 504¹, 504², 504⁴, 504⁸, and 504¹⁶, and then return 504¹⁶⋅504⁴⋅504². (Work through a couple of test cases, so that you internalize your understanding of why the algorithm works.)

   In a following problem, we visit an iterative version of this same algorithm.

5. (5pts) Section 3.6, #12 (p. 290): computing remainder,quotient.
   Be sure to clearly state your loop invariant, and show the four parts of the proof obligation as mentioned in lecture.
   Some remarks on how reading relates to lectures.

6. (6pts) (Repeated squaring via side-effects)
   Here is an iterative program for repeated-squaring. (It is the direct translation² of the accumulator-style program above.)

   // pow: return xn,
   // where x is any number, n ≥ 0, 
   // and if x=0,n=0 we return 1
   // even though NaN would be the mathematically correct answer.
   //
   real pow( real x_orig, natnum n_orig ) {
     real   soFar ← 1
     natnum n     ← n_orig;    
     real   x     ← x_orig;    // This will be x_orig(2i), where i is number of times through loop.
   
     // LoopInvariant: …?
     while (n > 0) {
       if odd?(n)   soFar ← soFar * x
       n ← quotient(n, 2)
       x ← sqr(x)              // Repeatedly square.
       }
   
     return soFar
     }
   

   Prove this loop correct, using the 4-part proof obligation as in the notes. Your loop invariant will be similar to pow-help's contract, relating x,n,soFar to x_orig,n_orig. (You'll need to include one smidgen more of info in your invariant, to get your proof to go through).

   You can assume that your programming language is high-level enough to do arithmetic at the fourth-grade level (add and multiply reals without round-off or overflow error). As last time, be sure to get a feel for what the algorithm is doing, presumably by working through some test cases.

;; pow: real, natnum → real
;; Return x-orign-orig  (where we interpret 00 as 1).
;; 
(define (pow x-orig n-orig)
  (let looper {[x     x-orig]
               [n     n-orig] 
               [soFar 1]
               }
    (cond [(zero? n) soFar]
          [(odd?  n) (looper (sqr x) (quotient n 2) (* soFar x))]
          [(even? n) (looper (sqr x) (quotient n 2) soFar)])))

;; pow: real, natnum → real
;; Return xn  (where we interpret 00 as 1).
;; 
(define (pow x n)
  (let loop {[x x] [n n] [soFar 1]}
    (cond [(zero? n) soFar]
          [else (loop (sqr x) (quotient n 2) (* soFar (if (odd? n) x 1)))])))