Блог

Я новичок в Dafny и изучаю его. Для следующего кода Dafny

 method Dummy(s: seq<nat>) returns (ret: nat)
    requires forall k :: 0 <= k < |s| ==> s[k] > 0
{
    ret := 0;
    var se := s;

    while |se| > 0
    {
        // Pick a random index of the seq.
        var i :| 0 <= i < |se|;
        if se[i] == 1 {
            // Remove the seq element if it is 1.
            se := se[..i]   se[i   1..];
        } else {
            // Replace the seq element with 3 occurences of 1.
            se := [1, 1, 1]   se[..i]   se[i   1..];
        }
    }

    return;
}
  

Я вижу жалобы, которые

 decreases |se| - 0Dafny VSCode
cannot prove termination; try supplying a decreases clause for the loopDafny VSCode
  

Я знаю, что для доказательства завершения, как правило, я должен предоставить decreases предложение. Я просто не могу найти, что вставить в decreases предложение в этом случае. Проще говоря

 decreases |se|
  

это не сработает, так как в else части if инструкции seq размер может фактически увеличиться.

Если это доказательство с помощью пера и бумаги, я хотел бы утверждать, что для любого элемента, равного 1, он будет удален; и для любого элемента, который больше 1, он будет заменен на 3 появления 1, которые все равно будут удалены окончательно. Следовательно se , в конце будет пусто, и цикл завершится.

Как мне преобразовать его в коды, с которыми согласится Dafny?

Ключ в том, чтобы ввести функцию, которую я называю «общий потенциал», которая вычисляет, сколько итераций потребуется циклу для обработки списка. Его определение таково: «для каждого 1 в списке добавьте 1 к общему потенциалу, для каждого не-1 в списке добавьте 4 к общему потенциалу». Затем мы сделаем decreases предложение общим потенциалом. Таким образом, когда 1 удаляется, потенциал уменьшается на 1, а когда не-1 удаляется и заменяется тремя единицами, потенциал также уменьшается на 1.

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