Here&#x27;s binary search from Go&#x27;s sort package:<p><pre><code>    func Search(n int, f func(int) bool) int {
        &#x2F;&#x2F; Define f(-1) == false and f(n) == true.
        &#x2F;&#x2F; Invariant: f(i-1) == false, f(j) == true.
        i, j := 0, n
        for i &lt; j {
            h := i + (j-i)&#x2F;2 &#x2F;&#x2F; avoid overflow when computing h
            &#x2F;&#x2F; i ≤ h &lt; j
            if !f(h) {
                i = h + 1 &#x2F;&#x2F; preserves f(i-1) == false
            } else {
                j = h &#x2F;&#x2F; preserves f(j) == true
            }
        }
        &#x2F;&#x2F; i == j, f(i-1) == false, and f(j) (= f(i)) == true  =&gt;  answer is i.
        return i
    }
</code></pre>
There&#x27;s lots more examples of you search for &quot;invariant&quot; thru the std library source code.<p>A few, to give a taste:<p>ast&#x2F;print.go printer.Write<p><pre><code>    &#x2F;&#x2F; invariant: data[0:n] has been written
</code></pre>
printer&#x2F;printer.go trimmer.Write:<p><pre><code>    &#x2F;&#x2F; invariants:
    &#x2F;&#x2F; p.state == inSpace:
    &#x2F;&#x2F;  p.space is unwritten
    &#x2F;&#x2F; p.state == inEscape, inText:
    &#x2F;&#x2F;  data[m:n] is unwritten
</code></pre>
path&#x2F;filepath&#x2F;path.go: path.Clean<p><pre><code>    &#x2F;&#x2F; Invariants:
    &#x2F;&#x2F;  reading from path; r is index of next byte to process.
    &#x2F;&#x2F;  writing to buf; w is index of next byte to write.
    &#x2F;&#x2F;  dotdot is index in buf where .. must stop, either because
    &#x2F;&#x2F;      it is the leading slash or it is a leading ..&#x2F;..&#x2F;.. prefix.
</code></pre>
Invariants really are a really useful way to think about code.