Програмирането е повече от кодиране

Тази статия е превод на семинара в Станфорд. Но преди това малко въведение. Как се образуват зомбита? Всеки е изпадал в ситуация, в която иска да повдигне приятел или колега до своето ниво, но не успява. И в случая „не успява“ не е толкова за теб, колкото за него: от едната страна имаш нормална заплата, задачи и т.н., а от другата — необходимостта да мислиш. Мисленето е неприятно и болезнено. Той бързо се отказва и продължава да пише код, без да включва мозъка си. Представяш ли си колко много усилия трябва да се положат, за да преодолееш бариерата на научената безпомощност, и просто не го правиш. Така се образуват зомбита, които уж могат да бъдат излекувани, но сякаш никой не желае да се заеме с това.

Когато видях, че Лесли Лемпарт (да-да, същият човек от учебниците) приезжда в Русия и прави не лекция, а сесия с въпроси и отговори, малко се насторожих. За всеки случай, Лесли е широко известен учен, автор на основополагающи трудове в разпределените изчисления, а вие също може да го познавате по буквите La в думата LaTeX — „Lamport TeX“. Вторият притеснителен фактор е неговото изискване: всеки, който дойде, трябва (абсолютно безплатно) предварително да изслуша няколко негови лекции, да измисли поне един въпрос и едва тогава да идва. Реших да видя какво точно проповядва Лемпорт — и това е прекрасно! Това е точно онази нещо, магическата връзка-таблетка за лечение на зомбита. Предупреждавам: текстът може да предизвика силно раздразнение у любителите на супер-гъвкавите методологии и у онези, които не обичат да тестват написаното.

След хаброката, всъщност, започва преводът на семинара. Приятно четене!

Каквото и задание да си поставите, винаги трябва да преминете през три стъпки:

• да определите каква цел искате да постигнете;
• да решите как точно ще постигнете целта си;
• да стигнете до целта си.

Това важи и за програмирането. Когато пишем код, трябва да:

• определим какво точно трябва да прави програмата;
• да определим как точно трябва да изпълнява задачата си;
• да напишем съответния код.

Последният етап, разбира се, е много важен, но за него няма да говоря днес. Вместо това ще обсъдим първите два. Те се изпълняват от всеки програмист преди да започне работа. Не сядате да пишете, ако не сте решили какво точно пишете: браузър или база данни. Определено представление за целта трябва да присъства. И задължително обмисляте какво точно програмата ще прави, а не пишете безцелно в надеждата, че кодът сам ще се преобразува в браузър.

Как точно протича това предварително обмисляне на кода? Колко усилия трябва да вложим в него? Всичко зависи от това колко сложен проблем решаваме. Да предположим, че искаме да напишем отказоустойчива разпределена система. В този случай трябва добре да обмислим всичко, преди да седнем пред кода. А ако просто трябва да увеличим целочислена променлива с 1? На пръв поглед, всичко изглежда тривиално и не са нужни разисквания, но после се сещаме, че може да настъпи препълване. Затова, дори за да разберем, дали проблемът е прост или сложен — първо трябва да помислим.

Ако предварително обмислите възможните решения на проблема, можете да избегнете грешки. Но за това е необходимо да имате ясен ум. За да постигнете това, трябва да записвате мислите си. Много харесвам цитата на Дик Гиндън: «Когато пишете, природата ви показва колко небрежно мислите». Ако не пишете, само ви се струва, че мислите. А записването на мислите трябва да става под формата на спецификации.

Спецификациите изпълняват множество функции, особено в големи проекти. Но ще говоря само за една от тях: те ни помагат да мислим ясно. Ясното мислене е много важно и доста трудно, затова тук ни е нужно всяко помощно средство. На какъв език трябва да пишем спецификациите? Това всъщност винаги е първият въпрос за програмистите: на какъв език ще пишем. Няма единствено правилен отговор на него: проблемите, които решаваме, са твърде разнообразни. За някои е полезен TLA+ — език за спецификации, който разработих. За други е по-удобно да ползват китайски. Всичко зависи от ситуацията.

По-важному, следващият въпрос е: как да постигнем по-ясно мислене? Отговорът е: трябва да мислим като учени. Това е начин на мислене, който отлично се е утвърдил през последните 500 години. В науката изграждаме математически модели на реалността. Астрономията вероятно е била първата наука в строгия смисъл на думата. В математическия модел, прилаган в астрономията, небесните тела се представят като точки с маса, положение и импулс, въпреки че в действителност те са изключително сложни обекти с планини и океани, приливи и отливи. Този модел, както и всеки друг, е създаден да решава определени задачи. Той е полезен за определяне на посоката, в която трябва да се насочи телескопа, ако трябва да се намери планета. Но ако искате да предскажете времето на тази планета, този модел не е приложим.

Математиката ни позволява да определим свойствата на модела. А науката показва как тези свойства кореспондират с реалността. Нека поговорим за нашата наука, компютърните науки. Реалността, с която работим, е изчислителни системи от най-различни видове: процесори, игрови конзоли, компютри, изпълняващи програми и така нататък. Ще говоря за изпълнението на програма на компютър, но всъщност всичките тези заключения са приложими за всяка изчислителна система. В нашата наука използваме множество различни модели: машина на Тюринг, частично подредени множества от събития и много други.

Какво е програма? Това е всеки код, който може да бъде разглеждан самостоятелно. Да предположим, че трябва да напишем браузър. Изпълняваме три задачи: проектираме представянето на програмата за потребителя, след това пишем високонаивен план на програмата и накрая пишем кода. Докато пишем кода, осъзнаваме, че трябва да напишем средство за форматиране на текст. Тук отново трябва да решим три задачи: да определим какъв текст това средство ще връща; да изберем алгоритъм за форматиране; да напишем кода. Тази задача има своя подзадача: правилно да вмъкваме дефис в думите. Тази подзадача решаваме също в три стъпки — как виждаме, те се повтарят на много нива.

Нека разгледаме по-подробно първата стъпка: каква задача решава програмата. Тук ние най-често моделираме програмата като функция, която получава някои входящи данни и дава някои изходни данни. В математиката функцията обикновено се описва като наредена сборка от двойки. Например, функцията на возводене в квадрат за натуралните числа се описва като съвкупност {, , , , …}. Областта на определение на такава функция — съвкупността от първите елементи на всяка двойка, т.е. натуралните числа. За да определим функция, трябва да посочим нейната област на дефиниция и формули.

Но функциите в математиката не са същите като функциите в езиците за програмиране. Математиката е значително по-проста. Понеже нямам време за сложни примери, нека разгледаме прост: функция в C или статичен метод в 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? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.

Тук трябва да направим малко отклонение относно производителността. Често я измерват в броя на редовете код, написани на ден. Но вашата работа е значително полезна, ако сте се избавили от определен брой редове, защото това намалява пространството за бъгове. И избавянето от код е най-лесно именно в първия етап. Възможно е просто да не ви трябват всички тези сложни неща, които се опитвате да реализирате. Най-бързият начин да опростите програмата и да спестите време е да не правите неща, които не трябва да правите. Вторият етап е на второ място по потенциал за спестяване на време. Ако измервате производителността в количество написани редове, размислянето за начина на изпълнение на задачата ще ви направи по-малко продуктивни, тъй като ще можете да решите същата задача с по-малко количество код. Не мога да предоставя точна статистика тук, тъй като нямам начин да преброя онези редове, които не написах, благодарение на времето, инвестирано в спецификацията, т.е. в първия и втория етап. И тук няма как да проведем експеримент, защото в експеримента нямаме право да извършим първия етап, задачата е предварително зададена.

В неформалните спецификации е лесно да не се вземат предвид много трудности. Няма нищо сложно в написването на строги спецификации за функции, това няма да обсъждам. Вместо това ще говорим за написването на строги спецификации за стандартни поведенчески модели. Съществува теорема, която гласи, че всяко множество поведения може да бъде описано с помощта на свойствата на безопасност (safety) и свойствата на живучест (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+. Спецификацията на алгоритъма на Евклид на този език ще изглежда по следния начин:

Символът на равенството с триъгълник означава, че стойността отляво от знака е определена като равна на стойността отдясно. В същността си, спецификацията е определение, в нашия случай две определения. Към спецификацията в TLA+ трябва да добавим декларирания и някакъв синтаксис, както е на слайда по-горе. В ASCII това ще изглежда по следния начин:

Както виждаме, няма нищо сложно. Спецификацията на TLA+ може да бъде тествана, т.е. да се обходят всички възможни поведения в малък модел. В нашия случай този модел ще бъде определени стойности M и N. Това е много ефективен и прост начин за проверка, който се извършва напълно автоматично. Освен това, може да бъдат написани формални доказателства за истинност и да бъдат проверени механично, но за това е нужно много време, затова почти никой не го прави.

Основният недостатък на TLA+ е, че това е математика, а програмистите и компютърните учени се страхуват от математиката. На пръв поглед това изглежда като шега, но за съжаление, говоря напълно сериозно. Моят колега току-що ми разказа как е опитвал да обясни TLA+ на няколко разработчици. Щом на екрана се появиха формули, веднага им стана стъклено на очите. Така че ако TLA+ плаши, може да се използва PlusCal, това е един вид игрален език за програмиране. Изразяването в 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 файл. Ето пример на едно от правилата: токен left-comment е LeftComment, подравнен с покриващия токен. Това правило е написано на, да кажем, математически английски: LeftComment подравнен, left-comment и покриващ токен — термините с определения. Това е начинът, по който математиката описва математиката: пишат определения на термините и на тяхна основа — правила. Ползата от такава спецификация е, че да разбереш и отстраниш проблеми с шест правила е значително по-лесно, отколкото с 850 реда код. Трябва да кажа, че написването на тези правила не беше лесно, отделих доста време за тяхното отстраняване на проблеми. Специално за тази цел написах код, който съобщаваше кое точно правило се използва. Благодаря на това, че проверих тези шест правила с няколко примера, не ми се наложи да отстранявам 850 реда код, и проблемите се оказаха доста лесни за намиране. В Java за това има отлични инструменти. Ако просто бях написал кода, щеше да ми отнеме значително повече време и форматирането щеше да е с по-ниско качество.

Защо не можеше да се използва формална спецификация? От една страна, точността тук не е толкова важна. Структурният печат непременно ще бъде неугоден на някого, така че не ми беше нужно да се старая да работи правилно във всички извънредни ситуации. Още по-важно е, че нямах подходящи инструменти. Средството за проверка на модели TLA+ тук е безполезно, така че щях да трябва ръчно да пиша примери.

Представената спецификация има черти, общи за всички спецификации. Тя е на по-високо ниво от кода. Може да бъде реализирана на всеки език. За нейното написване не са полезни никакви инструменти или методи. Никакой курс по програмиране няма да ви помогне да напишете тази спецификация. И не съществуват инструменти, които да направят тази спецификация ненужна, освен ако не пишете език специално за написване на програми за структурен печат на TLA+. Накрая, тази спецификация не казва нищо за това как точно ще напишем кода, в нея просто е посочено какво прави този код. Пишем спецификация, за да ни помогне да обмислим проблема, преди да започнем да мислим за кода.

Но тази спецификация има и особености, различаващи я от другите спецификации. 95% от другите спецификации са значително по-кратки и по-прости:

Освен това, тази спецификация представлява набор от правила. Обикновено, това е признак за лоша спецификация. Разбирането на последствията от набор от правила е доста трудно, именно затова ми отне много време, за да ги отстраня. Въпреки това, в този случай не намерих по-добър начин.

Няма да е излишно да кажем няколко думи за програмите, които работят непрекъснато. Обикновено, те работят паралелно, например операционни системи или разпределени системи. Много малко хора могат да ги разгадаят в ума си или на хартия, и аз не съм сред тях, макар че някога ми беше по силите. Поради това са необходими инструменти, които да проверяват нашата работа — например TLA+ или PlusCal.

Каква беше целта да се напише спецификация, ако и без това знаех какво точно трябва да прави кодът? Всъщност, просто ми се струваше, че знам. Освен това, при наличие на спецификация, на някой, който не е запознат, вече не му се налага да се вглежда в кода, за да разбере какво точно прави. Имам правило: не трябва да има общи правила. Това правило, разбира се, има изключение - единственото общо правило, което следвам: спецификацията на това, което прави кодът, трябва да информира хората за всичко, което им е нужно да знаят при използването на този код.

И така, какво точно трябва да знаят програмистите за мисленето? Първо, същото, което и всички останали: ако не пишеш, просто ти се струва, че мислиш. Освен това, трябва да мислиш преди да кодираш, а това означава, че трябва да пишеш, преди да кодираш. Спецификацията е нещото, което пишем преди да започнем да кодиране. Спецификацията е необходима за всеки код, който може да бъде използван или променен от някого. И този „някой“ може да бъде самият автор на кода след месец от неговото написване. Спецификацията е необходима за големи програми и системи, за класове, за методи и понякога дори за сложни участъци от отделен метод. Какво точно трябва да пишем за кода? Трябва да опишем какво прави, т.е. това, което може да бъде полезно за всеки човек, който използва този код. Понякога може да е необходимо също така да посочим как точно кодът постига целта си. Ако този начин сме изучавали в курса по алгоритми, наричаме го алгоритъм. Ако обаче това е нещо по-специално и ново, наричаме го високо ниво проектиране. Няма формална разлика тук: и двете са абстрактни модели на програмата.

Как точно трябва да се пише спецификация на кода? Най-важното: тя трябва да бъде на по-високо ниво от самия код. Тя трябва да описва състоянията и поведението. Тя трябва да бъде толкова строга, колкото изисква задачата. Ако пишете спецификация на начина на реализиране на задачата, може да я напишете на псевдокод или с помощта на PlusCal. Трябва да се научите да пишете спецификации на формални спецификации. Това ще ви даде необходимите умения, които ще помогнат и за неформални. А как да се научите да пишете формални спецификации? Когато учехме програмиране, пишехме програми и след това ги отстранявахме. Същото е и тук: трябва да напишете спецификация, да я проверите с инструмент за проверка на модели и да коригирате грешките. TLA+ не е най-добрият език за формална спецификация и вероятно за вашите конкретни нужди друг език ще е по-добър. Предимството на TLA+ е, че той прекрасно учи на математическо мислене.

Как да свържете спецификацията с кода? Чрез коментари, които свързват математическите концепции с тяхната реализация. Ако работите с графи, на ниво програма ще имате масиви от възли и масиви от връзки. Затова трябва да напишете как точно графът се реализира с тези структури на програмирането.

Трябва да се отбележи, че нищо от горепосоченото не се отнася до самия процес на писане на код. Когато пишете код, т.е. изпълнявате третата стъпка, трябва също така да мислите и да обмисляте програмата. Ако подзадачата се окаже сложна или неопределена, трябва да напишете спецификация за нея. Но не говоря за самия код тук. Можете да ползвате какъвто и да е език за програмиране, каквато и да е методология, тук не става въпрос за тях. Освен това, нищо от горепосоченото не освобождава от необходимостта да тествате и да отстранявате проблеми в кода. Дори когато абстрактният модел е написан правилно, в неговата реализация могат да бъдат налични бъгове.

Писането на спецификации е допълнителен етап в процеса на писане на код. Чрез него много грешки могат да бъдат улавяни с по-малко усилия — знаем това от опита на програмистите от Amazon. Със спецификациите качеството на програмите става по-високо. Как тогава често се справяме без тях? Защото е трудно да се пише. А пише трудно, защото за това трябва да се мисли, а мисленето също е трудно. Винаги е по-лесно да се прави, че мислиш. Тук можем да направим аналогия с бягането — колкото по-малко бягате, толкова по-бавно бягате. Нужно е да тренирате мускулите си и да се упражнявате в писане. Необходима е практика.

Спецификация може да е неверна. Можеше да направите грешка някъде или изискванията да са се променили, или може да е било необходимо да се направи подобрение. Всеки код, който някой използва, трябва да се променя, така че рано или късно спецификацията ще престане да съответства на програмата. В идеалния случай в този случай трябва да напишете нова спецификация и напълно да препишете кода. Ние отлично знаем, че никой не прави това. На практика ние пускаме корекции в кода и евентуално обновяваме спецификацията. Ако това непременно се случва рано или късно, тогава за какво въобще да пишем спецификации? Първо, за човека, който ще редактира вашия код, всяка излишна дума в спецификацията ще бъде на тежест. И този човек може да сте вие самите. Често се упреквам за недостатъчната спецификация, когато редактирам своя код. А аз пиша повече спецификации, отколкото код. Следователно, когато редактирате кода, спецификацията винаги трябва да се обновява. На второ място, с всяка редакция кодът става по-лош, все по-трудно е да се чете и поддържа. Това е нарастване на ентропията. Но ако не започнете със спецификация, всяка написана линия ще бъде редакция и кодът от самото начало ще бъде тромав и труден за четене.

Както каза Ейзенхауер, Няма нито една битка, спечелена по план, и няма нито една битка, спечелена без план.. А той знаеше нещо за битките. Съществува мнение, че написването на спецификации е безполезна загуба на време. Понякога наистина е така, а задачата е толкова проста, че няма какво да се обмисля. Но винаги трябва да помните, че когато ви съветват да не пишете спецификации, това означава, че ви съветват да не мислите. И за това всяка година трябва да се помисли. Обмислянето на задачата не гарантира, че няма да направите грешки. Както знаем, никой не е изобретил вълшебна пръчка и програмирането е сложно занимание. Но ако не обмисляте задачата, вие сигурно ще направите грешки.

По-подробно за TLA+ и PlusCal можете да прочетете на специализирания сайт, можете да влезете от моята домашна страница на линка. С това приключвам, благодаря за вниманието.

Напомням, че това е превод. Когато пишете коментари — помнете, че авторът им няма да ги прочете. Ако наистина искате да се свържете с автора, той ще бъде на конференцията Hydra 2019, която ще се проведе на 11-12 юли 2019 г. в Санкт Петербург. Билети могат да бъдат закупени на официалния сайт.

Източник: habr.com