І так. Знову про доведення. Одне з завдань в кінці глави звучить так
Розгляньте проблему пошуку
Вхідні дані: деяка послідовність з n чисел A = (a1, a1, ... , an) та деяке значення v
Вихідні дані: деякий індекс j, такий, що v = A[j], або спеціальне значення NULL, якщо v не з'являється в A
Напишіть псевдокод для лінійного пошуку, котрий сканує послідовність, шукаючи значення v. Використовуючи інваріянт циклу доведіть правильність алгоритму. Впевніться, що ваш інваріянт циклу задовольняє трьом основним умовам.
Під трьома умовами мається на увазі Initialization, Maintenance та Termination.
Озьдо код
const arr = [31, 41, 59, 26, 41, 58];
function sp(a, v) {
let j = 0;
while(j<a.length) {
if (a[j] === v) {
return j;
}
j++;
}
return null
}
console.log(sp(arr, 0));
Чесно кажучи, всі ці "доведення" я ніколи не розумів. Тому що як тільки я розумію, як працює якийсь алгоритм, то мені це все стає якимось очевидним, і таким, що не потребує ніяких доведень.
Але ось, як я пробую це довести, беручи за приклад доведення алгоритму Сортування вставленням.
▼Приклад доведення для сортування
Initialization. Тут, як я розумію, я повинен показати, що "тримає інваріянт циклу" перед першою ітерацією, коли j = 0. Так воно ніфіга не тримає, і взагалі, як інваріянт циклу може щось тримати, воно ж просто показує, що елементи масиву не змінюються після ітерації циклу!
Maintenance. Тут, як я розумію, я маю показати, що інваріянтність циклу зберігається після ітерації циклу. Так, як з кожною ітерацією ми не змінюємо елементи масиву, інваріянтність циклу зберігається.
Termination. Тут, як я розумію, я повинен розглянути те, що відбувається після закінчення роботи циклу. Умовою зупинки циклу може бути знаходження такого елементу A[j] значення котрого дорівнює змінній v. Тоді цикл зупиняється і повертається значення j. Також цикл зупиняється, коли j дорівнює n (n == A.length) , тому що умова j<A.length не виконається.
Таким чином алгоритм правильний.
Я довів все правильно, чи нє? Що не так? Як зробити, аби було так?
(
