Дафни, пост-условие не держится после цикла - PullRequest
Новая
       6

Дафни, пост-условие не держится после цикла

0 голосов
/ 22 мая 2018

В следующем методе Дафни сообщает, что постусловие может не выполняться, хотя я совершенно уверен, что оно выполнено. 

method toArrayConvert(s:seq<int>) returns (a:array<int>)
    requires |s| > 0
    ensures |s| == a.Length
    ensures forall i :: 0 <= i < a.Length ==> s[i] == a[i]  // This is the postcondition that might not hold.
{
    a := new int[|s|];
    var i:int := 0;
    while i < |s|
        decreases |s| - i
        invariant 0 <= i <= |s|
    {
        a[i] := s[i];
        i := i + 1;
    }

    return a;  // A postcondition might not hold on this return path.
}

1 Ответ

0 голосов
/ 22 мая 2018

Действительно, постусловие всегда выполняется, но Дафни не может сказать!

Это потому, что вам не хватает анвариантной аннотации цикла, такой как 

invariant forall j :: 0 <= j < i ==> s[j] == a[j]

После добавления этой строки в цикл, метод проверяет.

Для более подробного объяснения, почемуДафни иногда сообщает об ошибках в правильных программах, см. (Совершенно новый) FAQ .Подробнее об инвариантах цикла см. Соответствующий раздел в руководстве rise4fun .

.
...