CODEWITHSUNDEEP
javaalgorithmcorrectness
Andy
Andy

Reputation: 19

How can I prove algorithm correctness?

I have a problem with this exercise in Java, I don't understand how to prove this sum method in Java

This is what I made :

P(0) : If r=0 and i=0 => r=0+a[0]

p(i+1) : r'= r + a[i] and i'=i+1
       r'=r + a[i] + a[i+1]



public static int sum(int[] a) {
    int r = 0;
    int i = 0;
    while (i < a.length) {
        r = r + a[i];
        i = i + 1;
    }

    return r;
}

Upvotes: 0

Views: 435

Answers (2)

user1196549
user1196549

Reputation:

The loop invariant should express that r equals the sum of the elements of a from index 0 to index i, excluded. I.e. r = Sum(k<i: a[k]).

Then we can annotate

int r = 0;
int i = 0;
/* r = Sum(k<i: a[k]) */
while (i < a.length) {
    r = r + a[i];
    /* r = Sum(k<i: a[k]) + a[i] = Sum(k<i+1: a[k]) */
    i = i + 1;
    /* r = Sum(k<i: a[k]) */
}
/* r = Sum(k<=a.length: a[k]) */

The crux of the proof is

Sum(k<i: a[k]) + a[i] = Sum(k<i+1: a[k])

expressing that the sum is obtained incrementally.

Upvotes: 1

0x5453
0x5453

Reputation: 13589

The easiest method is to define a set of inputs along with their expected outputs. If this is for an exercise, you may be given these values, or you may need to calculate a handful of them by hand. Then I would write unit tests using those known inputs to see if each output matches the expected value. If you find places where they don't match, double check both your algorithm and the expected values. Work through the steps of each side-by-side and figure out which one is wrong (or if both are wrong).

Another option is to write the same algorithm in another language; ideally, one where you can't copy-paste the algorithm's implementation to prevent sharing common bugs. Then run both with a ton of inputs. If both implementations have matching results for every input, you can have a higher confidence that both are correct.

A third option is to find a set of invariants, i.e. things that are provably true at various stages of the algorithm. Then write tests (or just throw in assert statements) at all of those points that show that the invariants hold. Things like for every iteration of the "i" loop, r' >= r. Then run it against a large range of inputs, and if any of those assertions fail, you can start digging in and figuring out what edge case you forgot to handle in your algorithm (e.g. What if the input is empty? How do I handle negative numbers? etc.)

Upvotes: 0

Related Questions