The nominal objectives of this two-part exercise are for students to be exposed to using loop invariants to trace over a loop (without simulating its execution through even one iteration), and to be exposed to using loop invariants to reason about the correctness of a loop body (by tracing only one iteration).

Students like to optimize code. The obvious algorithm for this problem takes linear time. What is interesting here is that in the absence of reasoning with a loop invariant, a log-time algorithm (which is totally different from the usual recursive one) might not be apparent. The presentation will use Dafny, an interactive verification tool, available at: [Link]

The example is a function that computes a non-negative integral power of a real number. Two different loop invariants are presented in distinct illustrations of this function's body. Tracing over the loop without simulating its execution is rather straightforward in both cases. However, it is interesting that the second loop invariant (shown below) is appropriate for two entirely different loop bodies: one that computes the power in linear time and the other in logarithmic time. The process of reasoning about how to write the loop body that is correct for this invariant reveals how the more efficient implementation might be "discovered," making it less mysterious than otherwise is the case.

Below is a code skeleton for computing x to the power p > 0, with the loop invariant appearing in the maintains clause.

double result = 1.0;
double factor = x;
int pLeft = p;

/*
updates
     result, factor, pLeft
maintains
     pLeft >= 0 and result * factor ^ (pLeft) = x ^ (p)
decreases
     pLeft
*/

while (pLeft > 0) {
     ...
}

return result;


Correctness, alternative implementations, performance.

Data structures/algorithms, programming language, or software engineering students.

Medium.

The strength of this in-class activity (or related assignments) is that it connects motivation for loop invariants and improved software performance in a novel way.

Instructors need to teach loop invariants.

None.

Minor mutations of the loops and their loop invariants.