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

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

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

След habrokat всъщност започва превода на семинара. Наслади се на четенето!

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

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

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

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

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

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

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

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

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

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

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

Нека разгледаме по-подробно първата стъпка: какъв проблем решава програмата. Тук най-често моделираме програма като функция, която приема някои входни данни и произвежда малко изходни данни. В математиката функцията обикновено се описва като подреден набор от двойки. Например функцията за повдигане на квадрат за естествени числа се описва като набор {<0,0>, <1,1>, <2,4>, <3,9>, …}. Домейнът на такава функция е множеството от първите елементи на всяка двойка, тоест естествените числа. За да дефинираме функция, трябва да посочим нейния обхват и формула.

Но функциите в математиката не са същите като функциите в езиците за програмиране. Математиката е много по-лесна. Тъй като нямам време за сложни примери, нека разгледаме един прост: функция в 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? Нулата се дели на всички числа, така че в този случай няма най-голям делител. В тази ситуация трябва да се върнем към първата стъпка и да попитаме: наистина ли трябва да изчисляваме GCD за неположителни числа? Ако това не е необходимо, просто трябва да промените спецификацията.

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

Лесно е да се пренебрегнат много трудности в неофициалните спецификации. Няма нищо трудно в писането на строги спецификации за функции, няма да обсъждам това. Вместо това ще говорим за писане на силни спецификации за стандартно поведение. Има теорема, която казва, че всеки набор от поведения може да бъде описан с помощта на свойството сигурност (безопасност) и свойства за оцеляване (жизненост). Сигурността означава, че няма да се случи нищо лошо, програмата няма да даде грешен отговор. Оцеляването означава, че рано или късно ще се случи нещо добро, т.е. програмата рано или късно ще даде правилния отговор. По правило сигурността е по-важен показател, тук най-често възникват грешки. Затова, за да спестя време, няма да говоря за оцеляването, въпреки че, разбира се, също е важно.

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

Тези две формули могат да бъдат комбинирани в една формула на темпоралната логика. Тя е елегантна и лесна за обяснение, но сега няма време за нея. Може да се нуждаем от времева логика само за свойството оживеност, тя не е необходима за сигурност. Не харесвам времевата логика като такава, това не е съвсем обикновена математика, но в случая с жизнеността е необходимо зло.

В алгоритъма на Евклид, за всяка стойност x и y имат уникални стойности x' и y', които правят връзката със следващото състояние вярна. С други думи, алгоритъмът на Евклид е детерминиран. За да се моделира недетерминиран алгоритъм, текущото състояние трябва да има множество възможни бъдещи състояния и всяка стойност на непраймирана променлива да има множество стойности на променлива с прайм, така че връзката със следващото състояние да е вярна. Това е лесно да се направи, но сега няма да давам примери.

За да направите работещ инструмент, имате нужда от официална математика. Как да направя спецификацията официална? За да направим това, имаме нужда от формален език, например TLA+. Спецификацията на алгоритъма на Евклид би изглеждала така на този език:

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

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

Основният недостатък на TLA+ е, че е математика, а програмистите и компютърните учени се страхуват от математиката. На пръв поглед звучи като шега, но, за съжаление, го казвам съвсем сериозно. Колегата ми разказваше как се е опитал да обясни TLA+ на няколко разработчици. Щом формулите се появиха на екрана, веднага станаха стъклени очи. Така че, ако TLA+ ви плаши, можете да използвате PlusCal, това е нещо като език за програмиране играчка. Израз в PlusCal може да бъде всеки TLA+ израз, т.е. като цяло всеки математически израз. Освен това PlusCal има синтаксис за недетерминирани алгоритми. Тъй като PlusCal може да напише всеки TLA+ израз, PlusCal е много по-изразителен от всеки реален език за програмиране. След това PlusCal се компилира в лесно четима TLA+ спецификация. Това, разбира се, не означава, че сложната спецификация на PlusCal ще се превърне в проста на TLA + - просто съответствието между тях е очевидно, няма да има допълнителна сложност. И накрая, тази спецификация може да бъде проверена от TLA+ инструменти. Като цяло PlusCal може да помогне за преодоляване на математическата фобия и е лесен за разбиране дори за програмисти и компютърни учени. В миналото публикувах алгоритми за него за известно време (около 10 години).

Може би някой ще възрази, че TLA + и PlusCal са математика, а математиката работи само върху измислени примери. На практика се нуждаете от реален език с типове, процедури, обекти и т.н. Това е грешно. Ето какво пише Крис Нюкомб, който е работил в Amazon: „Използвахме TLA+ на десет големи проекта и във всеки случай имаше значителна разлика в развитието, защото успяхме да хванем опасни грешки, преди да започнем производството, и защото ни даде прозрението и увереността, от които се нуждаехме, за да постигнем агресивно представяне оптимизации, без да се засяга истинността на програмата". Често можете да чуете, че когато използваме формални методи, получаваме неефективен код - на практика всичко е точно обратното. Освен това има мнение, че мениджърите не могат да бъдат убедени в необходимостта от формални методи, дори ако програмистите са убедени в тяхната полезност. И Нюкомб пише: „Мениджърите сега настояват да напишат спецификации за TLA + и специално отделят време за това“. Така че, когато мениджърите видят, че TLA+ работи, те с радост го приемат. Chris Newcomb написа това преди около шест месеца (октомври 2014 г.), но сега, доколкото знам, TLA+ се използва в 14 проекта, а не в 10. Друг пример е в дизайна на XBox 360. Един стажант дойде при Charles Thacker и написа спецификация за системата памет. Благодарение на тази спецификация беше открита грешка, която иначе би останала незабелязана и поради която всеки XBox 360 се срива след четири часа употреба. Инженерите на IBM потвърдиха, че техните тестове не биха открили този бъг.

Можете да прочетете повече за TLA + в Интернет, но сега нека поговорим за неофициалните спецификации. Рядко се налага да пишем програми, които изчисляват най-малкия общ делител и други подобни. Много по-често пишем програми като инструмента за красив принтер, който написах за 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 г. в Санкт Петербург. Билети могат да бъдат закупени на официалния уебсайт.

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