Програмирањето е повеќе од кодирање

Ова е статија за превод Семинар во Стенфорд. Но, пред тоа има краток вовед. Како се формираат зомби? Секој се нашол во ситуација кога сака да доведе пријател или колега на своето ниво, но тоа не им успева. Згора на тоа, „не функционира“ не толку за вас, туку за него: на едната страна од вагата има нормална плата, задачи и така натаму, а од друга е потребата да се размислува. Размислувањето е непријатно и болно. Брзо се откажува и продолжува да пишува код без воопшто да го користи мозокот. Сфаќате колку напор е потребен за да се надмине бариерата на научената беспомошност и едноставно не го правите тоа. Вака се формираат зомби, кои се чини дека е можно да се излечат, но изгледа дека никој нема да го направи ова.

Кога го видов тоа Лесли Лампорт (да, истиот пријател од учебниците) доаѓа во Русија и не дава извештај, туку сесија на прашања и одговори, бев малку претпазлив. За секој случај, Лесли е светски познат научник, автор на семинални трудови во дистрибуирани компјутери, а можеби го познавате и по буквите La во LaTeX - „Lamport TeX“. Вториот алармантен фактор е неговото барање: секој што доаѓа мора (целосно бесплатно) да слуша неколку негови извештаи однапред, да постави барем едно прашање за нив и дури потоа да дојде. Решив да видам што емитува Лампорт таму - и тоа е одлично! Ова е токму тоа нешто, магична врска-пилула за лекување зомби. Ве предупредувам: текстот може сериозно да ги изгори оние кои сакаат супер-агилни методологии и кои не сакаат да го тестираат она што го напишале.

По хаброката всушност започнува преводот на семинарот. Уживајте во читањето!

Без оглед на задачата што ја преземате, секогаш треба да поминете низ три чекори:

• одлучете која цел сакате да ја постигнете;
• одлучете како точно ќе ја постигнете целта;
• достигнете ја вашата цел.

Ова исто така важи и за програмирање. Кога пишуваме код, ни треба:

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

Последниот чекор, се разбира, е многу важен, но јас нема да зборувам за тоа денес. Наместо тоа, ќе разговараме за првите две. Секој програмер ги изведува пред да започне со работа. Не седнувате да пишувате освен ако не сте одлучиле што пишувате: прелистувач или база на податоци. Мора да биде присутна одредена идеја за целта. И дефинитивно размислувате што точно ќе направи програмата и не ја пишувајте случајно со надеж дека самиот код некако ќе се претвори во прелистувач.

Како точно се случува ова претходно размислување за кодот? Колку труд треба да вложиме во ова? Се зависи од тоа колку е сложен проблемот што го решаваме. Да речеме дека сакаме да напишеме дистрибуиран систем толерантен на грешки. Во овој случај, треба внимателно да размислиме пред да седнеме да кодираме. Што ако само треба да зголемиме цела променлива за 1? Овде на прв поглед сè е тривијално и не е потребно размислување, но потоа се сеќаваме дека може да дојде до прелевање. Затоа, дури и за да разберете дали проблемот е едноставен или сложен, прво треба да размислите.

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

Спецификациите служат за многу функции, особено во големи проекти. Но, ќе зборувам само за еден од нив: тие ни помагаат да размислуваме јасно. Размислувањето јасно е многу важно и доста тешко, затоа ни треба каква било помош овде. На кој јазик треба да пишуваме спецификации? Во принцип, ова е секогаш првото прашање за програмерите: на кој јазик ќе пишуваме? Нема еден точен одговор: проблемите што ги решаваме се премногу разновидни. За некои луѓе, TLA+ е корисен - тоа е јазик за спецификација што го развив. За други, попогодно е да се користи кинески. Се зависи од ситуацијата.

Поважното прашање е: како можеме да постигнеме појасно размислување? Одговор: Мора да размислуваме како научници. Ова е начин на размислување кој функционира добро во последните 500 години. Во науката градиме математички модели на реалноста. Астрономијата беше можеби првата наука во строга смисла на зборот. Во математичкиот модел што се користи во астрономијата, небесните тела се појавуваат како точки со маса, положба и импулс, иако во реалноста тоа се исклучително сложени објекти со планини и океани, одливи и текови. Овој модел, како и секој друг, е создаден за да реши одредени проблеми. Одлично е за одредување каде да го насочите телескопот ако сакате да најдете планета. Но, ако сакате да го предвидите времето на оваа планета, овој модел нема да работи.

Математиката ни овозможува да ги одредиме својствата на моделот. И науката покажува како овие својства се поврзани со реалноста. Ајде да зборуваме за нашата наука, компјутерската наука. Реалноста со која работиме е компјутерските системи од секаков вид: процесори, конзоли за игри, компјутери кои работат програми итн. Ќе зборувам за извршување на програма на компјутер, но, во голема мера, сите овие заклучоци важат за секој компјутерски систем. Во нашата наука користиме многу различни модели: Туринговата машина, делумно нарачани збирки настани и многу други.

Која е програмата? Ова е секој код што може да се разгледа самостојно. Да речеме дека треба да напишеме прелистувач. Извршуваме три задачи: дизајнираме презентација на програмата од страна на корисникот, потоа го пишуваме дијаграмот на високо ниво на програмата и на крајот го пишуваме кодот. Додека го пишуваме кодот, сфаќаме дека треба да напишеме форматор на текст. Тука повторно треба да решиме три проблеми: да одредиме кој текст ќе го врати оваа алатка; изберете алгоритам за форматирање; напишете код. Оваа задача има своја подзадача: правилно вметнување цртички во зборовите. Оваа подзадача ја решаваме и во три чекори - како што гледаме, тие се повторуваат на многу нивоа.

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

Но, функциите во математиката не се исти како функциите во програмските јазици. Математиката е многу поедноставна. Бидејќи немам време за сложени примери, ајде да разгледаме едноставен: функција во C или статичен метод во Јава што го враќа најголемиот заеднички делител на два цели броеви. Во спецификацијата на овој метод ќе напишеме: пресметува 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] двата дела на изразот ќе бидат лажни, затоа нема следна состојба. Значи, имаме целосна спецификација на вториот чекор - како што гледаме, ова е сосема обична математика, како онаа на инженерите и научниците, и не е чудна, како во компјутерската наука.

Овие две формули може да се комбинираат во една формула на временска логика. Елегантно е и лесно да се објасни, но сега нема време за тоа. Можеби ни треба временска логика само за својството на живост; за сигурност не е потребна. Не ми се допаѓа временската логика како таква, не е сосема обична математика, но во случај на живост тоа е неопходно зло.

Во Евклидов алгоритам за секоја вредност 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 се математика, а математиката работи само со измислени примери. Во пракса, потребен ви е вистински јазик со типови, процедури, објекти итн. Ова е погрешно. Еве што пишува Крис Њукомб, кој работел во Амазон: „Користевме TLA+ на десет големи проекти, и во секој случај неговата употреба направи значителна разлика во развојот бидејќи можевме да фатиме опасни бубачки пред да стигнат до производството и затоа што ни даде увид и доверба што ни требаа за да направиме агресивни оптимизација на перформансите без да влијае на вистината на програмата“. Често може да слушнете дека кога користиме формални методи добиваме неефикасен код - во пракса, сè е токму спротивното. Покрај тоа, постои перцепција дека менаџерите не можат да бидат убедени во потребата од формални методи, дури и ако програмерите се убедени во нивната корисност. И Њукомб пишува: „Менаџерите сега вршат притисок на секој можен начин да напишат спецификации во TLA+ и конкретно одвојуваат време за тоа“.. Така, кога менаџерите ќе видат дека TLA+ функционира, тие го прифаќаат. Крис Њукомб го напиша ова пред околу шест месеци (октомври 2014), но сега, колку што знам, TLA+ се користи во 14 проекти, а не во 10. Друг пример се однесува на дизајнот на XBox 360. Кај Чарлс Такер дојде практикант и напиша спецификација за меморискиот систем. Благодарение на оваа спецификација, беше пронајден баг кој инаку би бил неоткриен и би предизвикал паѓање на секој XBox 360 по четири часа користење. Инженерите од IBM потврдија дека нивните тестови немало да ја откријат оваа грешка.

Можете да прочитате повеќе за TLA+ на Интернет, но сега ајде да зборуваме за неформалните спецификации. Ретко треба да пишуваме програми кои пресметуваат најмал заеднички делител и слично. Многу почесто пишуваме програми како алатката за прилично печатач што ја напишав за TLA+. По наједноставната обработка, TLA+ кодот би изгледал вака:

Но, во примерот погоре, корисникот најверојатно сакал сврзникот и знаците за еднакви да бидат порамнети. Значи, правилното форматирање би изгледало повеќе вака:

Да разгледаме уште еден пример:

Овде, напротив, порамнувањето на знаците за еднаквост, собирањето и множењето во изворот беше случајно, така што наједноставната обработка е сосема доволна. Во принцип, не постои точна математичка дефиниција за правилно форматирање, бидејќи „точно“ во овој случај значи „што сака корисникот“, а тоа не може да се одреди математички.

Се чини дека ако немаме дефиниција за вистината, тогаш спецификацијата е бескорисна. Но, тоа не е вистина. Само затоа што не знаеме што треба да прави една програма, не значи дека не треба да размислуваме како таа треба да работи - напротив, треба да потрошиме уште повеќе напор на неа. Спецификацијата е особено важна овде. Невозможно е да се одреди оптималната програма за структурирано печатење, но тоа не значи дека воопшто не треба да го преземеме, а пишувањето код како поток на свеста не е така. На крајот напишав спецификација од шест правила со дефиниции во форма на коментари во датотека Јава. Еве еден пример за едно од правилата: a left-comment token is LeftComment aligned with its covering token. Ова правило е напишано на, да речеме, математички англиски: LeftComment aligned, left-comment и covering token — термини со дефиниции. Вака математичарите ја опишуваат математиката: пишуваат дефиниции за поими и врз основа на нив создаваат правила. Придобивката од оваа спецификација е што шест правила се многу полесни за разбирање и отстранување грешки отколку 850 линии код. Морам да кажам дека пишувањето на овие правила не беше лесно; беше потребно доста време за да се дебагираат. Напишав код специјално за оваа цел што ми кажа кое правило се користи. Бидејќи ги тестирав овие шест правила со неколку примери, не морав да дебагирам 850 линии код, а грешките беа прилично лесно да се најдат. Јава има одлични алатки за ова. Да го напишав само кодот, ќе ми требаше многу подолго и форматирањето ќе беше послаб квалитет.

Зошто не може да се користи формална спецификација? Од една страна, правилното извршување не е премногу важно овде. Структурираниот отпечаток сигурно ќе биде незадоволителен за некои, па затоа не морав да го натерам да работи правилно во сите невообичаени ситуации. Уште поважен е фактот што немав соодветни алатки. Проверката на моделот TLA+ е бескорисна овде, па би морал да ги напишам примерите на рака.

Дадената спецификација има карактеристики заеднички за сите спецификации. Тоа е повисоко ниво од кодот. Може да се имплементира на кој било јазик. Нема алатки или методи за пишување. Ниту еден курс за програмирање нема да ви помогне да ја напишете оваа спецификација. И нема алатки што би ја направиле оваа спецификација непотребна, освен ако, се разбира, пишувате јазик специјално за пишување програми за структурирани отпечатоци во TLA+. Конечно, оваа спецификација не кажува ништо за тоа како точно ќе го напишеме кодот, туку само наведува што прави кодот. Ние пишуваме спецификација за да ни помогне да размислиме за проблемот пред да почнеме да размислуваме за кодот.

Но, оваа спецификација има и карактеристики што ја разликуваат од другите спецификации. 95% од другите спецификации се многу пократки и поедноставни:

Понатаму, оваа спецификација е збир на правила. Ова е обично знак за лоша спецификација. Разбирањето на последиците од збир правила е доста тешко, поради што морав да потрошам многу време за да ги дебагирам. Меѓутоа, во овој случај не можев да најдам подобар начин.

Вреди да се каже неколку зборови за програмите што работат постојано. Обично тие работат паралелно, како што се оперативни системи или дистрибуирани системи. Многу малку луѓе можат да ги разберат во нивните умови или на хартија, а јас не сум еден од нив, иако некогаш можев да го направам тоа. Затоа, потребни ни се алатки кои ќе ја проверат нашата работа - на пример, TLA+ или PlusCal.

Зошто требаше да напишам спецификација ако веќе знаев што треба да прави кодот? Всушност, само мислев дека го знам тоа. Покрај тоа, со одредена спецификација, аутсајдер повеќе не треба да го разгледува кодот за да разбере што точно прави. Имам правило: не треба да има општи правила. Се разбира, постои исклучок од ова правило, ова е единственото општо правило што го следам: спецификацијата за тоа што прави кодот треба да им каже на луѓето сè што треба да знаат кога го користат тој код.

Значи, што точно треба да знаат програмерите за размислувањето? За почеток, исто како и за сите: ако не пишувате, тогаш само ви се чини дека размислувате. Исто така, треба да размислите пред да кодирате, што значи дека треба да напишете пред да кодирате. Спецификација е она што го пишуваме пред да започнеме со кодирање. Потребна е спецификација за кој било код што може да го користи или менува секој. И овој „некој“ може да испадне дека е автор на кодот еден месец откако е напишан. Потребна е спецификација за големи програми и системи, за класи, за методи, а понекогаш дури и за сложени делови од еден метод. Што точно треба да напишете за кодот? Треба да опишете што прави, односно нешто што може да биде корисно за секој што го користи овој код. Понекогаш, исто така, може да биде неопходно да се специфицира како точно кодот ја постигнува својата цел. Ако го поминавме овој метод во курсот за алгоритми, тогаш го нарекуваме алгоритам. Ако е нешто поспецијализирано и ново, тогаш го нарекуваме дизајн на високо ниво. Тука нема формална разлика: и двата се апстрактни модели на програмата.

Како точно треба да напишете спецификација за код? Главната работа: треба да биде едно ниво повисоко од самиот код. Мора да ги опишува состојбите и однесувањата. Треба да биде строго колку што бара задачата. Ако пишувате спецификација за тоа како да имплементирате задача, тогаш таа може да биде напишана во псевдокод или со помош на PlusCal. Треба да научите да пишувате спецификации користејќи формални спецификации. Ова ќе ви ги даде потребните вештини кои исто така ќе ви помогнат со неформалните. Како можете да научите да пишувате формални спецификации? Кога научивме да програмираме, пишувавме програми и потоа ги дебагиравме. Истото овде: треба да напишете спецификација, да ја проверите со проверувач на модели и да ги поправите грешките. TLA+ можеби не е најдобриот јазик за формална спецификација, а друг јазик најверојатно ќе биде подобро прилагоден за вашите специфични потреби. Најдоброто нешто за TLA+ е тоа што одлично го предава математичкото размислување.

Како да ги поврзете спецификацијата и кодот? Користење на коментари кои ги поврзуваат математичките концепти и нивната имплементација. Ако работите со графикони, тогаш на ниво на програмата ќе имате низи од јазли и низи од врски. Значи, треба да напишете како точно графикот е имплементиран од овие програмски структури.

Треба да се напомене дека ништо од горенаведеното не се однесува на самиот процес на пишување код. Кога пишувате код, односно го изведувате третиот чекор, исто така треба да размислите и размислите низ програмата. Ако подзадачата се испостави дека е сложена или не е очигледна, треба да напишете спецификација за неа. Но, овде не зборувам за самиот код. Можете да користите кој било програмски јазик, која било методологија, ова не е за нив. Исто така, ниту едно од горенаведените не ја елиминира потребата за тестирање и дебагирање на вашиот код. Дури и ако апстрактниот модел е правилно напишан, може да има грешки во неговата имплементација.

Пишувањето спецификации е дополнителен чекор во процесот на кодирање. Благодарение на него, многу грешки може да се фатат со помал напор - ова го знаеме од искуството на програмерите од Amazon. Со спецификациите, квалитетот на програмите станува повисок. Па зошто тогаш толку често одиме без нив? Затоа што пишувањето е тешко. Но, пишувањето е тешко, бидејќи за ова треба да се размислува, а размислувањето е исто така тешко. Секогаш е полесно да се преправате дека размислувате. Тука може да се направи аналогија со трчањето - колку помалку трчате, толку побавно трчате. Треба да ги тренирате вашите мускули и да вежбате пишување. Потребна е пракса.

Спецификацијата може да биде неточна. Можеби сте згрешиле некаде, или барањата можеби се смениле или можеби треба да се направи подобрување. Секој код што некој го користи мора да се смени, па порано или подоцна спецификацијата повеќе нема да одговара на програмата. Идеално, во овој случај, треба да напишете нова спецификација и целосно да го преработите кодот. Добро знаеме дека никој не го прави ова. Во пракса, го закрпивме кодот и можеби ја ажурираме спецификацијата. Ако ова е обврзано да се случи порано или подоцна, тогаш зошто воопшто да пишувате спецификации? Прво, за лицето кое ќе го уреди вашиот код, секој дополнителен збор во спецификацијата ќе вреди злато, а оваа личност можеби сте вие. Често се шутнам себеси затоа што не сум доволно конкретен кога го уредувам мојот код. И пишувам повеќе спецификации отколку код. Затоа, кога го уредувате кодот, спецификацијата секогаш треба да се ажурира. Второ, со секое уредување кодот станува полош, станува потежок за читање и одржување. Ова е зголемување на ентропијата. Но, ако не започнете со спецификација, тогаш секој ред што ќе го напишете ќе биде уредување, а кодот ќе биде гломазен и тешко читлив од самиот почеток.

Како што е речено Ајзенхауер, ниту една битка не била добиена според план и ниту една битка не била добиена без план. И тој знаеше нешто за битките. Постои мислење дека пишувањето спецификации е губење време. Понекогаш тоа е точно, а задачата е толку едноставна што нема смисла да се размислува. Но, секогаш треба да запомните дека кога ве советуваат да не пишувате спецификации, тоа значи дека ве советуваат да не размислувате. И треба да размислувате за ова секој пат. Размислувањето низ задачата не гарантира дека нема да направите грешки. Како што знаеме, никој не измислил волшебно стапче, а програмирањето е тешка задача. Но, ако не размислите за задачата, гарантирано ќе направите грешки.

Можете да прочитате повеќе за TLA+ и PlusCal на посебна веб-локација, можете да отидете таму од мојата почетна страница по ссылке. Тоа е се за мене, благодарам за вниманието.

Запомнете дека ова е превод. Кога пишувате коментари, запомнете дека авторот нема да ги чита. Ако навистина сакате да разговарате со авторот, тој ќе биде на конференцијата Hydra 2019, која ќе се одржи на 11-12 јули 2019 година во Санкт Петербург. Билетите може да се купат на официјалната веб-страница.

Извор: www.habr.com