Dies sind Behauptungen für einen Algorithmus, um das Minimum eines Arrays b [h.k] zu finden:

<code>Precondition: h <= k < b.length
Postcondition: b[x] is the minimum of b[h...k]
</code>

Ist das die richtige Schleife für diese Invariante?

Invariante: b [x] ist das Minimum von b [h ... t]

<code>int x = t;    int t = h;
// {inv: b[x] is the minimum of b[h...t]}
while (t != k) {
   t = t+1;
   if (b[t] < b[x])
      { x = t;}
}
</code>