Harvey Mudd College
Computer Science 60
Assignment 10, Due Thursday, November 18, by midnight

Proving Programs Correct

1. Transition Induction

(A) Given the following program, devise an appropriate loop invariant (for the point marked by /* */) and use it to show that the following function returns the cube of its argument, provided that the argument is non-negative. That is, you will need to prove two things: (1) that the loop invariant holds true before every loop test and (2) that for the precondition N >= 0, the postcondition x = N*N*N holds (and N hasn't changed).

Note on the loop invariant Your loop invariant (along with the loop test, i < N) should be a statement of the form

assert( 1+1 == 2 ) && i < N

static long cube(long N)
  {
  long i, x, y, z;
  x = 0;
  y = 1;
  z = 6;

  for( i = 0; /* assert(...) && */ i < N; i++ )
    {
    x = x + y;
    y = y + z;
    z = z + 6;
    }
  return x;
}

(B) Devise an appropriate energy function and use it to show that the program terminates for arguments N >= 0. What invariant do you need to show that your function really is an energy function?

(C) Once you have your invariant, include it as the argument to an assert predicate in the code which is included in the loop test as shown below and test its validity by running the code on various input values, say 0 to 25, checking that the invariant never fails:

assert(.... your invariant ....) && i < N

Here the definition of assert is:

static boolean assert(boolean PredicateValue)
  {
  if( PredicateValue )
    return true;

  System.err.println("*** assertion failed ***");
  System.exit(1);
  return false;
  }

Thus a true assertion will have no effect on the test which follows, while a false assertion will terminate the program immediately, printing a message.

You should submit your code in a file Cube.java. You may also submit your proof as a comment in that file, or on a separate page -- see the notes on submitting, below.

2. Structural Induction

t1 leaves = 3, nonleaves = 2
t2 leaves = 6, nonleaves = 5
t3 leaves = 9, nonleaves = 8
t4 leaves = 15, nonleaves = 14

• t.leaves() and t.nonleaves() return an integer value
• t.leaves() = t.nonleaves() + 1

// A Tree is either a leaf or a nonleaf,
// the latter consisting of two subTrees
//
// leaves() is supposed to count the number of leaves
// nonleaves() is supposed to count the nonleaves

abstract class Tree
{
abstract int leaves();
abstract int nonleaves();



// test program

public static void main(String arg[])
  {
  Tree t1 = 
    new Nonleaf(new Nonleaf(new Leaf("a"), new Leaf("b")), new Leaf("c"));

  Tree t2 = new Nonleaf(t1, t1);

  Tree t3 = new Nonleaf(t1, t2);

  Tree t4 = new Nonleaf(t3, t2);


  test(t1, "t1");
  test(t2, "t2");
  test(t3, "t3");
  test(t4, "t4");
  }

public static void test(Tree t, String s)
  {
  System.out.println(s + " leaves = "     + t.leaves() + 
                         ", nonleaves = " + t.nonleaves());

  }
}


class Leaf extends Tree
{
Object value;

Leaf(Object value)
  {
  this.value = value;
  }

int leaves()    { return 1; }
int nonleaves() { return 0; }
}


class Nonleaf extends Tree
{
Tree left;
Tree right;

Nonleaf(Tree left, Tree right)
  {
  this.left = left;
  this.right = right;
  }

int leaves()    { return left.leaves() + right.leaves(); }
int nonleaves() { return 1 + left.nonleaves() + right.nonleaves(); }
}

Resources

All of the code in this assignment specification isProgram verification is covered in Chapter 10 of the text. There are no test files for this assignment.

Reading

Program verification is covered in Chapter 10 of the text.

Submission

You should submit a Cube.java source file that contains a Cube class and the static cube function mentioned above, with your loop invariant included.

In addition, you should submit the proofs of the claims made in both problem 1 and problem 2 above. The proofs can be written by hand and submitted under the door of Olin 245 (upstairs and west from the terminal room). OR, you can submit your proofs inside comments in your Cube.java file. Because the current submit system only handles one submission file (overwriting old submissions with newer ones), please do not submit more than one file electronically (unless you want to overwrite an old submission).

The usual submission command will work:

% cs60submit Cube.java