基于Hoare逻辑验证itoa()函数的相关疑问

循环不变式的修正 #

你最初的不变式思路是对的，但to_integer(s)的处理需要更精准。itoa的do-while循环是每次把n的个位数字追加到字符串s里，所以s的字符顺序是逆序的（比如n=123，循环会依次写入3、2、1，s最终是"321"，反转后才是正确结果）。

修正后的循环不变式P需要明确绑定辅助变量i和s的有效长度：
P: n * 10^i + reverse_to_integer(s[0..i-1]) = n₀
其中：

• n₀是n的初始输入值
• s[0..i-1]表示s的前i个字符（循环执行i次后，s中已经存入了i个数字字符）
• reverse_to_integer()是将输入字符串反转后转换为整数（比如输入"321"，返回123）

这个不变式的正确性可以通过循环体执行前后的状态验证：
执行循环体前满足P ∧ (n≠0)，即n_old * 10^i + reverse_to_integer(s[0..i-1]) = n₀。循环体执行的操作是：取出n的个位数字写入s的第i位，i自增1，n更新为n_old // 10。代入新状态到P后，推导结果仍等于n₀，符合{P ∧ B} S {P}的要求。

初始化的形式化声明 #

在Hoare逻辑中，初始化步骤可以用如下三元组描述：

{true} i:=0; s:=""; n:=n₀ {P}

这里true表示初始状态无约束，执行初始化后必须满足我们定义的不变式P。代入i=0、空字符串s、n=n₀验证：
n₀ * 10^0 + reverse_to_integer(空字符串) = n₀ * 1 + 0 = n₀，完全符合P的要求，所以这个初始化三元组是成立的。

完整的循环验证结构 #

结合初始化、循环体和终止条件，完整的Hoare验证结构如下：

{true}
    i:=0; s:=""; n:=n₀
{P}
    do n≠0 →
        digit := n % 10;
        s[i] := str(digit);
        i := i + 1;
        n := n // 10
    od
{P ∧ ¬(n≠0)}

当循环终止时，¬(n≠0)等价于n=0，代入P可得：
0 * 10^i + reverse_to_integer(s[0..i-1]) = n₀
即reverse_to_integer(s[0..i-1]) = n₀，这说明将s反转后得到的整数就是初始输入的n₀，完全符合itoa函数的功能（最后只需反转s即可得到正确的字符串结果）。

关于终止性的补充 #

你注意到的点非常重要：Hoare逻辑本身只保证部分正确性（如果循环终止，结果必正确），但不保证循环一定会终止。要证明这个循环的终止性，可以引入一个终止变元|n|（n的绝对值，兼容负数输入的情况）：

• 每次循环执行后，|n|会严格递减（因为n被除以10，且循环条件为n≠0，所以|n|的取值始终是非负整数，且每次至少变为原来的1/10）
• 非负整数序列无法无限递减，因此循环必然会终止。

内容的提问来源于stack exchange，提问作者Theo H