1

Тема: Доведення правильності алгоритму на прикладі сортування включенням

По-перше я не зовсім розумію термін "інваріант циклу", або loop invariant.
1) Якщо у нас є масив A, що мість n елементів, і поточний елемент має індекс j, то в книжці пишуть, що "інваріантом циклу" зветься те, що елементи від початку масиву до A(j-1) є тими самими елементами, котрі й були в цьому масиві на початку сортування, але тепер вони відсортованні.
Ось ця властивість і є інваріантом циклу, чи що?

2) Одна з властивостей правильності алгоритму в межах інваріанту циклу зветься Termination, або припинення. Ось, що пишеться в книзі
https://cdn.discordapp.com/attachments/333936584481177600/389021741055475714/unknown.png
Як це взагалі можливо? В нашому масиві ж всього n елементів, тоді якого дідька воно каже, що j має бути рівним n+1?

тут спілкуються українці, про політику, і інше (серед них є програмісти, але дуже мало, тому не заходьте туди лише з питаннями про програмування)
https://discord.gg/Zk29v4P

2

Re: Доведення правильності алгоритму на прикладі сортування включенням

по другому питанню зрозумів.
Ми ж спочатку інкрементуємо j, а потім перевіряємо умову. Тому воно й буде дорівнювати n+1

тут спілкуються українці, про політику, і інше (серед них є програмісти, але дуже мало, тому не заходьте туди лише з питаннями про програмування)
https://discord.gg/Zk29v4P
Подякували: koala1

3

Re: Доведення правильності алгоритму на прикладі сортування включенням

І так. Знову про доведення. Одне з завдань в кінці глави звучить так

Розгляньте проблему пошуку
Вхідні дані: деяка послідовність з 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));

Чесно кажучи, всі ці "доведення" я ніколи не розумів. Тому що як тільки я розумію, як працює якийсь алгоритм, то мені це все стає якимось очевидним, і таким, що не потребує ніяких доведень.
Але ось, як я пробую це довести, беручи за приклад доведення алгоритму Сортування вставленням.

Приклад доведення для сортування

https://cdn.discordapp.com/attachments/333936584481177600/389057456497491989/unknown.png

Initialization. Тут, як я розумію, я повинен показати, що "тримає інваріянт циклу" перед першою ітерацією, коли j = 0. Так воно ніфіга не тримає, і взагалі, як інваріянт циклу може щось тримати, воно ж просто показує, що елементи масиву не змінюються після ітерації циклу!

Maintenance. Тут, як я розумію, я маю показати, що інваріянтність циклу зберігається після ітерації циклу. Так, як з кожною ітерацією ми не змінюємо елементи масиву, інваріянтність циклу зберігається.

Termination. Тут, як я розумію, я повинен розглянути те, що відбувається після закінчення роботи циклу. Умовою зупинки циклу може бути знаходження такого елементу A[j] значення котрого дорівнює змінній v. Тоді цикл зупиняється і повертається значення j. Також цикл зупиняється, коли j дорівнює n (n == A.length) , тому що умова j<A.length не виконається.
Таким чином алгоритм правильний.

Я довів все правильно, чи нє? Що не так? Як зробити, аби було так?

тут спілкуються українці, про політику, і інше (серед них є програмісти, але дуже мало, тому не заходьте туди лише з питаннями про програмування)
https://discord.gg/Zk29v4P

4

Re: Доведення правильності алгоритму на прикладі сортування включенням

А який у вас інваріант? Тут, я так розумію, інваріантом буде "∀ i, 0<=i<j => A[ i ]!=v". Ну а доказ тут, звісно, елементарний, всі три кроки самоочевидні.

5

Re: Доведення правильності алгоритму на прикладі сортування включенням

koala написав:

А який у вас інваріант? Тут, я так розумію, інваріантом буде "∀ i, 0<=i<j => A[ i ]!=v". Ну а доказ тут, звісно, елементарний, всі три кроки самоочевидні.

не перекладається =((
https://cdn.discordapp.com/attachments/333936584481177600/389369786347290624/unknown.png
що то значе?

тут спілкуються українці, про політику, і інше (серед них є програмісти, але дуже мало, тому не заходьте туди лише з питаннями про програмування)
https://discord.gg/Zk29v4P

6 Востаннє редагувалося koala (10.12.2017 14:46:32)

Re: Доведення правильності алгоритму на прикладі сортування включенням

Простою мовою - "пройдені елементи не містять v". А я написав "для будь-якого i від 0 до j (не включно) A[ i ] не дорівнює v", тобто те саме, але коротше і точніше. Ця умова має виконуватися у будь-який момент.

7

Re: Доведення правильності алгоритму на прикладі сортування включенням

а що означає i ? в коді ж його нема. Чи це ви маєте на увазі, що j - кількість елементів, а i - індекс елементу, котрий рухається від 0 до j ?
І чому ви кажете лише про випадок, коли v ∉ A, і не зачіпаєте випадок, коли v таки міститься в A ?

тут спілкуються українці, про політику, і інше (серед них є програмісти, але дуже мало, тому не заходьте туди лише з питаннями про програмування)
https://discord.gg/Zk29v4P

8

Re: Доведення правильності алгоритму на прикладі сортування включенням

i не "рухається", це не частина алгоритму, це частина опису інваріанта.
А якщо v в A, то відбувається вихід з циклу, і під час цього теж підтримується інваріант. Це ви і маєте перевірити під час доказу.

Подякували: leofun011

9

Re: Доведення правильності алгоритму на прикладі сортування включенням

ееее, так а що з себе представляє той інваріант, бо чогось не розумію...

тут спілкуються українці, про політику, і інше (серед них є програмісти, але дуже мало, тому не заходьте туди лише з питаннями про програмування)
https://discord.gg/Zk29v4P

10 Востаннє редагувалося koala (10.12.2017 21:01:00)

Re: Доведення правильності алгоритму на прикладі сортування включенням

Інваріант - це щось, що лишається незмінним. Тут ідея в тому, щоб придумати певну властивість - наприклад, впорядкованість всіх елементів в певному діапазоні, або те, що жоден з них не дорівнює значенню v, і довести, що ця властивість присутня перед циклом, після кожної ітерації і при завершенні роботи коду. Власне, для нас головне останнє; але щоб його довести, треба спертися на попередні твердження. З Initialization випливає Maintenance, а з Maintenance - Termination.

Подякували: FakiNyan1

11

Re: Доведення правильності алгоритму на прикладі сортування включенням

То це типу мона довести, що елемент постійно є в масиві, або те, що елементу постійно немає в масиві? -_-

тут спілкуються українці, про політику, і інше (серед них є програмісти, але дуже мало, тому не заходьте туди лише з питаннями про програмування)
https://discord.gg/Zk29v4P

12

Re: Доведення правильності алгоритму на прикладі сортування включенням

FakiNyan написав:

То це типу мона довести, що елемент постійно є в масиві, або те, що елементу постійно немає в масиві? -_-

ЯК? О_о

13

Re: Доведення правильності алгоритму на прикладі сортування включенням

koala написав:
FakiNyan написав:

То це типу мона довести, що елемент постійно є в масиві, або те, що елементу постійно немає в масиві? -_-

ЯК? О_о

що саме як?
a) як довести, що елементу завжди нема в масиві
б) як довести, що елемент завжди є в масиві
c) свій варіянт

тут спілкуються українці, про політику, і інше (серед них є програмісти, але дуже мало, тому не заходьте туди лише з питаннями про програмування)
https://discord.gg/Zk29v4P

14

Re: Доведення правильності алгоритму на прикладі сортування включенням

FakiNyan написав:
koala написав:
FakiNyan написав:

То це типу мона довести, що елемент постійно є в масиві, або те, що елементу постійно немає в масиві? -_-

ЯК? О_о

що саме як?
a) як довести, що елементу завжди нема в масиві
б) як довести, що елемент завжди є в масиві
c) свій варіянт

А чи б, на ваш розсуд. Очевидно, що жодного не можна довести без масиву.

15

Re: Доведення правильності алгоритму на прикладі сортування включенням

koala написав:
FakiNyan написав:
koala написав:

ЯК? О_о

що саме як?
a) як довести, що елементу завжди нема в масиві
б) як довести, що елемент завжди є в масиві
c) свій варіянт

А чи б, на ваш розсуд. Очевидно, що жодного не можна довести без масиву.

оце ж я так само думаю. Без конкретного масиву, про котрий відомо, що в ньому або є v, або немає - довести правильну роботу алгоритму неможливо. Тоді якого дідька це завдання є в книзі, що саме вони хотіли, аби люди доводили?

тут спілкуються українці, про політику, і інше (серед них є програмісти, але дуже мало, тому не заходьте туди лише з питаннями про програмування)
https://discord.gg/Zk29v4P

16

Re: Доведення правильності алгоритму на прикладі сортування включенням

Так, ви заплуталися. Алгоритм має перевіряти наявність елементу в масиві - а доводити треба, що він це робить коректно, а не наявність/відсутність. Ми на рівень вище, контролюємо не масив, а сам алгоритм, так зрозуміло?

17

Re: Доведення правильності алгоритму на прикладі сортування включенням

Нууу, окай. І як застосувати інваріантність для вирішення цього завдання?

тут спілкуються українці, про політику, і інше (серед них є програмісти, але дуже мало, тому не заходьте туди лише з питаннями про програмування)
https://discord.gg/Zk29v4P

18

Re: Доведення правильності алгоритму на прикладі сортування включенням

погуглірував трохи, кажуть, що

Remember, this is pseudocode and math, not actual code on actual machines. If you assume the notation A[l...u] represents

{ A[i], ∀i i>=l ∧ i <= u }

, then A[0...-1] would represent an empty set. Saying that v is not on the empty set is true, so it holds at the beginning.

що ось це значе?

{ A[i], ∀i i>=l ∧ i <= u }
тут спілкуються українці, про політику, і інше (серед них є програмісти, але дуже мало, тому не заходьте туди лише з питаннями про програмування)
https://discord.gg/Zk29v4P

19

Re: Доведення правильності алгоритму на прикладі сортування включенням

це квантор загальності

∀i

— «для будь-якого i»

∀i i>=l ∧ i <= u

— «для будь-якого i, такого, що i>=l && i <= u»

{ A[i], ∀i i>=l ∧ i <= u }

— «Множина A-ітих для будь-якого i, такого, що i>=l && i <= u»

printf("Nested comments is %s\n", */*/**/"*/"/*"/**/ == '*' ? "OFF" : "ON");
Подякували: 0x9111A, FakiNyan, koala, leofun014

20

Re: Доведення правильності алгоритму на прикладі сортування включенням

ну, здається, я трохи роздуплився з тим доведенням.

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));

Тут виходе, що після ініціалізації, та до початку роботи циклу, розглянутий шматок множини буде A[0...0], тому що j == 0, але якщо розглянути множину A[0...-j], то вона буде дорівнювати A[0...-1], і це ж буде пуста множина, котра не може містити v.
Потім цикл починає перевіряти елемент A[0], тут вже може міститись v, і якщо воно там є, то ми повертаємо j, і переглянути множина буде дорівнювати A[0...j], і так, як більше ми нічо не робимо, то мона сказати, що A[0...j-1] ніколи не містить v, ось це і буде інваріантом.

І так, як до роботи циклу ми маємо A[0...-1], то етап 1, Initialization - доведене.

Далі йде Maintenance. Це я вже показавав на початку цього повідомлення, так, як ми зупиняємо цикл після того, як знаходимо v, то наступна ітерація не відбувається, одже A[0...j-1] не містить v.

Ну і далі йде Termination. У нас стоїть умова j<a.length. І так, як наша множина скінченна, то цикл зупиниться, або коли знайдеться v, або коли j буде дорівнювати a.length. В першому і другому випадку A[0...j-1] не буде містити v.

Як вам таке?

тут спілкуються українці, про політику, і інше (серед них є програмісти, але дуже мало, тому не заходьте туди лише з питаннями про програмування)
https://discord.gg/Zk29v4P
Подякували: koala1