What will be the decreases value for multiply two integer in Dafny

Question

Basically, my target is to learn dafny basics. But I am confused about invariant and decreases. In this code, my first while loop decreases by one so I have set decreases b but in my inner loop it is divided by 10, so when I was trying to set up b%10 as a decreases value, it always showed me an error. here I need some expert suggestions. What will be the decreases value for the second while loop in this code in this code invariant and decreases values are right?

method MultiplyTheory(N: int, M: nat) returns (Res: int)
  ensures Res == M*N;
  requires N>=0 && M>=0;
{
  var a := N;
  var b := M;
  var x := 0;
  var i :=0;
  while (b > 0)    
  invariant M * N == a * b + x
  decreases b
  {
    while (b % 10 != 0) 
    invariant M * N == a * b + x    
    decreases ?? // what will be the value here ??
    {
      x := x + a; 
      b := b - 1;
      
    }
    a := 10 * a;
    b := b / 10; 
  
  }
  Res := x; 
}

Answer 1

Here is a verification debugging technique: you should first write the assertion that, if proven, would make your previous failing assertions to verify. Since you have two errors, one on the postcondition, and one on the outer decrease clause, here are two assertions you could insert.
If you want to see the solution, skip the steps and go to the end of this post.

Steps to solution

method MultiplyTheory(N: int, M: nat) returns (Res: int)
  ensures Res == M*N;
  requires N>=0 && M>=0;
{
  var a := N;
  var b := M;
  var x := 0;
  var i :=0;
  while (b > 0)    
  invariant M * N == a * b + x
  decreases b
  {
    var oldB := b;
    while (b % 10 != 0) 
    invariant M * N == a * b + x
    {
      x := x + a; 
      b := b - 1;
      
    }
    a := 10 * a;
    b := b / 10;
    assert b < oldB; // Just added: If proven, the decreases condition holds
  }
  Res := x;
  assert Res == M*N; // Just added: If proven, the postcondition would be ok
}

Now you see the two errors are on these assert. It's time to "move the asserts up" by applying weakest precondition rules. That means we keep the assert, but we write assert before their preceding statement such that, if these new assertions held, the old assertions would be verified:

method MultiplyTheory(N: int, M: nat) returns (Res: int)
  ensures Res == M*N;
  requires N>=0 && M>=0;
{
  var a := N;
  var b := M;
  var x := 0;
  var i :=0;
  while (b > 0)    
  invariant M * N == a * b + x
  decreases b
  {
    var oldB := b;
    while (b % 10 != 0) 
    invariant M * N == a * b + x
    {
      x := x + a; 
      b := b - 1;
      
    }
    a := 10 * a;
    assert b / 10 < oldB; // Just added. The next assert conditionally verify
    b := b / 10;
    assert b < oldB;
  }
  assert x == M * N; // Just added. The next assert conditionally verify.
  Res := x;
  assert Res == M*N;
}

See in your IDE how the error is now on the two most recent asserts. Let's consider the second assert x == M * N;. Why is it wrong? There is an invariant that says M * N == a * b + x. So, if x == M * N;, it probably means that b should be equal to zero. However, when we exit the while loop, we only know the negation of the guard, which is !(b > 0), or b <= 0. That's why we could not conclude! Since we never intended b to be non-positive, we either need to add the invariant b >= 0 to the outer loop, or simply change the guard to b != 0 - but if you do that, then it will complain that with decreases b, b is not bounded by zero anymore. So the invariant is better.

method MultiplyTheory(N: int, M: nat) returns (Res: int)
  ensures Res == M*N;
  requires N>=0 && M>=0;
{
  var a := N;
  var b := M;
  var x := 0;
  var i :=0;
  while (b > 0)    
  invariant M * N == a * b + x
  invariant b >= 0  // Just added
  decreases b
  {
    var oldB := b;
    while (b % 10 != 0) 
    invariant M * N == a * b + x
    {
      x := x + a; 
      b := b - 1;
      
    }
    a := 10 * a;
    assert b / 10 < oldB;
    b := b / 10;
    assert b < oldB;
  }
  assert x == M * N;
  Res := x;
  assert Res == M*N;
}

Now the invariant b >= 0 might not be maintained by the loop. This is because the inner while loop modifies b and does not give invariant on the value of b. Of course, we want b >= 0. So we add the invariant in the inner loop.

method MultiplyTheory(N: int, M: nat) returns (Res: int)
  ensures Res == M*N;
  requires N>=0 && M>=0;
{
  var a := N;
  var b := M;
  var x := 0;
  var i :=0;
  while (b > 0)    
  invariant M * N == a * b + x
  invariant b >= 0
  decreases b
  {
    var oldB := b;
    while (b % 10 != 0) 
    invariant M * N == a * b + x
    invariant b >= 0  // Just added
    {
      x := x + a; 
      b := b - 1;
    }
    a := 10 * a;
    assert b / 10 < oldB;
    b := b / 10;
    assert b < oldB;
  }
  assert x == M * N;
  Res := x;
  assert Res == M*N;
}

Ok, now the only assertion remaining is assert b / 10 < oldB; Note that you don't need to write decreases in the inner clause because the default decreases for E > 0 is inferred to be decreases E, and in this case, Dafny can prove that b % 10 decreases. However, knowing that b%10 == 0 at the end is not useful to prove that b itself decreased. If b was 7, it could be that the inner loop was increasing b to 10 before exiting...

The most basic strategy would be to convert the assertion b / 10 < oldB as an invariant. If you add it like that, everything verifies!

Solution

method MultiplyTheory(N: int, M: nat) returns (Res: int)
  ensures Res == M*N;
  requires N>=0 && M>=0;
{
  var a := N;
  var b := M;
  var x := 0;
  var i :=0;
  while (b > 0)    
  invariant M * N == a * b + x
  invariant b >= 0
  decreases b
  {
    var oldB := b;
    while (b % 10 != 0) 
    invariant M * N == a * b + x
    invariant b >= 0
    invariant b / 10 < oldB
    {
      x := x + a; 
      b := b - 1;
    }
    a := 10 * a;
    assert b / 10 < oldB;
    b := b / 10;
    assert b < oldB;
  }
  assert x == M * N;
  Res := x;
  assert Res == M*N;
}

Now, you can experiment a bit about other invariant and observe that the following clauses would solve this last problem as well:

• invariant b <= oldB
• decreases b

Take some time to remove the asserts now because they were only used for scaffolding, but keep the invariant :-)