Доказательство инвариантности цикла и алгоритма

Question

Как получить инвариант цикла и доказать его для следующего алгоритма.

power(x,y): 
    z = 1 
    m = 0 
    while m < y: 
     z = z*x 
     m = m+1 
    return z 

Answer 1

Во-первых, я думаю, что вы имеете в виду г = г * х Чтобы показать инвариант цикла для любого заданного цикла, вы должны прийти с заявлением, что не меняется в начале и в конце каждой итерации , Используя этот инвариант, вы докажете, что когда программа завершается, функция работает. ваша функция сила в основном пытаясь сделать x^y.

Позволяет построить инвариант цикла: Z = x^m. Вы можете видеть, что это верно как в начале, так и в конце цикла.

Вы также знаете, что цикл может только выход, когда нет (т = у, или т = у.

Так что, если Z = х^м, а по окончании т = у. Тогда Z = х^у.

таким образом, мы можем видеть, что эта программа является частично правильным