Инвариантное доказательство цикла по алгоритму умножения

Question

В настоящее время я застрял в цикле инвариантного доказательства в моем домашнем задании Алгоритм, который мне нужен, чтобы доказать правильность, таков:

Multiply(a,b)
    x=a
    y=0
    WHILE x>=b DO
        x=x-b
        y=y+1
    IF x=0 THEN
        RETURN(y)
    ELSE
        RETURN(-1)

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

Пока что я построил, просто посмотрев на завершение алгоритма, и в этом случае, если x = 0 тогда он возвращает значение y содержащий значение n (количество итераций в цикле while), где как будто x не является 0, а также x < b потом возвращается -1, У меня просто такое чувство, что мне нужно это как-то доказать.

Я надеюсь, что кто-то может помочь мне осветить это, поскольку подобных случаев, которые я обнаружил здесь, было недостаточно.

Большое спасибо заранее за ваше время.

Answer 1

При условии, что алгоритм завершается (для этого давайте предположим, a>0 а также b>0(что достаточно), один инвариант заключается в том, что на каждой итерации вашего while петля, у вас есть x + by = a,

Доказательство:

• вначале, x = a а также y = 0 так что все в порядке
• Если x + by = a, затем (x - b) + (y + 1)b = a, которые являются значениями x а также y для вашей следующей итерации

Иллюстрация:

    Multiply(a,b)
        x=a
        y=0
        // x + by = a, is true
        WHILE x>=b DO
            // x + by = a, is true
            x=x-b // X = x - b
            y=y+1 // Y = y + 1
            // x + by = a
            // x - b + by + b = a
            // (x-b) + (y+1)b = a
            // X + bY = a, is still true
        // x + by = a, will remain true when you exit the loop
        // since we exited the loop, x < b
        IF x=0 THEN
            // 0 + by = a, and 0 < b
            // y = a/b
            RETURN(y)
        ELSE
            RETURN(-1)

Этот алгоритм возвращает a/b когда b водоразделы a, а также -1 иначе. Multiply не совсем похоже на подходящее название для него...

Answer 2

Мы не можем доказать правильность без точного указания того, что должна делать функция, чего я не могу найти в вашем вопросе. Даже название функции не помогает: как уже отмечалось, ваша функция возвращает a/b большую часть времени, когда b водоразделы a, а также -1 иначе. Multiply - неподходящее название для него.

Кроме того, если b=0 а также a>=b "алгоритм" не заканчивается, так что это даже не алгоритм.

Как отметил Алекс М, инвариант цикла для цикла x + by = a, В момент выхода из цикла, мы также имеем x < b, Других гарантий на x потому что (предположительно) a может быть отрицательным. Если бы у нас была гарантия, что a а также b положительные, то мы могли бы гарантировать, что 0<=x<b в тот момент, когда цикл завершается, это означает, что он реализует алгоритм деления с остатком (в конце цикла, y является частным и x это остаток, и он заканчивается аргументом типа "бесконечный спуск": убывающая последовательность натуральных чисел x должен прекратить). Тогда можно сделать вывод, что если x=0, b делит равномерно, и частное возвращается, в противном случае -1 возвращается

Но это не доказательство, потому что нам не хватает спецификации того, что должен делать алгоритм, и спецификации ограничений на его входные данные. (Являются ли a и b целыми положительными числами? Отрицательные и 0 не допускаются?)