Início / coding / Perguntas / 76937544
Accepted
Carl
Asked: 2023-08-20 08:39:47 +0800 CST

Em Dafny, mostre que uma sequência de elementos únicos tem o mesmo tamanho que o conjunto dos mesmos elementos

  • 772

Eu criei um SortedMap verificado em Dafny. É uma sequência de pares (chave, valor). As chaves são números inteiros distintos e classificados. Não consigo descobrir como mostrar que o comprimento do "KeySet" deve ser igual ao comprimento da sequência.

-- Carl

Erro:

this is the postcondition that could not be proved
  |
7 |   ensures |KeySet(sorted_seq)| == |sorted_seq|

Código simplificado:

predicate SortedSeq(sequence: seq<(int, int)>) {
  forall i, j | 0 <= i < j < |sequence| :: sequence[i].0 < sequence[j].0
}

function KeySet(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
{
  set i | i in sorted_seq :: i.0
}


method Main()
{
  var s: seq<(int,int)> := [(1, 2), (30, 40), (50, 50)];
  print KeySet(s);

}
dafny

1 respostas

  1. Best Answer

    Esta propriedade requer uma demonstração por indução. Como a forma como você definiu a função não é recursiva, isso não é fácil de fazer no Dafny. Você pode (1) provar a propriedade em um lema indutivo separado ou (2) alterar a definição para ser recursiva.

    (1)

    function KeySet(sorted_seq: seq<(int, int)>): set<int>
{
  set i | i in sorted_seq :: i.0
}

lemma KeySetSize(sorted_seq: seq<(int, int)>)
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
{
  if sorted_seq == [] {
  } else {
    assert KeySet(sorted_seq) == {sorted_seq[0].0} + KeySet(sorted_seq[1..]);
    KeySetSize(sorted_seq[1..]);
  }
}

// You can optionally then recombined the bare function and lemma 
// into a function with the right specification.
function KeySetWithPost(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySetWithPost(sorted_seq)| == |sorted_seq|
{
  KeySetSize(sorted_seq);
  KeySet(sorted_seq)
}

    (2)

    function KeySet(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
  ensures KeySet(sorted_seq) == set i | i in sorted_seq :: i.0
{
  if sorted_seq == [] then
    {}
  else
    {sorted_seq[0].0} + KeySet(sorted_seq[1..])
}

// Notice the extra postcondition above, which is required for the proof
// to go through. Once the proof is done, you can wrap it in a function
// with no extra postcondition.
function KeySetWithoutExtraPost(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
{
  KeySet(sorted_seq)
}
    • 2

relate perguntas