如何写一个正确的代码

我们如何写一个正确的代码?

答案是形式化验证,其中一个是霍尔逻辑

举个例子

快速幂
x> 0 
x/2/2 ... 必定会归到1 或者0, 所以递归会有限次

快速幂
a^x = floor(a^(x/2))^2 *a^(x%1);
fun(a,x) ={
    if(x== 0){
        return 1;
    }elseif(x== 1){
        return  a;
    }
    return  fun(a , floor(x/2)  )*a^(x%1);
}