Используйте инвариант цикла, чтобы доказать правильность «расщепляющейся части» в Mergesort - PullRequest
Новая
       8

Используйте инвариант цикла, чтобы доказать правильность «расщепляющейся части» в Mergesort

0 голосов
/ 19 февраля 2019 
def mergesort(U): 

===== SPLITTING PART =====
L = []
R = []
while U != [] and tail(U) != []:  
   L = L + [head(U)]  
   U = tail(U)  
   R = R + [head(U)]  
   U = tail(U)  
L = L + U 
===== SPLITTING PART =====
L = mergesort(L)  
R = mergesort(R)  
mergeFunction()
return

Разделительная часть разделяет U на две половины, L и R, приблизительно равной длины.Однако я не могу придумать ни одного инварианта цикла, чтобы доказать это.Я знаю, что инвариант цикла должен быть истинным перед циклом (инициализация), после каждой итерации (обслуживание) и дает нам интересный результат после завершения цикла (завершение), но я не могу думать о том, который удовлетворяет этим трем условиям.Это не домашняя работа, так как мне не нужны полные доказательства, и я только практикую использование инвариантов цикла, как в CLRS Кормена, чтобы доказать правильность сортировки слиянием.

...