Come trovare loop invariante dal presupposto più debole?

Question

Considera questo codice:

Precondizionismo:

Postcondition: rv == i <==> ∃i, 0 ≤ i ≤ a.length-1, a[i] == key

function Find(Array<int> a, int key) returns (int i) { i = a.length -1; while i ≥ 0 { if a[i] == key {return;} i = i - 1 } return -1; }

Guardando questo codice, è fondamentalmente alla ricerca di una chiave a partire dalla fine dell'array. Quello che sto cercando di trovare è un loop invariante usando il presupposto più debole e dimostrarlo. Tuttavia, non sono sicuro se il mio preliminare più debole sia corretto. Penso che il preliminare (e la preliminare) più debole non sia nulla perché nulla sembra essere vero prima di chiamare questa funzione, forse tranne a!=null. Quindi se non ho un preliminare più debole o a != null(Supponendo che questo sia il WP) Come posso ottenere un loop invariante? Non riesco a vedere come puoi derivare un loop invariante da questo. A parte questo, penso che l'invariante loop sia ∀i,j, j > i ∧ a[j] ≠ key Ma non ho usato il presupposto più debole per elaborare questo loop invariante. Qualche idea su cosa sto facendo di sbagliato qui?