Блог

Мне нужна помощь в доказательстве корректности итеративной программы:

 def term_ex_2(x,y):
 ''' Pre: x and y are natural numbers '''
 a = x
 b = y
 while a >= 0 or b >= 0:
     if a > 0:
         a -= 1
     else:
         b -= 1
 return x * y
  

Я знаю, что мне нужно каким-то образом найти инвариант цикла и доказать его путем индукции в цикле. Проблема в том, что операторы if / else здесь путают меня в том, как их придумать.

Я также должен доказать, завершается ли программа или нет после этого.

У меня есть общее представление о том, что такое пошаговый процесс, но я не знаю, с чего начать в этом примере из домашнего задания.

Любые советы будут оценены.

Обратите внимание, что на каждой итерации вашего внешнего while цикла a значение или b уменьшается на 1.

Поскольку x y предполагается, что и являются натуральными числами, оба они изначально > 0 .

Инвариант цикла: a >= 0 (Могут быть и другие возможности!)

Кроме того, программа не завершается, что совершенно очевидно из приведенного выше инварианта цикла, поскольку он заставляет while цикл вычислять true всегда.

Эскиз доказательства: пока a > 0 цикл продолжает a уменьшаться, пока не достигнет 0 . Затем else начинается выполнение условия, которое продолжает уменьшаться b вечно, поскольку a == 0 while цикл повторяется снова и снова.

Классическое использование помещения самого инварианта цикла в условие завершения цикла, чтобы цикл выполнялся бесконечно!