Início / coding / Perguntas / 77480353
Accepted
Drona Nagarajan
Asked: 2023-11-14 19:47:04 +0800 CST

Provar que a travessia não linear termina em Dafny

  • 772

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!

dafny

1 respostas

  1. Best Answer

    Você pode tentar as seguintes definições.

    predicate derangement(s: seq<nat>) {
    forall i :: 0 <= i < |s| ==> s[i] != i
}

predicate permutation(s: seq<nat>) {
    forall i :: 0 <= i < |s| ==> i in s
}

method test(anotherPerm: seq<nat>)
  requires permutation(anotherPerm) && derangement(anotherPerm)
 {
    var tests := [2,0,1];
    var tests2 := [0,1,2];
    assert derangement(tests);
    assert permutation(tests);
    assert permutation(tests2);
    // assert !derangement(tests2); //this will actually not verify despite being true
}

    No final, continuei trabalhando nisso. Consegui obter o seguinte para verificar.

    predicate derangement(s: seq<nat>) {
    forall i :: 0 <= i < |s| ==> s[i] != i
}

predicate permutation(s: seq<nat>) {
    forall i :: 0 <= i < |s| ==> i in s
}

function multisetRange(n: nat): multiset<nat> {
    multiset(seq(n, i => i))
}

predicate distinct<A(==)>(s: seq<A>) {
    forall x,y :: x != y && 0 <= x <= y < |s| ==> s[x] != s[y]
}

method test() {
    var tests := [2,0,1];
    var tests2 := [0,1,2];
    var t4 := seq(3, i => i);
    var test3 := multisetRange(3);
    assert t4 == tests2;
    assert 0 in t4;
    assert 0 in test3;
    assert multiset(tests) == multisetRange(3);
    assert derangement(tests);
    assert permutation(tests);
    assert permutation(tests2);
    // assert !derangement(tests2);
}

method {:timelimit 40} end(links: seq<nat>)
    requires |links| > 0
    requires permutation(links)
    requires derangement(links)
    requires distinct(links)
{
    assume forall x :: x in links ==> 0 <= x < |links|;
    assume forall x :: x in links ==> multiset(links)[x] ==1;
    // assume multiset(links) == multisetRange(|links|);
    var qAct: nat := links[0];
    assert links[0] in links;
    var i : nat := 0;
    ghost var oldIndex := 0;
    ghost var indices: multiset<nat> := multiset{0};
    ghost var visited: multiset<nat> := multiset{};

    while qAct != 0
        invariant 0 <= oldIndex < |links|
        invariant qAct == links[oldIndex]
        invariant oldIndex in indices
        invariant qAct in links
        invariant indices == visited + multiset{0}
        invariant forall x :: x in visited ==> exists k :: 0 <= k < |links| && links[k] == x && k in indices
        invariant qAct !in visited
        invariant 0 <= qAct < |links|
        decreases multiset(links) - visited
    {
        ghost var oldVisit := visited;
        ghost var oldqAct := qAct;
        ghost var oldOldIndex := oldIndex;
        oldIndex := qAct;
        visited := visited + multiset{qAct};
        indices := indices + multiset{qAct};
        assert oldqAct in visited;
        assert forall x :: x in visited ==> exists k :: 0 <= k < |links| && links[k] == x && k in indices by  {
            forall x | x in visited 
                ensures exists k :: 0 <= k < |links| && links[k] == x && k in indices
            {
                if x == oldqAct {
                    assert links[oldOldIndex] == oldqAct;
                    assert exists k :: 0 <= k < |links| && links[k] == x && k in indices;
                }else {
                    assert x in oldVisit;
                    assert exists k :: 0 <= k < |links| && links[k] == x && k in indices;
                }
            }
        }
        qAct := links[qAct];
        i := i + 1;
    }
}

    Idealmente, você deve mover as suposições para o requisito do método ou, melhor ainda, definir lemas que garantam que essas declarações baseadas nos links sejam uma permutação.

    • 1

relate perguntas