Как бы я написал цикл для этого инварианта?
Это утверждения алгоритма для нахождения минимума массива b [h.k]:
<code>Precondition: h <= k < b.length Postcondition: b[x] is the minimum of b[h...k] </code>
Это правильный цикл для этого инварианта?
инвариант: b [x] - минимум 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>