Invariant for Hoare-Logic on RandomSearch

Question

I'm trying to proof the following RandomSeach-Algorithm and to figure out the invariant for the loop.

Since the function randomIndex(..) creates a random number I cannot use an invariant like

𝑠 ≥ 0 ∧ 𝑠 < 𝑖 − 1 ⇒ 𝑓[𝑠] ≠ 𝑣𝑎𝑙𝑢e

. That means, all elements between 0 and i-1, with i is the index of the current checked element, is not the searched element.

So I thought I define a hypothetical sequence r, that contains all elements that have already been compared to the searched value or are going to be compared to the searched value. Thats why it is just a hypothetical sequence, because I actually do not know the elements that are going to be compared to the searched value until they have been realy compared.

That means it applies r.lenght() ≤ runs and in the case the searched element was found

(r[r.lenght()-1] = value) ↔ (r[currentRun] = value).

Then I can define a invariant like:

𝑠 ≥ 0 ∧ 𝑠 < currentRun  ⇒ r[𝑠] ≠ 𝑣𝑎𝑙𝑢e

Can I do this, because the sequence r is not real? It does not feel right. Does anyone have a diffrent idea for an invariant?

The program:

public boolean RandomSearch (int value, int[] f, int runs) {
    int currentRun = 0;
    boolean found = false;
    while (currentRun < runs || !found) {
        int x = randomIndex(0, n-1)
        if (value == f[x]) {
            found = true;
        }
        currentRun = currentRun + 1;
    }//end while
    return found;
}//end RandomSearch

Answer 1

Ok,

I use following invariant

currentRun <= runs & f.length > 0

Than I can proof the algorithm :)