Reputation: 97
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]
Upvotes: 3
Views: 764
Reputation: 4921
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.
Upvotes: 1
Reputation: 48196
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
Upvotes: 2