Language Theory - Loop Invariants - Pre/Post Conditions

Question

I am working on a revision assignment for an exam on language theory. A couple of the exercises that we can do involve writing pre and post conditions and loop invariants for a couple of methods.

I have completed one, and think it is pretty good (please tell me if it isn't :P), the next ones are supposed to be similar, but is there an easy way to work it out.

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;
}

Which I worked out the pre/pos + loop inv to be:

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]

I need to do the same for these (very) similar methods:

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;

So basically I am asking, is my first part correct (the pre/post/loop at the top), and if so how do these four vary (it doesn't seem to be much).

Thanks for your help in advance.

[Edit]

Attempted Q1 (unsure of quality)

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

your r=SUM should probably be r = SUM(i=0;k −1) a[i]

the first one just counts backwards

numbers 2 and 4 are essentially equivalent with l from 4 being an alias to a.length-1-k (see if you can prove that yourself) they both go from either end of the array and sum from there

the third takes increments of 2 for the counter var k but the invariant doesn't change because of it

Answer 2

Be interested to see the actual question because .. it is nonsense to "work out pre and post conditions": if the examiner asked that .. change to a better school.

You might be asked "find the weakest precondition for which the method terminates and gives a well defined answer, and, in that case the strongest post-condition": that's a sensible question.

On the other hand, given the first method together with the stated pre/post conditions, it does make sense to ask about the loop pre/post conditions and invariant, but as above the question should be worked out backwards: given the intended post-condition of the method, what is the weakest post-condition of the loop required for the method to satisfy its post-condition?

Then: given that post-condition, what is the weakest pre-condition of the loop required? Given that you can then ask if that pre-condition can be deduced from the stated method pre-condition (not forgetting code between the start of the method and the loop).

In that form the even predicate has no place, it is not required to satisfy the post-condition of the loop or method (this is the first algorithm cited).

As a matter of interest you have missed some vital pre-conditions. One of them is that the sum is in the range of type int, however whilst this is necessary it is not sufficient if overflow causes non-termination.