Дафни - инвариант L oop для вложенных циклов - PullRequest
Новая
       12

Дафни - инвариант L oop для вложенных циклов

0 голосов
/ 22 апреля 2020

Я пытаюсь создать программу Dafny, которая возвращает true тогда и только тогда, когда A не содержит дубликатов.

Это то, что я имею до сих пор, однако инвариант invariant r <==> (forall j :: 0 <= j < i && j != i ==> A[j] != A[i]); говорит, что он не будет удерживаться при входе.

Любой совет, что я делаю неправильно? 

`method CheckArr1(A: array<int>) returns (r: bool)
requires A.Length > 0
ensures r <==> (forall i, j :: 0 <= i < A.Length && 0 <= j < A.Length && i != j ==> A[i] != A[j]);
{
    var i := 0;
    r := true;
    while i < A.Length 
    decreases A.Length - i;
    invariant i <= A.Length;
    invariant r <==> (forall x, y :: 0 <= x < i && 0 <= y < i && x != y ==> A[x] != A[y]);
    {
        var j := 0;
        while j < i
        decreases i - j;
        invariant j <= i;
        invariant r <==> (forall j :: 0 <= j < i && j != i ==> A[j] != A[i]);
        {
            r := (r && (A[j] != A[i]));
            j := j + 1;
        }
        i := i + 1;
    }
}`

1 Ответ

0 голосов
/ 24 апреля 2020

Ошибка «инвариант не удерживает запись» относится к объявленному инварианту 

r <==> (forall j :: 0 <= j < i && j != i ==> A[j] != A[i])

внутреннего l oop. При входе к этому l oop, j равно 0, поэтому условие, которое необходимо сохранить при входе во внутренний l oop, равно 

r <==> (0 <= 0 < i && 0 != i ==> A[0] != A[i])

, которое мы можем упростить до 

r <==> (0 < i ==> A[0] != A[i])           // (*)

Нет оснований полагать, что r будет хранить это значение при входе во внутреннюю l oop. Все, что вы знаете внутри тела внешнего l oop, - это 

r <==> (forall x, y :: 0 <= x < i && 0 <= y < i && x != y ==> A[x] != A[y]) // (**)

, который говорит, что r говорит вам, есть ли какие-либо дубликаты в первых i элементах. Условие (*) что-то говорит о a[i], тогда как (**) ничего не говорит о a[i].

Из вашей текущей программы было бы проще, если бы вы изменили внутренний l oop на используйте другую переменную, скажем s, для достижения заданного вами инварианта. То есть используйте инвариант 

s <==> (forall j :: 0 <= j < i ==> A[j] != A[i])

Затем, после внутреннего l oop, обновите r, используя значение, вычисленное для s.

...