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

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 (количество итераций в то время как loop), где как будто x не равно 0, а x < b, тогда возвращается -1. У меня просто такое чувство, что мне нужно как-то это доказать.

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

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

Answer 1

Мы не можем доказать правильность без точного указания того, что должна делать функция, чего я не могу найти в вашем вопросе. Даже название функции не помогает: как уже отмечалось, ваша функция возвращает 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 не допускаются?)

Answer 2

При условии, что алгоритм завершается (для этого предположим, что 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 не совсем похоже на подходящее название для него ...