python - この累乗関数のループ不変式を見つける

Question

計算理論コースで反復プログラム/関数の正しさを証明するという概念を理解するのに苦労しています。より具体的には、ループ不変条件を考え出す方法がわかりません。関数が複数のループ不変条件を持つことができることは理解していますが、事後条件を証明するのに役立つ不変条件を見つける方法については、完全な謎です。私は現在、いくつかの宿題に取り組んでおり、次の関数のループ不変式を見つける方法がわかりません。

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

今のところ、関数がどのように機能するかは理解していますが、前に述べたように、この関数が a^b を返すことを示すのに役立つ適切なループ不変条件を見つけようとすると、非常に途方に暮れます。