CSci 420/520: Homework 2

Proofs of Programs

Due Wednesday, September 14th by 1pm.

Summary

In this assignment you will apply Hoare's axiomatic semantics to prove the correctness of a small program.

Assignment

Let a and b be arrays (indexed from 0 to n-1) of integers.

Prove that the algorithm:

c = 0;
while( c<n ) {
  b[c] = a[c];
  c=c+1;
}

Meets the postcondition of:

∀i ∈ {0, 1, ..., n-1} | b[i] = a[i]

given the precondition of:

n≥0

Provide your answer in proof outline format, providing all conditions, and justifications for how you derived each condition. You must also prove any verification conditions as well. You may also want to provide some expository prose to help the grader understand why you wrote particular conditions.

Hints:

• At one point in the proof you will need to deal with b[c] = a[c] over some values of c. It won't be a simple application of the assignment axiom, and you'll have to make an argument why your work is correct.
• Use my office hours if you need more hints.

Grading

100 points total.

Turn in your assignment at the start of class.