Как доказать правильность рекурсивного алгоритма?

Question

private static void swap(char[] str, int i, int j){ 
    char tmp = str[i]; 
    str[i] = str[j]; 
    str[j] = tmp; 
} 

public static void permute(String str){ 
    permute(str.toCharArray(), 0, str.length()); 
} 

private static void permute(char[] str, int low, int high){ 
    if(low == high){ 
    System.out.println(str); 
    } else { 
    for(int i = low; i < high; i++){ 
     swap(str, low, i); 
     permute(str, low+1, high); 
     swap(str, low, i); 
    } 
    } 
} 

Я реализовал рекурсивный метод для перестановки строк. Но у меня возник вопрос: как доказать правильность этого кода, используя индукцию? Я действительно понятия не имел.

Answer 1

Сначала вы должны конкретно сказать, что вы имеете в виду правильности (то есть, спецификация, против которого вы хотите проверить свой код, см также https://stackoverflow.com/a/16630693/476803). Давайте предположим, что правильность здесь означает

Каждый выход permute перестановка заданной строки.

Тогда у нас есть выбор, по которому натуральное число для индукции. Для рекурсивной функции permute у нас есть выбор между low или high или их комбинацией.

При чтении реализации становится очевидным, что существует префикс выходной строки, элементы которой не изменяются. Кроме того, длина этого префикса увеличивается во время рекурсии, и, таким образом, оставшийся суффикс, длина которого составляет high - low, уменьшается. Итак, давайте сделаем индукцию на high - low (в предположении, что low <= high, что является разумным с начала, мы используем 0 для низкого и длины некоторой строки для high, а рекурсия останавливается, как только low == high). То есть, мы показываем

Факт: Каждый выход permute(str, low, high) перестановка последних high - low символов в str.

• Базовый вариант: Предположим high - low = 0. Тогда утверждение пусто, так как оно должно удерживаться для последних 0 символов (т. Е. Ни для одного).

• Шаг: Предположим, что high - low = n + 1. Кроме того, поскольку гипотеза индукции (IH), мы можем предположить, что утверждение верно для n. От high - low = n + 1 у нас есть, что high - (low + 1) = n (начиная с high должно быть строго больше low для high - low = n + 1 для хранения). Таким образом, по IH каждый вывод permute(str, low+1, high) является перестановкой последних high - (low + 1) символов str.

  Теперь наступает момент, когда мы действительно должны что-то доказывать. А именно, что путем замены, в выходе, генерируемый permute(str, low+1, high), в low ей характер str с помощью любого символа после low (до high), мы генерируем перестановку символов между low и high. Этот шаг (который я пропустил здесь, так как я просто хотел продемонстрировать, как вы могли в принципе использовать индукцию) завершает доказательство.

Наконец, инстанцирование вышеуказанной Факта с 0 для low и str.length для high мы имеем, что каждый выход нерекурсивно permute перестановка str.

Примечание: Приведенное доказательство показывает только, что каждый выход является перестановка. Тем не менее, было бы также интересно узнать, что на самом деле напечатаны все перестановки.