Product m*n Dafny

user_14265848 0
Viewed 49
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; 


    }
 }

The method is about calculating m * n.

Could you guide me a little bit about where I should fix it?
I need to find appropriate invariants..

What I've done is that
for the first invariant,

m*n is what we want to calculate

res is what we've calculated

(m-m1)*n is what we need to calculate further

For the second invariant,

res + n is what we want to calculate

res+n1 is what we've calculated

(n-n1) is what we need to calculate further.

dafny
1 Answers

The issue is that your inner loop invariant does not have enough information to re-establish the outer loop invariant after the inner loop exits. You need to keep track of the relationship between res, m1, and m * n in the inner loop as well.

user_4382670
Related