Це стаття-переклад . Але перед нею невеликий вступ. Як утворюються зомбі? Кожен потрапляв у ситуацію, коли хочеться підтягнути друга чи колегу до свого рівня, а не виходить. Причому «не виходить» не так у тебе, як у нього: на одній чаші терезів знаходиться нормальна зарплата, завдання і так далі, а на іншій — необхідність думати. Думати неприємно та боляче. Він швидко здається і продовжує писати код, не включаючи мозок. Ти уявляєш, наскільки багато сил потрібно витратити, щоб подолати бар'єр вивченої безпорадності, і просто цього не робиш. Так утворюються зомбі, яких начебто можна вилікувати, але і ніхто цим займатися не стане.
Коли я побачив, що (так-так, той самий товариш із підручників) і робить не доповідь, а сесію запитань-відповідей, я трохи насторожився. Про всяк випадок, Леслі - всесвітньо відомий учений, автор основних робіт у розподілених обчисленнях, а ще ви його можете знати за літерами La в слові LaTeX - Lamport TeX. Другим фактором, що насторожує, є його вимога: кожен, хто прийде, повинен (цілком безкоштовно) заздалегідь прослухати пару його доповідей, придумати по них мінімум одне питання і тільки тоді вже приходити. Вирішив подивитися, що там Лемпорт мовить - і це чудово! Це точно та штука, чарівне посилання-таблетка для лікування зомбятини. Попереджаю: від тексту може знатно підгоріти у любителів надгнучких методологій та нелюбителів тестувати написане.
Після хаброкату власне починається переклад семінару. Приємного читання!
За яке б завдання ви не взялися, вам завжди потрібно пройти три кроки:
- визначитися, якої мети ви хочете досягти;
- вирішити, як саме ви добиватиметеся своєї мети;
- прийти до своєї мети.
Це стосується програмування. Коли ми пишемо код, нам потрібно:
- вирішити, що саме має робити програма;
- визначити, як саме вона має виконувати своє завдання;
- написати відповідний код.
Останній крок, звичайно, дуже важливий, але про нього я говорити сьогодні не буду. Натомість ми обговоримо перші два. Їх виконує кожен програміст, перш ніж почати працювати. Ви не сідайте писати, якщо не вирішили, що саме пишете: браузер чи базу даних. Певне уявлення про мету обов'язково має бути присутнє. І ви обов'язково продумуєте, що саме програма буде робити, а не пишете абияк у надії, що код сам якось перетвориться на браузер.
Як саме відбувається це попереднє продумування коду? Скільки зусиль нам слід витрачати на це? Все залежить від того, як складну проблему ми вирішуємо. Припустимо, ми хочемо написати стійку до відмови розподілену систему. У цьому випадку нам слід обдумати все як слід, перш ніж сідати за код. А якщо нам просто потрібно збільшити цілісну змінну на 1? На перший погляд, тут все тривіально, і жодних роздумів не потрібно, але потім ми згадуємо, що може статися переповнення. Тому навіть для того, щоб зрозуміти, проста проблема чи складна — спочатку треба подумати.
Якщо продумати можливі рішення проблеми, можна уникнути помилок. Але для цього потрібно, щоб ваше мислення було зрозумілим. Щоб цього досягти, потрібно записувати свої думки. Мені дуже подобається цитата Діка Гіндона: «Коли ви пишете, природа демонструє вам, наскільки неохайне ваше мислення». Якщо ви не пишете, вам тільки здається, що ви думаєте. А записувати свої думки потрібно у формі специфікацій.
Специфікації виконують безліч функцій, особливо у великих проектах. Але я говоритиму лише про одну з них: вони допомагають нам ясно мислити. Ясно мислити дуже важливо і досить важко, тому тут нам потрібна будь-яка підмога. Якою мовою нам слід писати специфікації? Це взагалі завжди перше питання для програмістів: якою мовою ми писатимемо. Одної правильної відповіді на неї немає: проблеми, які ми вирішуємо, надто різноманітні. Для деяких корисний TLA+ — це мова специфікацій, яку я розробив. Для інших зручніше користуватися китайською. Все залежить від ситуації.
Найважливіше інше питання: як досягти більш ясного мислення? Відповідь: ми маємо мислити як вчені. Це спосіб мислення, який добре зарекомендував себе за останні 500 років. У науці ми будуємо математичні моделі дійсності. Астрономія була, мабуть, першою наукою у строгому значенні цього слова. У математичній моделі, що використовується в астрономії, небесні тіла постають як крапки з масою, становищем та імпульсом, хоча насправді вони є вкрай складними об'єктами з горами та океанами, припливами та відливами. Ця модель, як і будь-яка інша, створена для вирішення певних завдань. Вона чудово підходить для того, щоб визначити, куди потрібно направити телескоп, якщо потрібно знайти планету. Але якщо ви бажаєте передбачити погоду на цій планеті, ця модель не підійде.
Математика дозволяє визначити властивості моделі. Наука ж показує, як ці властивості співвідносяться з реальністю. Поговоримо про нашу науку, computer science. Реальність, з якою ми працюємо - це обчислювальні системи різних видів: процесори, ігрові консолі, комп'ютери, що виконують програми і так далі. Я говоритиму про виконання програми на комп'ютері, але, за великим рахунком, всі ці висновки можна застосувати до будь-якої обчислювальної системи. У нашій науці ми використовуємо безліч різних моделей: машина Тьюринга, частково впорядковані безлічі подій та багато інших.
Що таке програма? Це будь-який код, який можна розглядати самостійно. Припустимо, що нам потрібно написати браузер. Ми виконуємо три завдання: проектуємо представлення програми для користувача, потім пишемо високорівневу схему програми і, нарешті, пишемо код. Під час написання коду ми розуміємо, що нам потрібно написати засіб для форматування тексту. Тут нам знову потрібно вирішити три завдання: визначити, який текст цей засіб повертатиме; вибрати алгоритм для форматування; написати код. Це завдання має своє завдання: правильно вставляти дефіс у слова. Це підзавдання ми теж вирішуємо за три кроки — як бачимо, вони повторюються на багатьох рівнях.
Розглянемо детальніше перший крок: яке завдання вирішує програма. Тут ми найчастіше моделюємо програму як функцію, яка отримує деякі вхідні дані та дає деякі дані на виході. У математиці функція зазвичай описується як упорядковане безліч пар. Наприклад, функція зведення квадрат для натуральних чисел описується як безліч {<0,0>, <1,1>, <2,4>, <3,9>, …}. Область визначення такої функції — множина перших елементів кожної пари, тобто натуральні числа. Щоб визначити функцію, нам потрібно вказати її область визначення та формулу.
Але функції в математиці - це не те, що функції в мовах програмування. Математика значно простіша. Оскільки на складні приклади у мене часу немає, розглянемо простий: функція в мові С або статичний метод Java, що повертає найбільший спільний дільник двох цілих чисел. У специфікації цього методу ми напишемо: обчислює GCD(M,N) для аргументів M и N, Де GCD(M,N) — функція, область визначення якої — безліч пар цілих чисел, а значення, що повертається, — найбільше ціле число, на яке ділиться M и N. Як із цією моделлю співвідноситься реальність? Модель оперує з цілими числами, а C або Java ми маємо 32-бітний int. Ця модель дозволяє нам вирішити, чи правильний алгоритм GCDале вона не запобігає помилкам переповнення. Для цього знадобилася б складніша модель, на яку немає часу.
Поговоримо про обмеження функції як моделі. Робота деяких програм (наприклад, операційних систем) не зводиться до того, щоб повернути певне значення певних аргументів, вони можуть виконуватися безперервно. Крім того, функція як модель погано підходить для другого кроку: планування способу розв'язання задачі. Швидке сортування та сортування бульбашкою обчислюють ту саму функцію, але це зовсім різні алгоритми. Тому для опису способу досягнення мети програми використовую іншу модель, назвемо її стандартна поведінкова модель. Програма в ній представлена як безліч усіх допустимих поведінок, кожна з яких, у свою чергу, є послідовністю станів, а стан - це присвоєння значень змінним.
Давайте подивимося, як виглядатиме другий крок для алгоритму Евкліда. Нам потрібно вирахувати GCD(M, N). Ми ініціалізуємо M як x, а N як y, Потім повторно забираємо меншу з цих змінних від більшої до тих пір, поки вони не будуть рівні. Наприклад, якщо M = 12, а N = 18, ми можемо описати таку поведінку:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
А якщо M = 0 и N = 0? Нуль ділиться попри всі числа, тому найбільшого дільника у разі немає. У цій ситуації нам потрібно повернутися до першого кроку і запитати: чи дійсно нам потрібно обчислювати НОД для непозитивних чисел? Якщо в цьому немає потреби, то потрібно просто змінити специфікацію.
Тут слід зробити невеликий відступ про продуктивність. Її часто вимірюють у кількості рядків коду, написаних протягом дня. Але ваша праця значно корисніша, якщо ви позбулися певної кількості рядків, тому що у вас поменшало місця для багів. І позбавлятися коду найпростіше саме на першому кроці. Цілком можливо, що вам просто не потрібні всі навороти, які ви намагаєтеся реалізувати. Найшвидший спосіб спростити програму та заощадити час – не робити речі, які не варто робити. Другий крок – на другому місці за потенціалом для економії часу. Якщо ви вимірюєте продуктивність у кількості написаних рядків, то продумування способу виконання завдання зробить вас менш продуктивними, оскільки ви зможете вирішити те саме завдання меншим обсягом коду. Точну статистику я тут навести не можу, оскільки я не маю способу порахувати ту кількість рядків, які я не написав завдяки тому, що витратив час на специфікацію, тобто на перший і другий кроки. І експеримент тут теж не поставити, тому що в експерименті ми не маємо права виконати перший крок, завдання заздалегідь визначене.
У неформальних специфікаціях легко не врахувати багато труднощів. Нічого складного у написанні суворих специфікацій для функцій немає, обговорювати це не буду. Натомість ми поговоримо про написання суворих специфікацій для стандартних поведінкових моделей. Є теорема, яка свідчить, що будь-яка безліч поведінок можна описати за допомогою якості безпеки (безпека) та властивості живучості (Liveness). Безпека означає, що нічого поганого не станеться, програма не дасть неправильної відповіді. Живучість означає, що рано чи пізно станеться щось хороше, тобто програма рано чи пізно дасть правильну відповідь. Як правило, безпека є важливішим показником, помилки найчастіше виникають саме тут. Тому для економії часу я не говоритиму про живучість, хоча вона, звичайно, теж важлива.
Ми домагаємось безпеки, прописуючи, по-перше, безліч можливих вихідних станів. І, по-друге, відносини з усіма можливими наступними станами кожного стану. Поводитимемося як вчені і визначимо стани математично. Набір вихідних станів описується формулою, наприклад, у разі алгоритму Евкліда: (x = M) ∧ (y = N). Для певних значень M и N існує лише один вихідний стан. Відношення з наступним станом описується формулою, в якій змінні наступного стану записуються зі штрихом, а поточного стану без штриха. У випадку з алгоритмом Евкліда ми матимемо справу з диз'юнкцією двох формул, в одній з яких x є найбільшим значенням, а на другий — y:
У першому випадку нове значення y дорівнює колишньому значенню y, а нове значення x ми отримуємо, відібравши від більшої змінної меншу. У другому випадку ми робимо навпаки.
Повернемося до алгоритму Евкліда. Припустимо знову, що M = 12, N = 18. Це визначає єдиний вихідний стан, (x = 12) ∧ (y = 18). Потім ми підставляємо ці значення формулу вище і отримуємо:
Тут єдине можливе рішення: x' = 18 - 12 ∧ y' = 12, і ми отримуємо поведінку: [x = 12, y = 18]. Так само ми можемо описати всі стани в нашій поведінці: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
В останньому стані [x = 6, y = 6] обидві частини виразу будуть хибні, отже, наступного стану в нього немає. Отже, ми маємо повну специфікацію другого кроку — як бачимо, це цілком звичайна математика, як у інженерів та вчених, а не дивна, як у комп'ютерній освіті.
Ці дві формули можна поєднати в одну формулу темпоральної логіки. Вона елегантна та пояснити її неважко, але на неї зараз немає часу. Темпоральна логіка нам може знадобитися тільки для якості жвавості, для безпеки вона не потрібна. Темпоральна логіка як така не подобається, це не зовсім проста математика, але у випадку з жвавістю вона є необхідним злом.
В алгоритмі Евкліда для кожного значення x и y є унікальні значення x' и y', які ставляться з наступним станом істинним. Інакше кажучи, алгоритм Евкліда детермінований. Щоб змоделювати недетермінований алгоритм, потрібно, щоб у поточного стану було кілька можливих майбутніх станів, і щоб у кожного значення змінної без штриха було кілька значень змінної зі штрихом, при яких ставлення до наступного стану є істинним. Це нескладно зробити, але зараз наводити приклади я не буду.
Щоб створити працюючий інструмент, потрібна формальна математика. Як зробити специфікацію формальною? Для цього нам знадобиться формальна мова, наприклад, . Специфікація алгоритму Евкліда цією мовою виглядатиме таким чином:
Символ знака рівності з трикутником означає, що значення ліворуч від знака визначено як рівне значення праворуч від знака. По суті, специфікація - це визначення, у нашому випадку два визначення. До специфікації у TLA+ потрібно додати оголошення та деякий синтаксис, як на слайді вище. В ASCII це буде виглядати так:
Як бачимо, нічого складного. Специфікацію на TLA+ можна перевірити, тобто обійти всі можливі поведінки у невеликій моделі. У нашому випадку цією моделлю будуть певні значення M и N. Це дуже ефективний та простий спосіб перевірки, який повністю виконується автоматично. Крім того, можна написати формальні докази істинності та перевірити їх механічно, але для цього потрібно багато часу, тому так майже ніхто не робить.
Головний недолік TLA+ у тому, що це математика, а програмісти та комп'ютерні науковці бояться математики. На перший погляд це звучить як жарт, але, на жаль, я говорю це цілком серйозно. Мій колега тільки-но розповідав мені, як він намагався пояснити TLA+ кільком розробникам. Як тільки на екрані з'явилися формули, у них зразу ж стали скляні очі. Тож якщо TLA+ лякає, можна використовувати , це свого роду іграшкова мова програмування. Вираз у PlusCal може бути будь-яким виразом TLA+, тобто, за великим рахунком, будь-яким математичним виразом. Крім того, PlusCal має синтаксис для недетерміністичних алгоритмів. Завдяки тому, що в PlusCal можна записати будь-який вираз TLA+, він є значно виразнішим за будь-яку реальну мову програмування. Далі, PlusCal компілюється в специфікацію TLA+, що легко читається. Це не означає, звичайно, що складна специфікація PlusCal перетвориться на просту на TLA+ — просто відповідність між ними очевидна, не буде додаткової складності. Зрештою, цю специфікацію можна буде перевірити інструментами TLA+. Загалом, PlusCal може допомогти подолати фобію математики, його легко зрозуміти навіть програмістам та комп'ютерним науковцям. У минулому якийсь час (близько 10 років) публікував на ньому алгоритми.
Можливо, хтось заперечить, що TLA+ та PlusCal – це математика, а математика працює лише на вигаданих прикладах. Насправді ж потрібна реальна мова з типами, процедурами, об'єктами тощо. Це не так. Ось, що пише Кріс Ньюкомб, який працював в Amazon: «Ми використовували TLA+ у десяти великих проектах, і в кожному випадку його використання вносило значний внесок у розробку, тому що ми змогли відловити небезпечні баги до потрапляння в продакшн, і тому що він дав нам розуміння та впевненість, необхідні для агресивних оптимізації продуктивності, не що впливають на істинність програми». Часто можна почути, що при використанні формальних методів ми отримуємо неефективний код — на практиці все навпаки. Крім того, існує думка, що менеджерів неможливо переконати в необхідності формальних методів, навіть якщо програмісти переконані в їхній корисності. А Ньюкомб пише: «Менеджери тепер всіляко підштовхують до того, щоб писати специфікації на TLA+ і спеціально виділяють на цей час». Отже, коли менеджери бачать, що TLA+ працює, вони з радістю його приймають. Кріс Ньюкомб написав це десь шість місяців тому (у жовтні 2014 року), зараз, наскільки я знаю, TLA+ використовується в 14 проектах, а не 10. Інший приклад відноситься до проектування XBox 360. До Чарльза Текера прийшов стажер і написав специфікацію системи пам'яті. Завдяки цій специфікації був знайдений баг, який інакше був би не помічений, і через який кожна XBox 360 падала б після чотирьох годин використання. Інженери з IBM підтвердили, що їхні випробування не виявили б цей баг.
Більш детально про TLA+ ви можете почитати в інтернеті, а зараз поговоримо про неформальні специфікації. Нам рідко доводиться писати програми, які обчислюють найменший спільний дільник тощо. Значно частіше ми пишемо програми на кшталт інструменту структурного друку (pretty-printer), який я написав для TLA+. Після найпростішої обробки код на TLA+ виглядав би так:
Але у наведеному прикладі користувач швидше за все хотів, щоб знаки кон'юнкції та рівності були вирівняні. Тож правильне форматування виглядало б швидше так:
Розглянемо ще один приклад:
Тут, навпаки, вирівнювання знаків рівності, складання та множення у джерелі було випадковим, тому найпростішої обробки цілком достатньо. Загалом, точного математичного визначення правильного форматування немає, тому що "правильне" в даному випадку означає "таке, яке хоче користувач", а це математично визначити не можна.
Здавалося б, якщо ми не маємо визначення істинності, то специфікація марна. Але це не так. Якщо ми не знаємо, що саме програма має зробити, це не означає, що нам не потрібно продумувати її роботу — навпаки, ми маємо витратити на це ще більше зусиль. Специфікація тут особливо важлива. Визначити оптимальну програму для структурного друку неможливо, але це не означає, що ми не повинні за неї братися взагалі, а писати код як потік свідомості — це не справа. У результаті я написав специфікацію із шести правил із визначеннями у формі коментарів у Java-файлі. Ось приклад одного з правил: a left-comment token is LeftComment aligned with its covering token. Це правило написано, скажімо так, математичною англійською: LeftComment aligned, left-comment и covering token - Терміни з визначеннями. Це те, як математики описують математику: пишуть визначення термінів і основі них — правила. Користь від такої специфікації полягає в тому, що зрозуміти та налагодити шість правил значно простіше, ніж 850 рядків коду. Треба сказати, що написати ці правила було непросто, чимало часу пішло з їхньої налагодження. Спеціально з цією метою я написав код, який повідомляв, яке саме правило використовується. Завдяки тому, що я перевірив ці шість правил на кількох прикладах, мені не потрібно було налагоджувати 850 рядків коду і баги виявилося досить легко знайти. У Java для цього є чудові інструменти. Якби я просто написав код, то в мене пішло б значно більше часу, і форматування вийшло б найгіршої якості.
Чому не можна було використати формальну специфікацію? З одного боку, правильність виконання тут не надто важлива. Структурний роздрук обов'язково комусь не догодить, тож мені не потрібно було добиватися правильної роботи в усіх неординарних ситуаціях. Ще важливішим є той факт, що у мене не було адекватних інструментів. Засіб для перевірки моделей TLA+ тут марний, тому мені довелося б вручну писати приклади.
У наведеної специфікації є риси, загальні всім специфікацій. Вона вищого рівня, ніж код. Реалізувати її можна будь-якою мовою. Для її написання марні будь-які інструменти чи методи. Жодний курс програмування вам не допоможе написати цю специфікацію. І не існує інструментів, які могли б зробити цю специфікацію непотрібною, якщо, звичайно, ви не пишете мову спеціально для написання програм структурного друку на TLA+. Нарешті, ця специфікація нічого не говорить про те, як саме ми писатимемо код, в ній тільки вказується, що цей код робить. Ми пишемо специфікацію, щоб допомогти нам продумати проблему, перш ніж ми почнемо думати про код.
Але ця специфікація має й особливості, що відрізняють її від інших специфікацій. 95% інших специфікацій значно коротше і простіше:
Далі ця специфікація є набором правил. Як правило, це ознака поганої специфікації. Зрозуміти наслідки набору правил досить важко, і саме тому мені довелося витратити багато часу на їхнє налагодження. Тим не менш, у цьому випадку найкращого способу мені було не знайти.
Варто сказати кілька слів про програми, які працюють безперервно. Як правило, вони працюють паралельно, наприклад операційні системи або розподілені системи. Розібратися в них в умі чи на папері можуть дуже мало хто, і я до них не належу, хоча колись мені це було під силу. Тому необхідні інструменти, які перевірятимуть нашу роботу, наприклад, TLA+ або PlusCal.
Навіщо треба було писати специфікацію, якщо я й так знав, що код повинен робити? Насправді мені тільки здавалося, ніби я це знаю. Крім того, за наявності специфікації сторонній людині вже не потрібно залазити в код, щоб зрозуміти, що саме вона робить. Я маю правило: не повинно бути жодних загальних правил. Це правило, звичайно ж, має виняток, це єдине загальне правило, яке я дотримуюсь: специфікація того, що робить код, повинна повідомляти людям все, що їм потрібно знати при використанні цього коду.
Отже, що саме програмістам потрібно знати про мислення? Для початку те ж, що й усім: якщо ти не пишеш, то тобі тільки здається, що ти мислиш. Крім того, потрібно думати, перш ніж кодити, а це означає, що потрібно писати, перш ніж кодити. Специфікація - це те, що ми пишемо перед тим, як почати кодувати. Специфікація потрібна для будь-якого коду, який може бути використаний або змінений. І цим «хтось» може виявитися сам автор коду через місяць після його написання. Специфікація потрібна для великих програм та систем, для класів, для методів і іноді навіть для складних ділянок окремого методу. Що саме потрібно писати про код? Потрібно описати, що він робить, тобто те, що може бути корисним будь-якій людині, яка використовує цей код. Іноді може бути необхідно вказати, як саме код досягає своєї мети. Якщо цей спосіб ми проходили у курсі алгоритмів, ми називаємо це алгоритмом. Якщо ж це щось більш спеціальне та нове, то ми називаємо це високорівневим проектуванням. Формальної різниці тут немає: і те, й інше є абстрактною моделлю програми.
Як саме слід писати специфікацію коду? Головне: вона повинна бути на рівень вище самого коду. Вона має описувати стани та поведінки. Вона має бути настільки строгою, наскільки цього вимагає завдання. Якщо ви пишете специфікацію способу реалізації завдання, її можна написати на псевдокоді або за допомогою PlusCal. Вчитися писати специфікації потрібно формальних специфікаціях. Це дасть вам необхідні навички, які допоможуть навіть з неформальними. Як навчитися писати формальні специфікації? Коли ми навчалися програмування, ми писали програми, а потім налагоджували їх. Те саме тут: потрібно написати специфікацію, перевірити її за допомогою засобу перевірки моделей і виправити помилки. TLA+, можливо, не найкраща мова для формальної специфікації, і для ваших конкретних потреб швидше за все краще підійде інша мова. Перевага TLA+ у тому, що він чудово вчить математичному мисленню.
Як пов'язати специфікацію та код? За допомогою коментарів, які пов'язують математичні поняття та їхню реалізацію. Якщо ви працюєте з графами, то на рівні програми у вас будуть масиви вузлів та масиви зв'язків. Тому потрібно написати, як саме граф реалізується цими структурами програмування.
Потрібно зауважити, що ніщо з вищесказаного не відноситься до процесу написання коду. Коли ви пишете код, тобто виконуєте третій крок, вам теж потрібно мислити та продумувати програму. Якщо підзавдання виявляється складним чи неочевидним, потрібно написати для неї специфікацію. Але про сам код я тут не говорю. Ви можете користуватися будь-якою мовою програмування, будь-якою методологією, не про них. Крім того, ніщо з вищесказаного не позбавляє необхідності тестувати та налагоджувати код. Навіть якщо абстрактна модель написана правильно, у її реалізації можуть бути баги.
Написання специфікацій – додатковий етап у процесі написання коду. Завдяки ньому багато помилок можна відловити меншими зусиллями - ми це знаємо з досвіду програмістів з Amazon. Зі специфікаціями якість програм стає вищою. То чому тоді ми так часто обходимося без них? Бо писати важко. А писати важко, бо для цього треба думати, а думати також важко. Завжди простіше вдавати, що думаєш. Тут можна провести аналогію з бігом – чим менше ви бігаєте, тим повільніше ви біжите. Потрібно тренувати свої м'язи та вправлятися у листі. Необхідна практика.
Специфікація може бути неправильною. Ви могли десь зробити помилку, або змінити вимоги, або виявилося необхідно зробити поліпшення. Будь-який код, яким хтось користується, доводиться змінювати, тому рано чи пізно специфікація перестане відповідати програмі. В ідеалі в цьому випадку потрібно написати нову специфікацію та повністю переписати код. Ми добре знаємо, що так ніхто не робить. Насправді ми патчемо код і, можливо, оновлюємо специфікацію. Якщо це обов'язково рано чи пізно відбувається, навіщо взагалі писати специфікації? По-перше, для людини, яка правитиме ваш код, кожне зайве слово у специфікації буде на вагу золота, і цією людиною цілком можете бути ви самі. Я часто лаю себе за недостатню специфікацію, коли керую свій код. А я пишу більше специфікацій, ніж коду. Тому, коли ви керуєте код, специфікацію завжди потрібно оновлювати. По-друге, з кожною правкою код стає гіршим, його стає все важче читати та підтримувати. Це наростання ентропії. Але якщо ви не починаєте зі специфікації, то кожен написаний рядок буде редагуванням, і код із самого початку буде громіздким і важкочитаним.
Як казав , жодна битва не була виграна за планом, і жодна битва не була виграна без плану. А він знав дещо про битви. Існує думка, що написання специфікацій — марнування часу. Іноді це справді так, і завдання настільки просте, що продумувати її нема чого. Але завжди треба пам'ятати, що коли вам радять не писати специфікацій, це означає, що вам радять не думати. І про це щоразу слід подумати. Продумування завдання не гарантує, що ви не зробите помилок. Як ми знаємо, чарівної палички ніхто не винайшов і програмування — складне заняття. Але якщо ви не продумуєте завдання, ви гарантовано зробите помилки.
Детальніше про TLA+ та PlusCal можна почитати на спеціальному сайті, туди можна зайти з моєї домашньої сторінки . На цьому у мене все, дякую за увагу.
Нагадую, що це переклад. Коли ви писатимете коментарі — пам'ятайте, що автор їх не прочитає. Якщо вам дійсно хочеться поспілкуватися з автором, він буде на конференції Hydra 2019, яка пройде 11-12 липня 2019 року в Санкт-Петербурзі. Квитки можна придбати .
Джерело: habr.com