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!