Dafny tem as seguintes maneiras de declarar tipos que suportam igualdade.
T(==)
Mas existe uma maneira de especificar o tipo que suporta ordenação ( <, <=, >, >=) etc.?
Estou tentando escrever um método de "busca linear" em Dafny. O método pega uma função fque mapeia números naturais para valores booleanos e sabe-se que existe um primeiro número npara o qual f(n) == True. Então o método garante que esse né o valor retornado.
Naturalmente npode ser arbitrariamente grande a partir dessa especificação, e somente sob a suposição de uma quantidade arbitrária de energia disponível pode-se garantir que o programa será capaz de encontrar n.
Isso é algo que não pode ser expresso em Dafny?
Aqui está o que eu tentei
method linear_search(f: nat -> bool) returns (x: nat)
requires exists n : nat :: f(n)
ensures f(x) && forall i : nat :: i < x ==> !f(i)
{
x := 0;
while !f(x)
{
x := x + 1;
}
}
O verificador falha com: "não é possível provar o término; tente fornecer uma cláusula de diminuição para o loop"
Uma busca linear limitada alternativa é verificada sem problemas.
method bounded_linear_search(f: nat -> bool, max_bound: nat) returns (x: nat)
requires exists n : nat :: n <= max_bound && f(n)
ensures f(x) && forall i : nat :: i < x ==> !f(i)
{
x := 0;
while !f(x) && x <= max_bound
decreases max_bound - x
invariant forall i : nat :: i < x ==> !f(i)
{
x := x + 1;
}
}
Como podemos provar que se para todas as entradas fe gretornar a mesma saída, então as duas funções são equivalentes?
lemma func_ext(f: int -> int, g: int -> int)
requires forall x :: f(x) == g(x)
ensures f == g
Eu diria que isso é um axioma, mas não funciona. A extensionalidade da função não é verdadeira em Dafny?
lemma blah(p:nat->bool, xs:seq<nat>)
requires forall t | t in xs :: p(t)
ensures forall i | 0 <= i < |xs| :: p(xs[i]) {}
lemma zero_is_zero(xs:seq<nat>)
requires forall x | x in xs :: (x == 0)
ensures forall k | 0 <= k < |xs| :: (xs[k] == 0) {
// blah(x => x == 0, xs);
}
Então, estou testando a versão dafny 4.4.0e estou lutando para entender o trecho de código acima. Corresponde aproximadamente a um dos dois lemas relevantes aqui ; mas eu os simplifiquei um pouco.
Meu entendimento é que o zero_is_zerolema é basicamente uma generalização do blahlema (sendo a propriedade pneste caso x => x == 0). Então, na verdade, deveria ser mais fácil verificar automaticamente o zero_is_zero. Eu esperava que um elemento da sequência fosse considerado indistinguível do mesmo elemento quando acessado por meio de um índice.
Na prática, acontece que isso blahé verificado automaticamente (ou seja, não preciso fazer nada no corpo do lema). Mas zero_is_zerotenho que invocar explicitamente blahpara mostrar que isso realmente vale para a propriedade x => x == 0e, de repente, não é mais um problema.
Qual é a explicação para isso?
Obrigado!
Tenho uma série de limpos em Dafny que desejo percorrer de maneira não linear. Para elucidar o problema: Considere um array tal que (ignore a sintaxe por enquanto):
var links : array<nat>;
links := [1,2,5,4,0,3];
Num determinado índice 'i', links[i]contém o índice do próximo elemento que deve ser considerado. Aqui, vamos i == 2 ==> links[i] == 5. Na próxima iteração, o loop lê o valor no índice 5 que é 3 e assim por diante até links[i] == 0.
Implementei um loop while e alguns predicados que não parecem provar o encerramento.
O primeiro predicado é que cada elemento da lista é único e nenhum elemento é maior que o comprimento do loop. Isso ocorre porque, caso contrário, a matriz se tornará circular. O predicado vem daqui .
forall i, j | 0 <= i < links.Length && 0 <= j < links.Length && i != j :: links[i] != links[j]
O segundo predicado é que existe um elemento na matriz que é 0. Esta é a condição final.
exists q :: 0 <= q < links.Length && links[q] == 0
O loop while itera da seguinte maneira:
qAct = links[0];
while(qAct != 0)
/* invariants and decreases ??? */
{
qAct = links[qAct];
}
O problema aqui é que o qAct realmente não diminui. Para remediar isso, raciocinei que o loop nunca irá iterar mais do que seu comprimento, então tentei:
qAct = links[0];
var i : nat;
i := 0
while(qAct != 0 && i < links.Length)
/* this terminates */
decreases links.Length - i
{
qAct := links[qAct];
i := i + 1;
}
O raciocínio é que, de acordo com o design do array, o número de elementos não pode ser maior que o comprimento do array. Portanto, o loop itera na maioria dos links.Length vezes.
Existe como comprovar a rescisão sem usar "i"? Também tentei definir "i" como uma variável fantasma, mas recebo um erro dizendo "a atribuição a uma variável não fantasma não é permitida neste contexto". em qAct := links[qAct].
Uma prova em papel e caneta com lógica Hoare (e raciocínio simples) é suficiente para mostrar que qAct eventualmente converge para 0 devido ao segundo predicado. Mas Dafny não consegue raciocinar com esse predicado.
A ajuda de pessoas experientes com Dafny é inestimável!
Estou tentando depurar o tempo de verificação variável no Dafny. Tento executar o verifyLogger, mas não obtenho saída.
Estou no Windows (mas ficaria feliz com uma solução Linux)
Defino meu caminho para a versão do Dafny instalada pelo complemento VSCode, assim:
definir caminho=C:\Usuários\carlk.vscode-insiders\extensions\dafny-lang.ide-vscode-3.1.2\out\resources\4.2.0\github\dafny;%caminho%
Eu corro:
dafny verify --verification-time-limit:15 --cores:6 --boogie -randomSeedIterations:10 --boogie -verificationLogger:csv repro1.dfy
mas não vejo nenhuma saída CSV.
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);
}
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.