Estou aberto a qualquer forma de escrever CountLessThan que seja verificável. Aqui está o que eu tenho:
function SetLessThan(numbers: set<int>, threshold: int): set<int>
{
set i | i in numbers && i < threshold
}
method CountLessThan(numbers: set<int>, threshold: int) returns (count: int)
ensures count == |SetLessThan(numbers, threshold)|
{
count := 0;
var shrink := numbers;
var grow := {};
while |shrink | > 0
decreases shrink
invariant shrink + grow == numbers
invariant count == |SetLessThan(grow, threshold)|
{
var i: int :| i in shrink;
shrink := shrink - {i};
grow := grow + {i};
if i < threshold {
count := count + 1;
}
}
}
method Main()
{
var s: set<int> := {1, 2, 3, 4, 5};
var c: int := CountLessThan(s, 4);
print c;
// assert c == 3;
}
Este é um pequeno passo para definir um conjunto classificado, depois um mapa classificado e, por fim, um conjunto de intervalos.
Você tem um exercício clássico de depuração de verificação pela frente :)
A abordagem básica para a depuração de verificação é adicionar
assertinstruções para restringir onde está o seu problema.Escrevi uma transcrição completa de uma sessão de depuração idealizada. Sinta-se à vontade para pular para o final se quiser apenas o código funcional.
O código em sua postagem relata o seguinte erro na invariante do loop:
Isso significa que Dafny não conseguiu restabelecer a invariante na parte inferior do loop. Vamos converter isso em uma afirmação.
Na verdade, não fizemos nada, mas observe que o erro na invariante não é mais relatado, portanto, há apenas um total de erros. Isso é Dafny dizendo "se você pudesse provar a afirmação, o restante do código também seria verificado".
Agora começamos a mover a afirmação para trás no loop. A maneira mais fácil de movê-lo para uma instrução if unilateral é introduzir artificialmente uma
elseramificação vazia e, em seguida, fazer uma cópia da afirmação em ambos os lados.Observe que o erro na parte inferior
assertdesapareceu. Temos dois erros, mas se pudermos corrigi-los, estaremos resolvidos. Estamos progredindo.Na primeira ramificação, agora movemos a
assertparte de trás da atribuição. Para fazer isso, substituímos as ocorrências decountporcount + 1emassert:Observe ainda apenas dois erros.
Agora precisamos extrair o assert do topo do arquivo
if. A maneira mais fácil de fazer isso é com umaifexpressão -.Dafny ainda mostra erros separados para os dois ramos, mas agora todos fazem parte de uma
assertdeclaração novamente, mais progresso.Em seguida, voltamos na atribuição para
grow. Substituímosgrow + {i}nogrowassert.Nós movemos o erro novamente com sucesso.
Poderíamos continuar retrocedendo na
shrinkatribuição, mas como não é relevante para esta afirmação, não importa, então vamos ficar aqui.Neste ponto, eliminamos todas as "coisas imperativas" no problema de verificação e só temos "coisas lógicas" com as quais nos preocupar. Vamos provar esta afirmação.
Primeiro, podemos reescrever a afirmação para retirar
==o arquivoif-then-else. Coloque issoassertacima do anterior.Este é agora o nosso único erro, por isso ainda estamos progredindo. Dafny provará o resto se pudermos provar isso.
Podemos retirar a ocorrência de
counttambém. Coloque esta afirmação acima da anterior.Vamos provar isso com um
calcbloco de ulação. Coloque este bloco acima da afirmação anterior.Temos um loop invariante sobre
count, então vamos substituí-lo em.Ainda apenas um erro, então Dafny concorda com a primeira etapa do nosso cálculo.
Para preencher a lacuna entre a segunda e a terceira linhas, precisamos conectar os conjuntos
SetLessThan(grow + {i}, threshold)eSetLessThan(grow, threshold). Como eles estão conectados? Bem, sei < thresholdentão o primeiro é o último maisi, caso contrário, eles são iguais. Vamos dizer isso.Observe que não há erro no assert no topo! Portanto, Dafny gosta de nossa igualdade definida, mas ainda não pode provar o fato de cardinalidade.
Vamos tentar preencher a lacuna entre a segunda e a terceira linhas puxando o operador de cardinalidade para fora do sinal de mais.
Ah! O erro mudou. Agora, a penúltima e a penúltima linhas são iguais, mas as duas linhas do meio não. O que da?
Bem, a cardinalidade de uma união nem sempre é a soma das cardinalidades. Isso só é verdade se eles forem disjuntos. Esses conjuntos são disjuntos? Sim! Por que? porque saímos
ido psiquiatra egrowsomosshrinkdisjuntos. Mas Dafny não pode dizer porque precisamos de outro loop invariante.Em Dafny,
A !! BsignificaAeBsão disjuntos.Adicionamos este loop invariante:
Todos os erros sumiram!!! Wooo. Nós celebramos.
E agora nós limpamos. Adicionamos uma tonelada de afirmações desnecessárias que agora podemos excluir e descobrir o que realmente importa. Apenas tente excluir coisas e ver o que ainda verifica.
Acontece que as únicas coisas que importam são o loop invariante e um
assert. Aqui está o loop final