Как я могу доказать правильность алгоритма?

Question

У меня есть проблема с этим упражнением в Java, я не понимаю, как доказать этот метод суммы в Java

Вот что я сделал:

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

Answer 1

Инвариант цикла должен выражать это r равна сумме элементов a из индекса 0 индексировать i, не входит. Т.е. r = Sum(k<i: a[k]),

Тогда мы можем аннотировать

    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]) */

Суть доказательства

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

выражая, что сумма получается постепенно.

Answer 2

Одна из возможностей, которая доказывает, что ваш алгоритм имеет ожидаемый ответ, - это покрыть его модульными тестами.

@Test
public void sumWorksFineWithNaturalValues() {

    int[] input = {1, 2, 3, 4};
    int expectedResponse = 10;

    assertThat(sum(input)).isEqualTo(expectedResponse);
}

@Test
public void sumCanHandleNegativeValues() {

    int[] input = {0, 1, -2, -3, 4};
    int expectedResponse = 0;

    assertThat(sum(input)).isEqualTo(expectedResponse);
}

@Test
public void sumCanHandleEmptyArray() {

    int[] input = {};
    int expectedResponse = 0;

    assertThat(sum(input)).isEqualTo(expectedResponse);
}

Я использовал библиотеку assertj для тестов Java

Answer 3

Самый простой способ - определить набор входных данных вместе с их ожидаемыми выходными данными. Если это для упражнения, вам могут быть даны эти значения, или вам может понадобиться рассчитать несколько из них вручную. Затем я написал бы модульные тесты, используя эти известные входные данные, чтобы увидеть, соответствует ли каждый выходной результат ожидаемому значению. Если вы найдете места, где они не совпадают, проверьте еще раз ваш алгоритм и ожидаемые значения. Проработайте шаги каждого рядом и выясните, какой из них неправильный (или если оба неправильны).

Другой вариант - написать тот же алгоритм на другом языке; в идеале, тот, где вы не можете скопировать и вставить реализацию алгоритма, чтобы предотвратить совместное использование общих ошибок. Затем запустите оба с кучей входов. Если обе реализации имеют совпадающие результаты для каждого ввода, вы можете быть более уверены, что обе они верны.

Третий вариант - найти набор инвариантов, то есть вещей, которые доказуемо верны на разных этапах алгоритма. Затем напишите тесты (или просто добавьте assert утверждения) во всех тех точках, которые показывают, что инварианты имеют место. Вещи как for every iteration of the "i" loop, r' >= r, Затем запустите его для большого диапазона входных данных, и если какое-либо из этих утверждений не сработает, вы можете начать копать и выяснить, какой крайний случай вы забыли обработать в своем алгоритме (например, что делать, если входное значение пустое? номера? и т. д.)