SUNY Geneseo Department of Computer Science

Problem Set 9 -- Proofs about Loops

CSci 240, Spring 2007

Prof. Doug Baldwin

Due Friday, March 2

Purpose

The goal of this exercise is to give you a basic ability to prove things about loop invariants and the correctness of loops.

Background

This problem set draws on material in chapter 8 of the textbook, particularly section 8.2. Section 8.2 was discussed in lecture on February 28, and loop invariants in general (section 8.1) on February 26.

Exercise

Do each of the following exercises, which involve proving loop invariants or loops' correctness.

  1. Exercise 8.13 on page 270 of our text
  2. Exercise 8.14 on pages 270 and 271 of our text
  3. Exercise 8.12 on page 270, except prove that the algorithm really returns true if n is a power of 2 and false otherwise. In other words, prove all aspects of the algorithm's correctness, not just the loop invariant.

Follow-Up

I will grade this exercise in a face-to-face meeting with you. Make an appointment to meet with me at some time convenient for you, as long as that time is before the end of the due date above. Meetings only need to be 15 minutes long. You can make an appointment by signing up on the copy of my schedule on the bulletin board outside my office. Please bring written solutions to each of the exercises to the meeting.