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. // Invar

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.