Блог

Главная - Вопросы по программированию - Дафни предполагает, что умножение нечетных чисел не всегда дает нечетный результат

Дафни предполагает, что умножение нечетных чисел не всегда дает нечетный результат

#dafny

#дафни

Вопрос:

У меня есть последовательность чисел, и я выполняю операции, основанные на нечетности числа. В конечном итоге это сводится к наличию только нечетных чисел в одной переменной, что приводит к сбою инварианта, поскольку он настаивает на том, что число не является нечетным.

Чтобы проверить это, я сделал это. Здесь, когда число нечетное, оно пытается его умножить. Если я что-то не упустил из виду, умножение двух нечетных чисел всегда должно приводить к другому нечетному числу (поскольку так и должно быть (m 1)*(n 1) ). Хотя dafny признает, что число нечетное, оно называет умножение нарушением утверждения.

 if A[i]%2 == 0 {
  ... // not important skip for now
} else {
  assert A[i]%2 == 1;
  assert (A[i] * A[i])%2 == 1;
  ... // do something with it, lets say multiply
}

Есть ли способ решить эту проблему?
Сам массив содержит целые числа (как четные, так и нечетные).
(это операция, выполняемая в цикле while).

Комментарии:

1. Я в замешательстве, вы говорите, что получаете нарушение утверждения при втором утверждении? Это означало бы, что Дафни не смог бы доказать, что результат был нечетным. Не могли бы вы поделиться полным примером, демонстрирующим вашу ошибку, возможно, через rise4fun ?

2. rise4fun.com/Dafny/q7ww

3. Или вот один со структурой, похожей на то, что я сделал, когда я попытался перенести его и доказать как отдельную функцию, просто чтобы изолировать побочные эффекты. rise4fun.com/Dafny/Ritb

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

Ответ №1:

Мы хотели бы показать следующую лемму.

 lemma odd_mul_odd(a: int, b: int)
requires a % 2 == 1
requires b % 2 == 1
ensures (a * b) % 2 == 1

Проведя несколько математических доказательств в Dafny, я узнал, что одна аксиома, которую он может легко доказать, такова a == (a/b)*b (a%b) .

Поэтому я бы попытался доказать, основываясь на следующей логике:

  • Напишите a=2x 1 для некоторого x
  • Запишите b=2y 1 для некоторого y
  • Запишите (a* b)=4xy 2x 2y 1 = 2(2xy x y) 1
  • Следовательно (a * b)% 2 == 1

Вот это в Дафни,

 lemma odd_mul_odd(a: int, b: int)
requires a % 2 == 1
requires b % 2 == 1
ensures (a * b) % 2 == 1
{
  var x := a / 2;
  var y := b / 2;

  calc {
    a * b;
    {   
      assert a == 2*x   1;
      assert b == 2*y   1;
    }   
    (2*x   1) * (2*y   1); 
    4*x*y   2*x   2*y   1;
    2*(2*x*y   x   y)   1;
  }

  calc {
    (a * b) % 2;
    (2*(2*x*y   x   y)   1) % 2;
    1;  
  }
}

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