4 ms·

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

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.

dilap 11y ago
Here's binary search from Go's sort package: 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 } There's lots more examples of you search for "invariant" thru the std library source code. A few, to give a taste: ast/print.go printer.Write // invariant: data[0:n] has been written printer/printer.go trimmer.Write: // invariants: // p.state == inSpace: // p.space is unwritten // p.state == inEscape, inText: // data[m:n] is unwritten path/filepath/path.go: path.Clean // 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. Invariants really are a really useful way to think about code.
- ufo 11y ago
  Binary search is one of my favorite examples for introducing people to loop invariants. There are tons of opportunities to mess up with an off-by-one error but if you state the invariant beforehand getting it right is super easy. There are also many variations of the binary search problem so you can't just memorize the implementation.
eliteraspberrie 11y ago
Here's an example in a getline implementation: https://github.com/eliteraspberries/ttyprompt/blob/master/getline.c#L55 https://github.com/eliteraspberries/ttyprompt/blob/master/ge... /*@ 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 are part of the ACSL specification language, and they can be verified automatically with Frama-C. http://frama-c.com/acsl.html http://frama-c.com/acsl.html
mcguire 11y ago
Weirdly, I hadn't tripped over 'loop invariant' in years, then I scribbled my own ode to them[1] and now this. Loop invariants get important in the section on Bentley-McIlroy three section partioning. [1] http://maniagnosis.crsr.net/2016/02/quicksort.html http://maniagnosis.crsr.net/2016/02/quicksort.html

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.

dilap 11y ago

Here's binary search from Go's sort package: 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 } There's lots more examples of you search for "invariant" thru the std library source code. A few, to give a taste: ast/print.go printer.Write // invariant: data[0:n] has been written printer/printer.go trimmer.Write: // invariants: // p.state == inSpace: // p.space is unwritten // p.state == inEscape, inText: // data[m:n] is unwritten path/filepath/path.go: path.Clean // 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. Invariants really are a really useful way to think about code.

ufo 11y ago
Binary search is one of my favorite examples for introducing people to loop invariants. There are tons of opportunities to mess up with an off-by-one error but if you state the invariant beforehand getting it right is super easy. There are also many variations of the binary search problem so you can't just memorize the implementation.

eliteraspberrie 11y ago

Here's an example in a getline implementation: https://github.com/eliteraspberries/ttyprompt/blob/master/getline.c#L55 https://github.com/eliteraspberries/ttyprompt/blob/master/ge... /*@ 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 are part of the ACSL specification language, and they can be verified automatically with Frama-C. http://frama-c.com/acsl.html http://frama-c.com/acsl.html

mcguire 11y ago

Weirdly, I hadn't tripped over 'loop invariant' in years, then I scribbled my own ode to them[1] and now this. Loop invariants get important in the section on Bentley-McIlroy three section partioning. [1] http://maniagnosis.crsr.net/2016/02/quicksort.html http://maniagnosis.crsr.net/2016/02/quicksort.html