产品m*n Dafny

Question

method Product1 (m: nat, n: nat) returns (res:nat) 
    ensures res == m * n; //postcondition
    // requires m >= 0 && n >= 0 
{   
    var m1: nat := 0; 
    var n1: nat := 0; 
    res := 0; 
    while (m1 < m) 
        // invariant res == m1*n + (m-m1)*n 
        invariant res + (m-m1)*n == m * n && (m1 <= m)       
    { 

        n1 := 0; 

        while (n1 < n)  
            // invariant res == m1*n + n1
            // invariant res+n1+ (n - n1) == (m1)*n
            invariant res + n == (res+n1 + (n-n1)) && (n1 <= n)
        
        { 
            res := res + 1;
            n1 := n1 + 1; 
        } 
            //(res + m1) n ==? m*n


        m1 := m1 + 1; 


    }
 }

该方法是关于m* n的计算。

你能给我指点一下我该在哪里修吗？

我需要找到合适的不变量。

我所做的就是

对于第一个不变量，

m*n是我们想要计算的，we是我们计算出来的(m-m1)*n是我们需要进一步计算的

对于第二个不变量，

res +n是我们想要计算的，res+n1是我们计算出来的(n-n1)是我们需要进一步计算的。

Answer 1

问题是，内环不变量没有足够的信息来在内环退出后重新建立外部循环不变量。您还需要在内部循环中跟踪res、m1和m * n之间的关系。