Доказательство правильности типа "разделяй и властвуй"

Question

Предположим, у нас есть метод сортировки:

void DD_sort(int a[], int x, int y, int size_a)
{
   if(x == y){
      return;
   }
   else if(y == x+1){
      if(a[x] > a[y]){
         /* swap the content */
         return;
      }
   }
   else{
      int s = floor((y+1-x)/3);
      DD_sort(a, x, y-s, s);
      DD_sort(a, x+s, y, s);
      DD_sort(a, x, y-s, s);
   }  
}

Какие методы мы можем использовать, чтобы показать, что алгоритм сортировки правильно или неправильно сортирует массив a? Есть ли систематические подходы к этой проблеме? Я понимаю, что это работает в случае size_a == 1 и size_a == 2, но если size_a, скажем, 30, то мы рекурсивно вызываем метод сортировки для фрагмента размером ~2/3 размера. Похоже, что это работает, но я не уверен, как формально показать это.

Answer 1

Вы должны доказать, что эти строки

  DD_sort(a, x, y-s, s);
  DD_sort(a, x+s, y, s);
  DD_sort(a, x, y-s, s);

отсортирует весь массив от x до y, учитывая, что каждый из трех вызовов будет правильно сортировать заданное подмножество массива. Последний из трех вызовов гарантирует, что элементы от x до ys упорядочены. Второй вызов гарантирует, что элементы от ys до y упорядочены. Чтобы сделать вывод, что все элементы упорядочены, вам нужно показать, что элементы от ys до y больше, чем элементы от x до ys.

Это верно, потому что: первый вызов гарантирует, что элементы s большего размера выйдут за пределы индекса yss >= x+s. Таким образом, второй вызов отправит их в конец массива.

Все эти рассуждения верны, если длина массива ровно 3* с. Это остается верным, если s меньше трети длины, на самом деле, если s меньше, отсортированные подмножества больше.