As a source of motivation for students, does anyone could point me to some "real (open source) code" where the programmer commented a loop with an invariant for clarity.
func Search(n int, f func(int) bool) int {
// Define f(-1) == false and f(n) == true.
// Invariant: f(i-1) == false, f(j) == true.
i, j := 0, n
for i < j {
h := i + (j-i)/2 // avoid overflow when computing h
// i ≤ h < j
if !f(h) {
i = h + 1 // preserves f(i-1) == false
} else {
j = h // preserves f(j) == true
}
}
// i == j, f(i-1) == false, and f(j) (= f(i)) == true => answer is i.
return i
}
A few, to give a taste:
ast/print.go printer.Write
// invariant: data[0:n] has been written
// invariants:
// p.state == inSpace:
// p.space is unwritten
// p.state == inEscape, inText:
// data[m:n] is unwritten
// Invariants:
// reading from path; r is index of next byte to process.
// writing to buf; w is index of next byte to write.
// dotdot is index in buf where .. must stop, either because
// it is the leading slash or it is a leading ../../.. prefix.
/*@ loop invariant i;
loop invariant j >= 0;
loop assigns j, eol;
*/
for (j = 0; j < (size_t) i; j++) {
if (read_buffer[j] == '\n') {
eol = 1;
j++;
break;
}
}
Loop invariants get important in the section on Bentley-McIlroy three section partioning.