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

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 

Моя предпосылка: б и е представляют собой целые числа больше нуля

Мой пост условие: возвращает целое число х или у (не уверен, что об этом)

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

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

Answer 1

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

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

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

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