SUNY Geneseo Department of Computer Science

Problem Set 2 -- Proof

CSci 240, Spring 2007

Prof. Doug Baldwin

Due Wednesday, January 24

Purpose

The purpose of this exercise is to reinforce your understanding of what it means to formally prove something in computer science.

Background

This exercise is based on the ideas in sections 3.1 through 3.5 of our text. This material is also discussed in our January 22 lecture.

Exercise

Solve each of the following problems.

Problem 1

Prove that the product of two even numbers is always a multiple of 4.

Problem 2

Prove that the following algorithm swaps the values of variables x and y:

    x = x + y
    y = x - y
    x = x - y

More formally, prove that, given the preconditions that x = x0, y = y0, x0 and y0 are both numbers, the algorithm establishes the postconditions that x = y0 and y = x0. (Note that much of what the preconditions are doing here is just introducing the names x0 and y0 for the initial values of x and y; such definition of terms used elsewhere in a specification is an occasional use for preconditions.)

Problem 3

Prove that "the parity (i.e., oddness or evenness) of x never changes" is a class invariant for the following class: 

    class Parity {
        private int x;
        public Parity( int initialX ) {
            x = initialX;
        }
        public increment() {
            x = x + 2;
        }
        public decrement() {
            x = x - 2;
        }
    }

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 answers to each of the problems to the meeting.