Почему не удается проверить этот пример с Дафни? - PullRequest
Новая
       14

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

0 голосов
/ 07 марта 2019

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

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;
     }
}

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

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

1 Ответ

0 голосов
/ 08 марта 2019

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

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

Rustan

...