이 힘 함수에 대한 루프 불변성 찾기

Question

나는 Theory of Computation 과정에서 반복 프로그램/함수의 정확성을 증명하는 개념을 파악하는 데 어려움을 겪고 있습니다. 좀 더 구체적으로, 나는 루프 불변성을 생각해 낼 수있는 방법을 모른다. 함수가 다중 루프 불변량을 가질 수 있다는 것을 이해하지만, 포스트 조건을 증명하는 데 도움이되는 것을 찾는 방법에 대한 완전한 신비가 있습니다. 현재 숙제를 통해 작업 중이며 다음 함수에 대한 루프 불변성을 찾는 방법을 알지 못합니다.^

PREcondition: a is a number, b is a natural number. 
POSTcondition: return a^b. 
    def power(a, b): 
     s = a 
     k = b 
     p = 1 
     while k > 0: 
      if k % 2 == 1: 
       p = p * s 
      s = s * s 
      k = k // 2 
     return p 

는 지금, 나는 기능의 작동 방식을 이해하지만 내가 전에 언급 한 나를이 함수는를 반환 보여 도움이 될 것입니다 적절한 루프 불변을 발견 할 때, 나는 슈퍼 잃었어요 비.

Answer 1

^은 일부 언어에서는 "힘"을 의미하지만 파이썬에서는 비트 xor입니다. 파워 연산자는 다음

** 루프가 올바른 결과 향하는 것을 확인 커플되어있다

while k > 0: 
     assert s ** k * p == a ** b 
     if k % 2 == 1: 
      p = p * s 
     s = s * s 
     k = k // 2 
     assert k == 0 or s ** k * p == a ** b 

이

s >= a 
n <= b 

같은 방어 불변 물품 수도