3

我正在学习循环不变量，我一直在用越来越难的问题挑战自己。今天我解决了一个问题，但我不确定我的解决方案是否正确。任何人都可以验证我的答案，并请解释而不是仅仅给出解决方案吗？

代码：

/**
 * @require a!= null && b!=null && a.size() == b.size() &&
 * !a.contains(null) && !b.contains(null)
 * @ensure \result is an array of size a.size() such that
 * for each index j of \result, c.get(j) is
 * the minimum of a.get(j) and b.get(j)
 */
public static List<Integer> pairwiseMin(List<Integer> a, List<Integer> b) {
    List<Integer> c = new ArrayList<Integer>();
    int i = 0;
    while (i < a.size()) {
        if (a.get(i) <= b.get(i)) {
            c.add(a.get(i));
        } else {
            c.add(b.get(i));
        }
        i++;
    }
    return c;
}

循环不变量：c.size() == i

问题：

简要解释谓词c.size()==i是否是循环不变量。如果它是循环不变量，请解释是否足以验证该方法在其规范方面是部分正确的。如果谓词不是循环不变量，或者不足以验证方法 pairwiseMin 的部分正确性，则定义一个循环不变量，可用于显示该方法部分正确。

我的解决方案：

是的，它是循环不变量，因为在执行循环之前和之后满足前置条件后置条件。

第一次迭代：

expected: 
pre: i == 1;
post i == 2;

检查 c.size()

pre: c.size() == 0;
post: c.size == 1;

因此，证明部分正确性就足够了。

4

1 回答 1

-1

我不清楚你在问什么。

但是循环不变量是不合适的。

想想 ArrayList b 的大小比 a 大的情况。

这将导致错误“索引超出范围”。

于 2015-06-11T04:03:10.570 回答