Dafny中char数组转整数atoi方法的ensures与循环不变式编写问题

核心问题说明 #

现有代码无法通过验证的原因有三点：

• 前置条件不完整：仅约束字符转数字后<=9，未约束>=0，存在负数值的可能性干扰推导。
• 辅助函数规约不足：ten_pos_pow未明确递推关系的确保子句，Dafny无法自动推导指数运算的关联逻辑。
• 循环不变式约束缺失：仅声明了各位的对应关系，未提供r的取值范围、r与前i位的直接数值关联，Dafny无法推导迭代过程中r的变化与位对应关系的一致性。

解决方案1：使用直接求和式规约（最易验证） #

直接用求和表达式定义r的取值，不需要num_in_int辅助函数，Dafny可自动推导验证：

// 计算10的p次幂
function ten_pos_pow(p:int):int
requires p>=0
ensures ten_pos_pow(p) >= 1
ensures p > 0 ==> ten_pos_pow(p) == 10 * ten_pos_pow(p-1)
{
    if p==0 then 1 else 10 * ten_pos_pow(p-1)
}

method atoi(a:array<char>) returns(r:int)
requires a.Length>0
requires forall k :: 0<= k <a.Length ==> 0 <= (a[k] as int) - ('0' as int) <= 9
ensures r == sum k: int | 0 <= k < a.Length :: ((a[k] as int) - ('0' as int)) * ten_pos_pow(a.Length - k - 1)
{
    var i:int := 0;
    r := 0;
    while i < a.Length
       invariant 0<= i <= a.Length
       invariant r >= 0
       invariant r == sum k: int | 0 <= k < i :: ((a[k] as int) - ('0' as int)) * ten_pos_pow(i - k - 1)
    {
        r := r*10 + (a[i] as int) - ('0' as int);
        i := i + 1;
    }
}

解决方案2：保留num_in_int的实现 #

如果需要保留按位校验的逻辑，需要补充辅助引理证明乘10加位操作后的位对应关系，代码如下：

// 计算10的p次幂
function ten_pos_pow(p:int):int
requires p>=0
ensures ten_pos_pow(p) >= 1
ensures p > 0 ==> ten_pos_pow(p) == 10 * ten_pos_pow(p-1)
{
    if p==0 then 1 else 10 * ten_pos_pow(p-1)
}

// 取整数v从右往左数第i位（i从0开始）
function num_in_int(v:int,i:int) : int
requires i>=0
requires v>=0
{
    (v % ten_pos_pow(i+1))/ten_pos_pow(i)
}

// 辅助引理：证明乘10加新位后的位对应关系
lemma NumShiftLemma(v:int, d:int)
requires v >=0
requires 0<=d<=9
ensures num_in_int(v*10 +d, 0) == d
ensures forall i: int :: i >=1 ==> num_in_int(v*10 +d, i) == num_in_int(v, i-1)
{
}

method atoi(a:array<char>) returns(r:int)
requires a.Length>0
requires forall k :: 0<= k <a.Length ==> 0 <= (a[k] as int) - ('0' as int) <= 9
ensures forall k :: 0<= k < a.Length ==> ((a[k] as int) - ('0' as int)) == num_in_int(r,a.Length-k-1)
{
    var i:int := 0;
    r := 0;
    while i < a.Length
       invariant 0<= i <= a.Length
       invariant r >=0
       invariant forall k :: 0<= k < i ==> ((a[k] as int) - ('0' as int)) == num_in_int(r,i-k-1)
    {
        var d := (a[i] as int) - ('0' as int);
        NumShiftLemma(r, d);
        r := r*10 + d;
        i := i + 1;
    }
}

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