7:30 AM, Tuesday, May 13, 2008 (to be turned in at the beginning of lecture)

After completing this assignment you will:

Write your assertions and program code using a minimal subset of a Java-like language.

In particular, this Java-like subset language is restricted to only use +,-,*,/ integer operations, and uses the Boolean literals, "true" and "false".

This language is further restricted to use only if, while, and assignment statements.

Assertions should be written as,

assert(B);

where B is a Boolean expression, i.e., evaluates to either true or false.

Assert expressions may also make use of the shorthand notation, "SUM", written as shown here,

SUM index=low,hi: EXPR

Which has the meaning,

subst(EXPR,index,low) + subst(EXPR,index,low+1) + ... + subst(EXPR,index,hi)

Or you may use the traditional mathematical symbol, Σ (Note, in case your browser doesn't display, this is a capital Greek SIGMA) where the index,lo are written below and the hi written above. Or you can skip using product shorthands and use the less formal notation with ellipsis (...) as shown in the definitions of INV and POST.

Additional suggestions and guidelines may be discussed during lecture.

Let PRE, the precondition, be defined as

true

This means that on any input to the program, if the program should complete, the postcondition will be satified.

For the following problem, let INV be defined as,

sumsq = SUM x=i..n (x*x)

Informally, when n is less than i,

sumsq = 0

and otherwise is,

sumsq = (i * i) + ... + (n * n)

Let POST, the postcondition, be defined as

sumsq = SUM x=1..n (x*x)

Again informally when n is bigger than 0,

sumsq = (1 * 1) + (2 * 2) + ... + (n * n)

Notice that the only difference between INV and POST is INV's use of the free variable, i, where POST starts from 1.

Write the initialization code, C, and prove, using weakest precondition analysis,

true --> wp(C, INV)

Show all work.

You will need to develop code which supports the invariant assertion is maintained. "Maintained" means that if the invariant is true at the both the beggining of the loop body and the end of the loop body.

To accomplish this let's say, for example, your loop body, B, is a sequence of three statements. And you should be able to annotate by asserting INV before and after these statements.

B. 

assert(INV);
stmt1;
stmt2;
stmt3;
assert(INV);

Prove, using weakest precondition analysis,

INV --> wp(B, INV)

Which means the invariant is true at beginning and ending of your chosen loop body, B.

Show all work.

Write the guard of the while loop. Then prove, using predicate transformers, why this establishes the postcondition, POST to be true.

Please submit completed assignments in a hardcopy printout (or neatly handwritten) on US letter (8 1/2 x 11). Your submission should include all work and be legible and neat.

	Caution
	As advertised, late submissions receive NO CREDIT.