Can anyone help me with this program? I am new to Dafny. I just need to know what will be invariant and decreases values. Thanks in advance
method MultiplyTwoNumber(N: int, M: nat) returns (Result: int)
ensures Result == M*N;
requires N>=0 && M>=0;
{
var a := N;
var b := M;
var x := 0;
var i :=0;
while (b > 0)
invariant ?? // what will be the invariant value
decreases ?? // what will be the decreases value
{
while (b % 15 != 0)
invariant ?? // what will be the invariant value
decreases ?? what will be the decreases value
{
x := x + a;
b := b - 1;
}
a := 15 * a;
b := b / 15;
}
Result := x;
}
In outer loop b will decrease, since every loop iteration divides b by 15. In inner loop b and b % 15 will decrease.
For invariant observe that in inner loop M * N == a * b + x holds, since every iteration will decrease b by 1 and add a to x as a result a * b + x does not change. Same invariant can be used in outer loop as after loop b must be divisible by 15. And multiplying a by 15 and dividing b by 15 does not change value of a * b + x.