¿Cómo escribiría un bucle para este invariante?
Estas son afirmaciones para que un algoritmo encuentre el mínimo de una matriz b [h.k]:
<code>Precondition: h <= k < b.length Postcondition: b[x] is the minimum of b[h...k] </code>
¿Es este el bucle correcto para este invariante?
invariante: b [x] es el mínimo de 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>