Может ли кто-нибудь помочь мне с этой программой? Я новичок в Дафни. Мне просто нужно знать, что будет инвариантным и уменьшать значения. заранее спасибо
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;
}
Я хотел знать на каждой итерации цикла while, что будет инвариантным значением и уменьшать значение
инвариант ?? уменьшается ?? каковы будут эти два значения
Вы до сих пор не представили, каков ваш мыслительный процесс в отношении создания инварианта?
@DivyanshuRanjan спасибо за ваши комментарии. Здесь у меня есть два цикла while для первого цикла while. Я просто проверяю значение b и в конце присваиваю значение своему умножению на старое значение a, а также обновляю значение b. но я смущен, как я могу реализовать эту логику в инварианте.
Вот подсказка: подумайте о числах, написанных в базе 15. Внутренний цикл вычисляет строки в длинном умножении. И внешние петли суммируют эти строки. Можете ли вы попробовать, что придумать инвариант для основания 2. Можете ли вы обобщить его на основание 15
Я совершенно новичок в инварианте. не могли бы вы помочь мне написать его? @DivyanshuRanjan
Во внешнем цикле 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 таким же, как первый, и уменьшение будет? ?
Можете ли вы указать, что вы пытались и где вы застряли