Hw07: program proofs; proof methods

Before you tackle the homework, remind yourself of our general hw policies.

(The 4ed. page-numberings will be added mar.01(sat) eve.

• (2pts) Section 1.5, #26. (p. 75; 4ed p.184 #22)
• (2pts) Section 1.5, #28. (p. 75; 4ed p.184 #28)
• (2pts) Section 1.5, #64. (p. 76; 4ed p.185 #62)
• (2pts) Section 2.5, #2. (p. 179; 4ed p.135 #6 )
• (2pts) Convert the following binary numerals into numbers (written in conventional base-10 numerals). Observe how each numeral relates to the one before it.
  1. [ 1101 ]₂
  2. [ 11010 ]₂
  3. [ 110101 ]₂
• (1pt) Section 2.5, #10. (p. 180; 4ed does-not-exist, but similar to p.135 #12: convert [ 1 1000 0110 0011 ]₂ to hexadecimal.)
• (5pts) Section 3.7, #12. (as deferred from last week) Be sure to express the loop invariant, and the four parts of the proof obligation as mentioned in lecture:
  1. the loop invariant holds when the loop is first reached.
  2. the loop invariant is maintained through the loop
  3. the loop invariant, with the loop-condition being false, imply the goal as stated in rosen)
  4. The loop condition will eventually become false.
  (If you did this problem for hw06, you can give an answer as in Rosen. Your points will be included on that hw.)
• (4pts) Prove that the following algorithm computes xn:

  ;; pow: real, natnum --> real
  ;; Return xn.
  ;;
  (define (pow x n)
    (cond [(zero? n) 1]
          [(even? n)      (sqr (pow x (quotient n 2)))]
          [(odd?  n) (* x (sqr (pow x (quotient n 2))))]
  

  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^18, you don't need to do 18 multiplications, but rather just compute (504^9)^2. In turn, 504^9 can be computed by observing 504^9 = 504^8*504 = (504^4)^2*504.

• (5pts) Consider an iterative program which uses roughly the same idea as above, but in a bottom-up way:

  // pow: compute xn.
  //
  rational pow( rational x, natnum n) {
    rational soFar     <-- 1
    natnum   restOfN   <-- n    
    rational xToTwoToI <-- x    // This will be x^(2^i), where i is number of times through loop.
  
    // LoopInvariant: x^n = (xToTwoToI ^ restOfN) * soFar.
    while (restOfN > 0) {
      if odd?(restOfN)  soFar <-- soFar * xToTwoToI
      restOfN   <-- quotient(restOfN, 2)
      xToTwoToI <-- xToTwoToI * xToTwoToI   // Repeatedly square.
      }
  
    return soFar
    }
  

  Using the loop invariant as stated in the code, show the four parts of the proof obligation for the loop.

  (You can assume that your programming language is sane, and that rationals and natnums are represented exactly without round-off or overflow error.)