Estou trabalhando com Dafny e tentando entender como as especificações, particularmente modifica e garante multiconjuntos, afetam a verificação.
Tenho um método do_nothingespecificado para modificar um array a, mas que garante que o multiconjunto de seus elementos permaneça inalterado. O corpo do método está vazio.
method do_nothing(a: array<int>)
modifies a
ensures multiset(a[..]) == multiset(old(a[..]))
{
// nothing is done
}
method test()
{
var a := new int[6] [2, -3, 4, 1, 1, 7];
assert a[..] == [2, -3, 4, 1, 1, 7]; // Verifies
assert a[0] !=0 ; // Verifies
do_nothing(a);
assert a[0] != 0; // <-- Verification Error: This assertion cannot be proved
}
Minha expectativa:
Como não há 0 dentro ade nada, e dafny concorda que isso do_nothinggarante multiset(a[..]) == multiset(old(a[..])). Portanto, a afirmação a[0] != 0 deve ser válida e verificada com sucesso.
O problema:
Dafny falha ao verificar a afirmação final assert a[0] != 0;