Я работаю над ревизионным заданием для экзамена по теории языка. Пара упражнений, которые мы можем выполнить, включают написание условий до и после и циклические инварианты для пары методов.
Я закончил один и думаю, что он довольно хорош (пожалуйста, скажите мне, если это не так: 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 + 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;
Итак, в основном я спрашиваю, верна ли моя первая часть (pre / post / loop вверху), и если да, то как эти четыре изменяются (кажется, не так уж много).
Заранее спасибо за помощь.
[Изменить]
Попытка 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]