Доказательство правильности программы

Question

Функция рекурсивно находит и возвращает наименьший элемент из массива, который имеет целочисленные элементы

Min(A, b, e)
if (b=e)
     return A[b]
m = (b+e)/2 // floor is taken
x = Min(A, b, m)
y = Min(A, m +1, e)
If(x < y)
     return x
else
     return y

Моим предварительным условием является то, что b и e являются целыми числами больше нуля

Мое условие публикации: вернуть целое число x или y (не уверен в этом)

Итак, как я могу доказать, что это правильно, показав, что до и после условия являются индуктивными

Извините за формат, новый в этом.

Answer 1

Доказательство: доказательство математической индукцией.

Базовый случай: рассмотрим случай, когда b=e. Мы смотрим на часть списка с размером 1; минимальный элемент списка с одним элементом - это один элемент списка, который в этом случае возвращает алгоритм.

Индукционная гипотеза: теперь предположим, что алгоритм правильно возвращает минимальный элемент для всех списков размером до k включительно. Для доказательства: возвращает минимальное значение для списков размером до k+1.

Шаг индукции: мы имеем e = b + k + 1 и хотим показать, что мы возвращаем минимальный элемент. Мы знаем, что m будет равно (e+b)/2 = (2b+k+1)/2 = b+(k+1)/2. Это разделит список размера k + 1 на две части размера floor((k+1)/2) и cieling((k+1)/2). Оба они меньше или равны k для всех значений k больше нуля (наш базовый случай начинается с k=1, так что это означает, что мы хороши). Таким образом, по предположению индукции, x является минимальным значением нижней половины списка, а y является минимальным значением верхней половины списка. Алгоритм возвращает x, если он меньше y, и y в противном случае. Поскольку минимальное значение в списке A должно встречаться в одной половине списка, и мы возвращаем меньшее из минимальных значений из двух половинок A, мы знаем, что возвращаем минимальное значение в A. Это завершает доказательство.