Инвариант для Hoare-Logic в RandomSearch

Я пытаюсь доказать следующий алгоритм RandomSeach-Algorithm и выяснить инвариант для цикла.

Поскольку функция randomIndex(..) создает случайное число, я не могу использовать такой инвариант, как

???? ≥ 0 ∧ ???? < ???? − 1 ⇒ ????[????] ≠ ????????????????e

. Это означает, что все элементы между 0 и i-1, где i является индексом текущего проверяемого элемента, не являются искомым элементом.

Поэтому я решил определить гипотетическую последовательность r, содержащую все элементы, которые уже сравнивались с искомым значением или будут сравниваться с искомым значением. Вот почему это всего лишь гипотетическая последовательность, потому что я на самом деле не знаю элементы, которые будут сравниваться с искомым значением, пока они не будут действительно сравнены.

Это означает, что он применяет r.lenght() ≤ runs и в случае, если искомый элемент был найден

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

Затем я могу определить инвариант, например:

???? ≥ 0 ∧ ???? < currentRun  ⇒ r[????] ≠ ????????????????e

Могу ли я это сделать, потому что последовательность r ненастоящая? Это неправильно. У кого-нибудь есть другая идея для инварианта?

Программа:

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