инвариант цикла для степенной функции - PullRequest
Новая
       39

инвариант цикла для степенной функции

0 голосов
/ 01 марта 2019

пытается доказать правильность, используя цикл-инвариант следующего алгоритма Power: 

    Power(x,n)
     result <- 1
     if n = 1
         then return x
     if n = 0
         then return result
     While n > 0
         if n mod 2 = 1
               do result <- result * x
         n <- n/2(floor value)
        x <- x*x
     return result

Я пытаюсь доказать, что переменная результата вернет правильный ответ, если я обозначу k чтобы быть счетчиком итераций, то каждая итерация x равна x ^ 2 ^ k, а n равно n / 2 ^ k, поэтому оно совпадает.на последней итерации n = 1, так что если n не было нечетным, то результат = 1, и он будет умножен на x ^ 2 ^ k, что является правильным ответом, но если в середине вычисления n нечетно, то я нене знаю, как это доказать.

надеюсь, что вы мне поможете.

...