Início / coding / Perguntas / 79599041
Accepted
f1sherb0y
Asked: 2025-04-30 02:51:53 +0800 CST

O verificador Dafny falha em provar a consequência do multiconjunto

  • 772

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;

functional-programming

2 respostas

  1. Seu método do_nothingé especificado apenas para manter multiset(a[..]) intacto, não necessariamente o array a. Como os elementos em um multiconjunto não têm uma ordem definida, essa propriedade é mantida mesmo se você permutar entradas no array. Por exemplo, a seguir está uma implementação correta de um do_nothingwhen a.Length >1:

    method do_nothing(a: array<int>)
  requires a.Length>1
  modifies a
  ensures multiset(a[..]) == multiset(old(a[..]))
{ 
    a[0],a[1] := a[1],a[0]; 
}

    Agora, no site de chamada de do_nothing, dentro de test, Dafny não se importa com sua implementação de do_nothing, ele apenas considera sua especificação -- e como visto acima, isso não garante que a[0]não possa ter sido trocado por algum outro a[i].

    • 0
  2. Best Answer

    Os multiconjuntos têm gatilhos ocultos para evitar sobrecarregar o verificador de Dafny com gatilhos.

    Você pode adicionar esta afirmação depois do_nothingpara ajudar Dafny a acionar alguns axiomas necessários em multiconjuntos.

    assert 0 !in multiset(a[..]);

    Isso fará com que seu código passe na verificação. Observe que, como se trata de gatilhos, inserir o seguinte código no-op faria o mesmo

    ghost var _ := 0 !in multiset(a[..]);
    • 0

relate perguntas