“Гарантія коректності” як методика обходу багів


Дізнайтесь більше про нові кар'єрні можливості в EchoUA. Цікаві проекти, ринкова оплата, гарний колектив. Надсилайте резюме та приєднуйтеся до нас.

Вам коли-небудь доводилося гарантувати коректність виконання своєї програми? Насправді це великий об’єм роботи, який не завжди можливо виконати. У самих доказах можуть бути помилки, про це говориться і в мудрості, узятій з Дао програмування:

Навіть у ідеальних програмах є помилки.

Зіткнувшись з цими труднощами, Саймон Пейтон-Джонс запропонував ось такий вихід:

“Я думаю, буде досить продуктивно відразу позначити, що в програмі обов’язково повинно або не повинно статися. Наприклад, “це дерево завжди має бути збалансоване”. Чи “ця функція завжди повинна повертати число більше нуля”. Можливо, в майбутньому знайдеться простіший спосіб гарантувати правильну роботу усієї програми, але поки що його немає”.

По суті, ми досі не можемо гарантувати відсутність помилок. Хороші програмісти завжди задаються питанням, як і чому працює кожна ділянка коду. Вони відразу ж намагаються відтворити ситуацію, де щось йде не так. Передбачити все виходить не завжди – і коли щось все ж йде не так, програміст відразу ж намагається придумати спосіб більше не припускатися цієї помилки.

Це основна теза практичних доказів. І до речі: хороші програмісти відразу намагаються запевнитися в тому, що все завжди працюватиме як належить, але в одному вони іноді промахуються. Вони не діляться своїми міркуваннями з іншими. Адже доказ повинен пройти перевірку не лише його творцем – важливо перевірити, чи вірно воно, переказавши свої думки комусь ще.

До речі, ви вже могли чути цю тезу: деякі програмісти ставлять на стіл фігурку, іграшку – будь-який предмет, з яким можна обговорити проблему. Саме в ході пояснення проблеми комусь іншому ми найчастіше і бачимо усі виходи і недоліки. Тому не бійтеся виглядати безглуздо і не соромтеся обговорювати з ким-небудь свої ідеї.

Ось вам приклад ситуації, коли необхідно бути упевненим хоч в чомусь: багатопоточність. Це складно і важко передбачуване – не можна покрити юніт-тестами увесь код, надто багато всього залежить від випадковостей. Тому для того, щоб понизити вірогідність помилок, треба спроєктувати все так, щоб у вас було точне логічне обгрунтування того, що помилка не може виникнути.

Ось цей код може упевнено заявити про себе: тут не можуть виникнути умови гонки (race conditions) і дедлоки. Зверніть увагу на те, як саме програміст розв’язав цю проблему :

//------------------------------------------// Усі виклики до 'slicedMelon' повинні// знаходитися в цій секції. Необхідно,// щоб ви могли візуально переконатися в тому, що// у кожного LOCK відповідаю йому UNLOCK.// Цей м'ютекс не можна використати у іншому місці.
//------------------------------------------//// Немає race conditions: ця змінна використовується тільки з мьютексом// Немає дедлоков: умову Кофмана №4//FUNCTION (getResetSlicedMelon,' LOCK (slicedMutex) movl_slicedMelonLocation (%rip), %r12d movl $- 1,_slicedMelonLocation (%rip) UNLOCK (slicedMutex) movl %r12d, %eax') //'// Зберігає значення в slicedMelon// Немає race conditions: для доступу потрібний м'ютекс// Немає дедлоків: ланцюжків очікувань тут немає//FUNCTION (putSlicedMelon,' movl %edi, %r12d LOCK (slicedMutex) movl %r12d,_slicedMelonLocation (%rip) UNLOCK (slicedMutex)')

Про умови Кофмана можна почитати тут.

Можна зробити і простіше. Наприклад, як говорить Кен Томпсон: “У мого коду є одна відмінна риса: він простий, уривистий і короткий. Так його може прочитати будь-яка людина”.

Так що цей приклад насправді можна поліпшити: наприклад, автоматизувати розблокування за допомогою макросу, використати мову або бібліотеку, що підтримують більше високорівневе управління потоками.

В даному прикладі програміст вирішив, що для роботи його коду важливе, щоб в кожен момент часу був відкритий тільки один клапан. Уся логіка знаходиться в одному місці, а для майбутніх програмістів передбачені коментарі, що пояснюють, чому все зроблено саме так.

//-----------------------------------------------// - Valve guard -// Уся логіка управління клапанами знаходиться тут.// Клапани управляються тільки і тільки цими функціями.//-----------------------------------------------//// Відкриває лівий клапан, тільки якщо закритий правий// Повертає true, якщо клапан був відкритий//FUNCTION (openLeftValve,' movl $ 0, rv ifEqual ($ 0,_rightValveOpen (%rip), 'movl $ 1,_leftValveOpen (%rip) movl $ 1, rv hardwareOpen (left) ')') //// Відкриває правий клапан, тільки якщо закритий лівий// Повертає true, якщо клапан був відкритий//FUNCTION (openRightValve,' movl $ 0, rv ifEqual ( $ 0,_leftValveOpen (%rip), 'movl $ 1,_rightValveOpen (%rip) movl $ 1, rv hardwareOpen (right) ')')

Звичайно, і цей приклад не досконалий. Що робитиме hardwareOpen () при виникненні помилки? Розуміння того, які виклики відбуваються в кожному з випадків, обов’язково при написанні коду, що гарантує відсутність певних помилок.

Каскадний код – місце, в якому треба бути особливо уважним. Також будьте гранично обережні при роботі з отриманими від користувача значеннями: вони можуть обрушити усю програму незалежно від використовуваної мови, а звичайним тестуванням виловити пов’язані з введенням помилки дуже складно.

Інакше кажучи, почніть думати про те, як зробити ваш код безпечніше і забезпечити правильну роботу його частин – так ви зменшите кількість багов і зробите крок на шляху до дзену, звичайно ж.

Трохи первинників з цієї статті (приклади написані на M4, досить рідкісній мові).

Джерело: блог Кейт Томпсон

Київ, Харків, Одеса, Дніпро, Запоріжжя, Кривий Ріг, Вінниця, Херсон, Черкаси, Житомир, Хмельницький, Чернівці, Рівне, Івано-Франківськ, Кременчук, Тернопіль, Луцьк, Ужгород, Кам'янець-Подільський, Стрий - за статистикою саме з цих міст програмісти найбільше переїжджають працювати до Львова. А Ви розглядаєте relocate?


Залишити відповідь

Ваша e-mail адреса не оприлюднюватиметься. Обов’язкові поля позначені *