Perguntas[dafny](coding)

Esta é uma pergunta semelhante, mas não consegui mapeá-la para o meu caso de uso. Basicamente, quero usar Dafny para provar uma afirmação básica com quantificadores aninhados (para todo X existe Y) em lógica de primeira ordem sobre inteiros. A afirmação específica que escolhi é que a absfunção é sobrejetiva em inteiros não negativos. Aqui está um trecho de código minimizado:

function abs(x: int): int {
    if x > 0 then x else -x
}

// Passes the verifier
lemma AbsSurjectiveFor(y: int)
requires y >= 0
ensures exists x :: abs(x) == y
{
    assert abs(y) == y;
}

// Error in this lemma (universal generalization of the above)
lemma AbsSurjective()
ensures forall y: int :: y >= 0 ==> exists x :: abs(x) == y
{
    // Forall introduction syntax
    forall y: int | y >= 0
    ensures exists x :: abs(x) == y
    {
        AbsSurjectiveFor(y);
    }
}

Pergunta

Qual é a sintaxe correta para que o segundo lema seja aprovado?

De forma mais geral, estou procurando a sintaxe para as regras de introdução e eliminação para todos, caso eu queira fazer uma demonstração manualmente (por exemplo, em um estilo de dedução natural). Suspeito que estou fazendo algo muito "óbvio" errado, mas não consegui encontrar a sintaxe correta no manual de referência.

Notas

Dafny prova o primeiro lema (fácil, não é necessária a introdução de um quantificador), mas falha no segundo lema, embora eu tenha correspondido exatamente à sintaxe dada na resposta de Rustan , que sugere usar um bloco de instruções forall dentro do lema.

Uma dica do que pode estar errado é que estou recebendo avisos por usar quantificadores sem gatilhos. No entanto, não me importo muito com os gatilhos, pois minha intenção é provar as instruções forall/exists manualmente. Não tenho certeza se existe uma maneira de simplesmente desativar os gatilhos ou dizer ao Dafny para não instanciar os quantificadores, a menos que eu diga para ele fazer isso.

Saída de dafny verify:

$ dafny verify fol-minimal.dfy 
fol-minimal.dfy(15,8): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
   |
15 | ensures forall y: int :: y >= 0 ==> exists x :: abs(x) == y
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

fol-minimal.dfy(18,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
   |
18 |     forall y: int | y >= 0
   |     ^^^^^^^^^^^^^^^^^^^^^^

fol-minimal.dfy(16,0): Error: a postcondition could not be proved on this return path
   |
16 | {
   | ^

fol-minimal.dfy(15,8): Related location: this is the postcondition that could not be proved
   |
15 | ensures forall y: int :: y >= 0 ==> exists x :: abs(x) == y
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

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.