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

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

Одна из возможностей, доказывающих, что ваш алгоритм имеет ожидаемый ответ, состоит в том, чтобы покрыть его модульными тестами.

@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 2

Инвариант цикла должен выражать, что 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 3

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

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

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