我正在为语言理论考试做修订作业。我们可以做的一些练习包括为几种方法编写前置条件和后置条件以及循环不变量。
我已经完成了一个，并且认为它非常好（如果不是，请告诉我：P），下一个应该是相似的，但是有一个简单的方法来解决它。
int sum(int[] a) //method header
Pre: even(a.length) //precondition
Post: result = SUM(i=0;a.length−1) a[i] //postcondition
int sum(int[] a) {
int r = 0;
int k = 0;
while (k < a.length) {
r = r + a[k];
k = k + 1;
}
return r;
}
我计算出 pre/pos + loop inv 是：
Pre: even(a.length) ∧ r = 0 ∧ k = 0
Post: r = SUM(i=0;a.length−1) a[k]
Inv: 0 ≤ k ≤ a.length ∧ r = SUM(i=0; k −1) a[i]
我需要对这些（非常）相似的方法做同样的事情：
1.
int r = 0;
int k = a.length-1;
while (k >= 0 ) {
r = r + a[k];
k = k - 1;
}
return r;
2.
int r = 0;
int k = 0;
while (k < a.length/2) {
r = r + a[k] + a[a.length-1-k];
k = k + 1;
}
return r;
3.
int r = 0;
int k = 0;
while (k < a.length) {
r = r + a[k] + a[k+1];
k = k + 2;
}
return r;
4.
int r = 0; int s = 0;
int k = 0; int l = a.length-1;
while (k < l) {
r = r + a[k]; s = s + a[l];
k = k + 1; l = l - 1;
}
return r + s;
所以基本上我在问，我的第一部分是否正确（顶部的前/后/循环），如果是这样，这四个如何变化（似乎并不多）。
提前感谢您的帮助。
[编辑]
已尝试 Q1（质量不确定）
Pre: even(a.length) ∧ r = 0 ∧ k = a.length-1
Post: r = SUM(a.length−1; i=0) a[k]
Inv: 0 ≤ k ≤ a.length ∧ r = SUM(k-1; i=0) a[i]