суммирование списка чисел в dafny

Дафни может провести доказательство, но оно требует некоторой индукции. Следовательно, вы должны написать свое утверждение таким образом, чтобы Дафни спровоцировал попытку индукции. Самый простой способ сделать это — написать лемму. Обычно простое написание утверждения не приводит к тому, что Дафни пытается провести индуктивное доказательство.

function sum (s: seq<int>, i: int) : int {
  if |s| == 0 || i == 0 then 0 
  else s[0] + sum(s[1..], i - 1)  
}

lemma sumLemma(s: seq<int>, i: int)
   requires i >= 0 && i < |s|
   ensures (sum(s, i) + s[i]) == sum(s, i + 1)
{

}

/* 
 code: 
 cnt = 0;  
 while i < |input|
   cnt += input[i]; 
   i += 1
*/

method test (input : seq<int>, cnt : int, i : int) 
{
  // invariant: cnt = sum(input, i) && i <= |input| && i >= 0
  // prove that loop invariant is preserved:

  if cnt == sum(input, i) && i >= 0 && i < |input| 
  { 
      assert i+1 <= |input|;
      assert i+1 > 0;
      sumLemma(input,i);
      assert (cnt + input[i]) == sum(input, i + 1);
  }
}

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

lemma {:induction false} sumLemma(s: seq<int>, i: int)
   requires i >= 0 && i < |s|
   ensures (sum(s, i) + s[i]) == sum(s, i + 1)
{
  if |s| == 0 || i == 0
  { } else {
    sumLemma(s[1..], i-1);
  }
}

Здесь мы проводим индуктивный аргумент либо в отношении (индуктивного) определения последовательности, либо в отношении хорошо обоснованного (естественного) упорядочения положительных целых чисел. Обычно вы можете думать об индуктивном доказательстве как о некотором хорошо обоснованном упорядочении - здесь у нас есть выбор порядка, при котором хвост последовательности меньше, чем последовательность, за исключением пустой последовательности, у которой нет хвоста; или естественное упорядочение положительных целых чисел. Техника индуктивного доказательства говорит, что вы можете доказать некоторое свойство для всех элементов порядка следующим образом:

1. доказательство свойства для всех наименьших элементов
2. доказательство свойства для произвольного другого элемента в предположении, что свойство выполняется для предшествующего элемента (мы называем это предположение гипотезой индукции)

Итак, в нашем случае доказательство имеет два случая:

1. В базовом случае либо последовательность пуста, либо i==0 — в этом случае мы также находимся в базовом случае рекурсивной функции sum. Дафни легко доказывает этот случай непосредственно определением sum.

2. Индуктивный случай - здесь мы вызываем гипотезу индукции. Это sumLemma относится к хвосту последовательности, а i-1. Дафни может доказать этот случай с помощью гипотезы индукции и определения sum (вы можете думать об этом как о том, что Дафни разворачивает определение sum один раз).

Для достоверности Дафни также должен доказать, что сама индукция хорошо обоснована. Это соответствует доказательству того, что лемма sumLemma завершается. Dafny всегда доказывает полную правильность (прекращение) функций и процедур (если только вы не запретите это делать или в каких-то особых случаях). Большую часть времени Dafny угадывает правильную меру прекращения, но если у вас есть случай, когда он не может угадать меру прекращения, вы можете указать пункт уменьшения.

lemma {:induction false} sumLemma(s: seq<int>, i: int)
   decreases s
   requires i >= 0 && i < |s|
   ensures (sum(s, i) + s[i]) == sum(s, i + 1)

Причина, по которой индуктивная лемма и индуктивно определенная функция очень похожи по структуре, заключается в том, что нам нужно, чтобы базовый случай индукции соответствовал базовому случаю индукционного доказательства, чтобы избежать потенциальной проблемы, связанной с развертыванием определения sum. неизвестное/произвольное количество раз (т.е. если базовый случай индукции был на некоторое количество шагов выше в порядке, чем базовый случай sum).

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