Assignment 6: Exponentiation proof

Due: 5:00pm, Friday, October 5. Value: 30 pts.

For this assignment, you may if you wish use a pen and paper, or you may type if you wish. You may submit through Moodle, or you may submit the sheet(s) of paper to my office. Feel free to slide the paper under my door if I'm away.

Using the axiomatic proof system we studied in class, provide a step-by-step partial correctness proof for the following hypothesis. For each step involving C code, justify the step using one of the seven axioms (Sequence, Consequence, Assignment, Preconditions, Postconditions, Condition, or Iteration). If the step involves no C code, give a short verbal explanation of what specifically makes that fact true.

x = m ∧ y = n ∧ n ≥ 0 }
z = 1;
while (y != 0) {
    if (y % 2 == 0) {
        y = y / 2;
    } else {
        z = z * x;
        y = (y - 1) / 2;
    x = x * x;

z = mn }

Since the proof involves writing similar things many times, you may, if you wish, use letters to represent blocks of code or logical statements, as long as those definitions are clearly defined in a separate section. Do not use arrows in lieu of copying text. Be neat: Part of the grade will be based on how easily I can figure out what you're writing.

Hint: A good invariant to choose is z ⋅ xy = mn.