Дафни не проверяет тривиальное утверждение - PullRequest
Новая
       28

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

0 голосов
/ 16 февраля 2020

Код ниже, также в https://rise4fun.com/Dafny/I4wM, 

function abst(bits: array<int>,low:int,high: int): int
    requires 0<=low<=high<=8
    requires bits.Length==8
    decreases high-low
    reads bits
{   if low==high
        then 0 
        else 2*abst(bits,low+1,high) + bits[low]
}

method M() {

    var byte: int;
    var bits:= new int[8];
    bits[0]:= 1;
    bits[1]:= 1;
    bits[2]:= 1;
    bits[3]:= 1;
    bits[4]:= 1;
    bits[5]:= 1;
    bits[6]:= 1;
    bits[7]:= 1;

    // assert abst(bits,2,2) == 0; // Why is this needed?
    assert abst(bits,0,2) == 3;

}

не в состоянии проверить утверждение в последней строке. (Я использую он-лайн Dafny на Rise4Fun.) Если утверждение незадолго до этого прокомментировано, проверка успешна.

Буду признателен за помощь. Спасибо!

1 Ответ

1 голос
/ 18 февраля 2020

Верификатор Dafny разворачивает функции только один или два раза. В частности, если функция встречается в утверждении, которое вы пытаетесь доказать (как это делает abst в вашем примере), то функция будет развернута дважды. Однако, чтобы подтвердить ваше утверждение, определение abst необходимо развернуть 3 раза. Следовательно, верификатор не может доказать это автоматически. Вам придется помочь ему в этом.

Когда вы раскомментируете первое утверждение, оно используется в доказательстве второго утверждения. Поскольку первое утверждение обеспечивает последний экземпляр abst, который вам нужен, это помогает доказать второе утверждение. Само первое утверждение также доказано, но оно автоматически c, поскольку для него требуется только одно развертывание abst.

. Если подробно выписать доказательство, оно выглядит следующим образом: 

calc {
  abst(bits,0,2);
==  // def. abst
  2*abst(bits,1,2) + bits[0];
==  // def. abst
  2*(2*abst(bits,2,2) + bits[1]) + bits[0];
==  // def. abst
  2*(2*0 + bits[1]) + bits[0];
==  // def. bits[0] and bits[1]
  2*(2*0 + 1) + 1;
==  // arithmetic
  3;
}

В этом доказательстве вы можете увидеть необходимые экземпляры функции.

Вам действительно нужны массивы в вашем приложении? Массивы размещаются в куче и являются изменяемыми (что означает, что вам нужно предложение reads и другие сложности). Если вам нужна только неизменная последовательность, я бы порекомендовал вам изменить array<int> на seq<int>. Это облегчит работу (опять же, если вам не нужны изменяемые качества массивов). Более того, для вашего утверждения выше это приносит еще одно преимущество: все аргументы, которые вы затем передаете abst, являются литералами. Для литералов Дафни готов развернуть функции (более или менее) без ограничений. Итак, ваше первоначальное утверждение проверяется автоматически.

Rustan

...