Jak napisałbym pętlę dla tego niezmiennika?
Są to twierdzenia dla algorytmu, aby znaleźć minimum tablicy b [h.k]:
Precondition: h <= k < b.length
Postcondition: b[x] is the minimum of b[h...k]
Czy to poprawna pętla dla tego niezmiennika?
niezmiennik: b [x] to minimum b [h ... t]
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;}
}