Дафни простое утверждение не выполняется - PullRequest
Новая
       56

Дафни простое утверждение не выполняется

0 голосов
/ 19 июня 2020

В exercise_1a что можно сделать, чтобы сделать утверждение cnt > 0 действительным? 

method exercise_1a(n: int)
    requires n > 0
{
    var idx := 0;
    var cnt := 0;

    while idx < n
        decreases n - idx
    {
        idx := idx + 1; 
        cnt := cnt + 1;
    }

    assert idx > 0; // valid
    assert cnt > 0; // *** invalid ***
}

Удивительно, но эта версия также делает недействительным утверждение idx > 0: 

method exercise_1b(n: int)
    requires n > 0
{
    var idx := 0;
    var cnt := 0;

    while idx < n && cnt < n
        decreases n - idx
        decreases n - cnt
    {
        idx := idx + 1; 
        cnt := cnt + 1;
    }

    assert idx > 0; // *** invalid ***
    assert cnt > 0; // *** invalid ***
}

1 Ответ

1 голос
/ 19 июня 2020

В вашем первом фрагменте кода, когда while l oop выходит, Дафни знает только это !(idx < n). Следовательно, он может сделать вывод, что idx > 0. Однако Дафни ничего не знает о переменной cnt на данный момент, поэтому ваше второе утверждение не выполняется.

Во втором фрагменте кода, когда while l oop завершается, все Дафни он знает, что это !(idx < n && cnt < n) (опять же, отрицание условия на while l oop). Это эквивалент idx > n || cnt > n. Отсюда Дафни может вывести idx > 0 || cnt > 0, но он не сможет доказать ни idx > 0, ни cnt > 0 самостоятельно.

Чтобы исправить это, вам нужно добавить некоторую связь между переменными cnt и idx, которые Дафни может проверить, а затем использовать. 

    while idx < n && cnt < n 
        decreases n - idx 
        decreases n - cnt 
        invariant idx == cnt 
    {   
        idx := idx + 1;  
        cnt := cnt + 1;
    }

Дополнительная строка invariant сообщает Дафни проверку, что idx == cnt будет сохраняться на каждой итерации l oop, и тогда он может использовать этот факт в конце. Однако Дафни не узнает, чтобы рассмотреть факт idx == cnt, если вы не скажете ему об этом.

(В качестве примечания вы увидите, что Дафни может самостоятельно определить, что n > 0 содержится в конце while l oop, даже если вы не указываете его явно, как в invariant. Это потому, что n не изменяется в тело while l oop, поэтому Дафни автоматически перенесет тот факт, что n > 0 с самого начала.)

...