Почему проверка этого примера Дафни не удалась?

Это пример для изучения Дафни.

method test5(x:array<int>,y:array<int>,n:int)
requires 0<=n
requires 0< x.Length
requires 0< y.Length  
requires x[0]==y[0]; 
requires (x[0]>=0 ==> y[0]>=0)
requires  (y[0]>= 0 ==> x[0]>= 0)
requires  (x[0]+y[0]==0 || x[0]+y[0]>0);
modifies y;  
modifies x; 
ensures  (x[0]==y[0]); 
ensures (x[0]>0 ==> y[0]>0)
ensures (y[0] > 0 ==> x[0] > 0)
ensures  (x[0]+y[0]==0 || x[0]+y[0]>0)     
{     if (x[0]>0)
    {x[0]:=x[0]- 1; 
     y[0]:=y[0]- 1;
     }
}

Почему проверка не проходит?

Может ли Дафни привести контрпример?


dafny
person yongjianLi    schedule 06.03.2019    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Да, вы можете привести контрпример. Если вы используете Visual Studio, просто щелкните красный кружок в том месте, где находится ошибка. Это вызывает отладчик проверки. Если вы используете VS Code, нажмите F7 (см. https://marketplace.visualstudio.com/items?itemName=correctnessLab.dafny-vscode). Это перепроверит вашу программу и покажет вам некоторую информацию из контрпримера.

В вашем случае эти контрпримеры показывают, что x и y равны и изначально имеют x[0]==y[0]==1. Действительно, начиная с этого начального состояния, test5 не установит свое объявленное постусловие.

Рустан

person Rustan Leino    schedule 07.03.2019