How to find loop invariant from weakest precondition?

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?

I'm only familiar with elementary hoare logic, which does not account for returns/exits, which must be mimicked by booleans. So let's rewrite your program to do just that. In fact, it becomes easier to understand once we do so!

i ≔ N - 1 ;
found ≔ a[i] ≈ key;
while ¬found ∧ 0 ≤ i-1:
i ≔ i - 1;
found ≔ a[i] ≈ key;

Where we define

$$N : a.length$$

Notice that we have 0 ≤ i - 1 instead of 0 ≤ i since after the decrement i ≔ i - 1 the look-up a[i] in the next statement might not be well-defined. So the loop guard ensures that the decrement is still non-negative and so the look-up is well defined. In particular, look at case i ≈ 1; then 0 ≤ 0 ≈ 1 - 1 ≈ i - 1 and the loop decreases i to 0 and the look-up is defined; afterwards the test 0 ≤ 0 - 1 fails and the loop terminates.

Now your postcondition speaks of the return value, which is essentially just i, so let's simplify that to obtain

$$R : 0 ≤ i < N ⇒ a[i] ≈ key$$

Now the postcondition ought to follow from the negation of the loop guard and the loop invariant: so let's take the invariant to be

$$P : i < N ∧ (found ≡ a[i] ≈ key) % \text{ (we always have i < N and found is true iff a[i] ≈ key)}$$

then after the loop we have the post condition can be seen:

after-loop we have the loop guard fails and the invaraint still holds
≡⟨ foramlise ⟩
(found ∨ i-1 < 0) ∧ (i < N ∧ (found ≡ a[i] ≈ key))
⇒⟨ substitution ⟩
(a[i] ≈ key ∨ i-1 < 0) ∧ i < N
⇒⟨ weakening: A ∨ B ⇒ A ∨ B ∨ C ⟩
(a[i] ≈ key ∨ i-1 < 0 ∨ i < 0) ∧ i < N
≡⟨ arithmetic ⟩
(a[i] ≈ key ∨ i < 0) ∧ i < N
≡⟨ implication ⟩
(0 ≤ i ⇒ a[i] ≈ key) ∧ i < N
⇒⟨ weakening ⟩
0 ≤ i < N ⇒ a[i] ≈ key

and that's the post-condition!

For ease of reference, let the guard be denoted by B; i.e.,

$$B : ¬ found ∧ 0 ≤ i - 1$$

We still haven't actually proved that P is an invaraint: ie that it does not vary with the changes that occur in the loop body and that it is initally true i.e. we need to show

$$\{ ? \} i ≔ N - 1 ; found ≔ a[i] ≈ key \{P\}$$ and $$\{P ∧ B\} i ≔ i - 1 ; found ≔ a[i] ≈ key \{P\}$$

Initialisation is seen as follows: the wp for assignment tells us: $$wp(Q , v ≔ e) = e \text{ well-defined } ∧ Q[e / v]$$, so applying twice means we need to have the following as pre-condition:

wp(P , i ≔ N - 1 ; found ≔ a[i] ≈ key)
≡⟨ sequence rule ⟩
wp( wp(P , found ≔ a[i] ≈ key) , i ≔ N - 1)
≡⟨ assignment rule ⟩
wp( a[i] well-defined ∧ P[ a[i] ≈ key / found ] , i ≔ N - 1)
≡⟨ definitions ⟩
wp( 0 ≤ i < N ∧ i < N ∧ (a[i] ≈ key ≡ a[i] ≈ key) , i ≔ N - 1)
≡⟨ equivalence ⟩
wp( 0 ≤ i < N , i ≔ N - 1)
≡⟨ assignment rule ⟩
0 ≤ N-1 < N
≡⟨ arithmetic ⟩
1 ≤ N

So the precondition is that the array is non-empty and in-particular is non-null (the well-definedness condition that you mentioned).

For the invariance part we need to show

{P ∧ B}  i ≔ i - 1 ; found ≔ a[i] ≈ key {P}
≡⟨ assignment rule ⟩
{P ∧ B}  i ≔ i - 1 {0 ≤ i < N ∧ (found ≔ a[i] ≈ key ≡ a[i] ≈ key)}
≡⟨ reflexivitivy of equivalence ⟩
{P ∧ B}  i ≔ i - 1 {0 ≤ i < N }
≡⟨ assignment rule ⟩
P ∧ B ⇒ 0 ≤ i - 1 < N
≡⟨ definitions ⟩
true

Sweet!

So the program now has annotations:

{ 1 ≤ N } // array is non-empty
i ≔ N - 1 ;
found ≔ a[i] ≈ key;
{invariant P }
while !found ∧ 0 ≤ i - 1:
i ≔ i - 1;
found ≔ a[i] ≈ key;
{ R }

We've only shown "partial correctness", for complete correctness we must prove termination. In particular, we need to find a bound function bf that is initially positive and is decreased by the loop body: want bf such that for any constant t,

{ bf = t }   i ≔ i - 1; found ≔ a[i] ≈ key { bf < t }

Since during the loop body we always have P ∧ B and so namely 0 ≤ i - 1, let's take the bound to be

$$bf : i$$

Now since $B ⇒ 0 ≤ i-1 ⇒ 1 < i ⇒ 0 < bf$ we have that bf is initially positive. (One might be tempted to try N-i as bound but that fails since the loop decreases i which means that N-i increases!) It remains to check that it is decreasing: for any t, we have

{ bf = t }   i ≔ i - 1; found ≔ a[i] ≈ key { bf < t }
≡⟨ assignment rule ; bf does not mention varaible found ⟩
{ bf = t }   i ≔ i - 1 { bf < t }
≡⟨ assigment rule ⟩
bf = t ⇒ bf[ i-1 / i] < t
≡⟨ definitions ⟩
i = t ⇒ i - 1 < t
≡⟨ arithmetic ⟩
true

Alright! That was pretty fun!

One final note, if you write this, say in Python, or another language that supports parallel assignment, you can make the program even more succinct!

i, found ≔ N - 1 , a[i] ≈ key;
while ¬found ∧ 0 ≤ i-1:
i, found ≔ i - 1, a[i] ≈ key

Enjoy!