Каково будет значение уменьшения для умножения двух целых чисел в Дафни

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

Шаги к решению

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
}

Теперь вы видите две ошибки в этих утверждениях. Пришло время «поднять утверждения», применяя правила самых слабых предварительных условий. Это означает, что мы сохраняем утверждение, но пишем его перед их предыдущим утверждением, так что, если эти новые утверждения верны, старые утверждения будут проверены:

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

Посмотрите в своей среде IDE, как теперь ошибка на двух самых последних утверждениях. Рассмотрим второе утверждение x == M * N;. Почему это неправильно? Существует инвариант, который говорит M * N == a * b + x. Итак, если x == M * N;, это, вероятно, означает, что b должно быть равно нулю. Однако, когда мы выходим из цикла while, мы знаем только отрицание защиты, то есть !(b > 0) или b <= 0. Вот почему мы не смогли сделать вывод! Поскольку мы никогда не предполагали, что b будет неположительным, нам нужно либо добавить invariant b >= 0 во внешний цикл, либо просто изменить защиту на b != 0 - но если вы это сделаете, то он будет жаловаться, что с decreases b, b не ограничен ноль уже. Так что инвариант лучше.

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

Теперь инвариант b >= 0 может не поддерживаться циклом. Это связано с тем, что внутренний цикл while изменяет b и не дает инварианта значения b. Конечно хотим b >= 0. Итак, мы добавляем инвариант во внутренний цикл.

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

Хорошо, теперь осталось только одно утверждение assert b / 10 < oldB; Обратите внимание, что вам не нужно писать decreases во внутреннем предложении, потому что decreases по умолчанию для E > 0 подразумевается как decreases E, и в этом случае Дафни может доказать, что b % 10 уменьшается. Однако, зная, что b%10 == 0 в конце, бесполезно доказывать, что b само уменьшилось. Если бы b было 7, возможно, внутренний цикл увеличивал b до 10 перед выходом...

Самой простой стратегией было бы преобразовать утверждение b / 10 < oldB как инвариант. Если вы добавите это так, все проверяется!

Решение

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

Теперь вы можете немного поэкспериментировать с другим инвариантом и заметить, что следующие предложения решат и эту последнюю проблему:

• invariant b <= oldB
• decreases b

Потратьте некоторое время, чтобы удалить утверждения сейчас, потому что они использовались только для строительных лесов, но сохраните инвариант :-)