Умножение двух значений int в Dafny

Может ли кто-нибудь помочь мне с этой программой? Я новичок в Дафни. Мне просто нужно знать, что будет инвариантным и уменьшать значения. заранее спасибо

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; 
}

Можете ли вы указать, что вы пытались и где вы застряли

Divyanshu Ranjan 27.10.2022 06:29

Я хотел знать на каждой итерации цикла while, что будет инвариантным значением и уменьшать значение

Engr Aminul Islam 27.10.2022 10:17

инвариант ?? уменьшается ?? каковы будут эти два значения

Engr Aminul Islam 27.10.2022 11:19

Вы до сих пор не представили, каков ваш мыслительный процесс в отношении создания инварианта?

Divyanshu Ranjan 27.10.2022 13:26

@DivyanshuRanjan спасибо за ваши комментарии. Здесь у меня есть два цикла while для первого цикла while. Я просто проверяю значение b и в конце присваиваю значение своему умножению на старое значение a, а также обновляю значение b. но я смущен, как я могу реализовать эту логику в инварианте.

Engr Aminul Islam 27.10.2022 13:34

Вот подсказка: подумайте о числах, написанных в базе 15. Внутренний цикл вычисляет строки в длинном умножении. И внешние петли суммируют эти строки. Можете ли вы попробовать, что придумать инвариант для основания 2. Можете ли вы обобщить его на основание 15

Divyanshu Ranjan 27.10.2022 14:01

Я совершенно новичок в инварианте. не могли бы вы помочь мне написать его? @DivyanshuRanjan

Engr Aminul Islam 27.10.2022 14:23
Некоторые методы, о которых вы не знали, что они существуют в Python
Некоторые методы, о которых вы не знали, что они существуют в Python
Python - самый известный и самый простой в изучении язык в наши дни. Имея широкий спектр применения в области машинного обучения, Data Science,...
0
7
75
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Во внешнем цикле b будет уменьшаться, так как каждая итерация цикла делит b на 15. Во внутреннем цикле b и b % 15 будут уменьшаться.

Для инварианта обратите внимание, что во внутреннем цикле выполняется M * N == a * b + x, поскольку каждая итерация будет уменьшать b на 1 и добавлять a к x, в результате чего a * b + x не изменится. Тот же инвариант можно использовать во внешнем цикле, так как после цикла b должно делиться на 15. И умножение a на 15 и деление b на 15 не меняет значение a * b + x.

поэтому для первого цикла инвариант будет инвариантом M * N == a * b + x и уменьшением = b% 15, а для второго инварианта цикла M * N == a * b + x таким же, как первый, и уменьшение будет? ?

Engr Aminul Islam 27.10.2022 15:02

Другие вопросы по теме