How to find loop invariant from weakest precondition?

Question

Consider this code:

Precondition:

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; }

Looking at this code, it's basically searching for a key starting from the end of the array. What I am trying to find is a loop invariant using the Weakest Precondition, and prove it. However, I'm unsure if my weakest precondition is correct.I think the weakest precondition (and precondition) is nothing because nothing seems to have to be true before calling this function, maybe except a!=null. So if I have no weakest precondition or a != null(assuming this is the wp) how can I get a loop invariant? I can't see how you can derive a loop invariant from this. Aside from all this, I think the loop invariant is ∀i,j, j > i ∧ a[j] ≠ key but I didn't use the weakest precondition to come up with this loop invariant at all. Any ideas on what I am doing wrong here?