语言理论 - 循环不变量 - 前置/后置条件

Question

我正在为语言理论考试做复习作业。我们可以做的一些练习包括为几种方法编写前置条件和后置条件以及循环不变量。

我已经完成了一个，并且认为它非常好（如果不是请告诉我：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;
}

循环 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]

我需要对这些（非常）相似的方法执行相同的操作：

所以

int r = 0;
int k = a.length-1;
while (k >= 0 ) {
r = r + a[k];
k = k - 1;
}
return r;

我计算出 pre/pos +

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;

基本上

int r = 0;
int k = 0;
while (k < a.length) {
r = r + a[k] + a[k+1];
k = k + 2;
}
return r;

1.2.3.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]

Answer 1

你的 r=SUM 可能应该是 r = SUM(i=0;k −1) a[i]

第一个只是向后计数

数字 2 和 4 本质上是等价的其中 l from 4 是 a.length-1-k 的别名（看看你是否能自己证明这一点），它们都来自数组的任意一端，并从第三

个计数器 var 的增量为 2 k 但不变量并不会因此而改变

Answer 2

有兴趣看看实际的问题，因为..“制定前置条件和后置条件”是无稽之谈：如果考官要求..换一个更好的学校。

您可能会被问到“找到方法终止的最弱的前提条件并给出明确定义的答案，并且在这种情况下找到最强的后置条件”：这是一个明智的问题。

另一方面，考虑到第一种方法以及规定的前置/后置条件，询问循环前置/后置条件和不变量确实有意义，但如上所述，应该向后解决问题：给定预期的后置条件方法的条件，该方法满足其后置条件所需的循环的最弱后置条件是什么？

那么：给定后置条件，循环所需的最弱前置条件是什么？鉴于您可以询问是否可以从所述方法前提条件中推导出该前提条件（不要忘记方法开始和循环之间的代码）。

在这种形式中，even 谓词没有位置，不需要满足循环或方法的后置条件（这是引用的第一个算法）。

有趣的是，您错过了一些重要的先决条件。其中之一是总和在 int 类型的范围内，然而，虽然这是必要的，但如果溢出导致非终止，那么这是不够的。