我怎么写这个不变量的循环？

这些是算法的断言，用于查找数组b [hk]的最小值：

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

这是这个不变量的正确循环吗？

不变量：b [x]是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;} } 

Answer 1

你可以通过这种方式找到最小的数组（伪代码）：

 // assume b.length > 0 min = b[0] for i=1 to b.length if b[i] < min min = b[i] 

要将其限制为b[h, ..., k] ：

 min = b[h] for i=h+1 to k if b[i] < min min = b[i] 

所以你基本上只是改变了循环的上限和下限

由于h<=k ， b[h]有效并且从下一个元素执行循环，直到k遍历reqiured元素（如果h==k ，则循环为空）

更新：因为你一直无法将伪代码实现到java中，我会为你翻译它：

 // assume: int b[]; int h; int k; h<=k<=b.length and b.length>0 // find min == b[i] such that b[i]<=b[j] for all h<=j<=k int min = b[h]; for (int i=h+1; i 

注意：您也可以将i=i+1写为++i