Гэта артыкул-пераклад . Але перад ёй невялікі ўступ. Як утвараюцца зомбі? Кожны трапляў у сітуацыю, калі хочацца падцягнуць сябра ці калегу да свайго ўзроўню, а не атрымоўваецца. Прычым "не атрымліваецца" не столькі ў цябе, колькі ў яго: на адной чары шаляў знаходзіцца нармальная зарплата, задачы і гэтак далей, а на іншай - неабходнасць думаць. Думаць непрыемна і балюча. Ён хутка здаецца і працягвае пісаць код, зусім не ўключаючы мозг. Ты ўяўляеш, наколькі шмат сіл трэба патраціць, каб пераадолець бар'ер вывучанай бездапаможнасці, і проста не робіш гэтага. Так утвараюцца зомбі, якіх быццам бы можна вылечыць, але быццам бы і ніхто гэтым займацца не стане.
Калі я ўбачыў, што (так-так, той самы таварыш з падручнікаў) і робіць не даклад, а сесію пытанняў-адказаў, я крыху насцярожыўся. На ўсякі выпадак, Леслі – сусветна вядомы вучоны, аўтар асноўных прац у размеркаваных вылічэннях, а яшчэ вы яго можаце ведаць па літарах 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? Нуль дзеліцца на ўсе лікі, таму найбольшага дзельніка ў гэтым выпадку няма. У гэтай сітуацыі нам трэба вярнуцца да першага кроку і спытаць: ці сапраўды нам трэба вылічаць НОД для недадатных лікаў? Калі ў гэтым няма неабходнасці, тое трэба проста змяніць спецыфікацыю.
Тут варта зрабіць невялікі адступ аб прадуктыўнасці. Яе часта вымяраюць у колькасці радкоў кода, напісаных за дзень. Але ваша праца значна карысней, калі вы пазбавіліся ад вызначанай колькасці радкоў, таму што ў вас стала менш месцы для багаў. І пазбаўляцца ад кода прасцей за ўсё менавіта на першым кроку. Цалкам магчыма, што вам проста не патрэбны ўсе тыя навароты, якія вы спрабуеце рэалізаваць. Самы хуткі спосаб спрасціць праграму і зэканоміць час - не рабіць рэчы, якія не варта рабіць. Другі крок - на другім месцы па патэнцыяле для эканоміі часу. Калі вы вымяраеце прадуктыўнасць у колькасці напісаных радкоў, тое прадумванне спосабу выканання задачы зробіць вас менш прадуктыўнымі, паколькі вы зможаце вырашыць тую ж задачу меншым аб'ёмам кода. Дакладную статыстыку я тут прывесці не магу, паколькі ў мяне няма спосабу палічыць тую колькасць радкоў, якія я не напісаў дзякуючы таму, што патраціў час на спецыфікацыю, гэта значыць на першы і другі крокі. І эксперымент тут таксама не паставіць, таму што ў эксперыменце мы не маем права выканаць першы крок, заданне вызначана загадзя.
У нефармальных спецыфікацыях лёгка не ўлічыць шматлікія цяжкасці. Нічога складанага ў напісанні строгіх спецыфікацый для функцый няма, абмяркоўваць гэта я не буду. Замест гэтага мы пагаворым аб напісанні строгіх спецыфікацый для стандартных паводніцкіх мадэляў. Ёсць тэарэма, якая абвяшчае, што любое мноства паводзін можна апісаць з дапамогай уласцівасці бяспекі (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] абедзве часткі выразы будуць ілжывыя, такім чынам, наступнага стану ў яго няма. Такім чынам, мы маем поўную спецыфікацыю другога кроку – як бачым, гэта цалкам звычайная матэматыка, як у інжынераў і навукоўцаў, а не дзіўная, як у computer science.
Гэтыя дзве формулы можна аб'яднаць у адну формулу тэмпаральнай логікі. Яна элегантная і растлумачыць яе няцяжка, але на яе зараз няма часу. Тэмпаральная логіка нам можа спатрэбіцца толькі для ўласцівасці жвавасці, для бяспекі яна не патрэбна. Тэмпаральная логіка як такая не падабаецца, гэта не зусім звычайная матэматыка, але ў выпадку з жвавасцю яна з'яўляецца неабходным злом.
У алгарытме Еўкліда для кожнага значэння x и y ёсць унікальныя значэння x' и y', якія робяць стаўленне з наступным станам сапраўдным. Іншымі словамі, алгарытм Еўкліда дэтэрмінаваны. Каб змадэляваць недэтэрмінаваны алгарытм, трэба, каб у бягучага стану было некалькі магчымых будучых станаў, і каб у кожнага значэння зменнай без рыскі было некалькі значэнняў зменнай са рыскай, пры якіх стаўленне з наступным станам з'яўляецца праўдзівым. Гэта нескладана зрабіць, але зараз прыводзіць прыклады я не буду.
Каб зрабіць працавальную прыладу, патрэбна фармальная матэматыка. Як зрабіць спецыфікацыю фармальнай? Для гэтага нам спатрэбіцца фармальная мова, напрыклад, . Спецыфікацыя алгарытму Еўкліда будзе на гэтай мове выглядаць наступным чынам:
Сімвал знака роўнасці з трыкутнікам азначае, што значэнне злева ад знака вызначана як роўнае значэнню справа ад знака. Па сутнасці, спецыфікацыя - гэта вызначэнне, у нашым выпадку два вызначэння. Да спецыфікацыі ў TLA+ трэба дадаць аб'явы і некаторы сінтаксіс, як на слайдзе вышэй. У ASCII гэта будзе выглядаць так:
Як бачым, нічога складанага. Спецыфікацыю на TLA+ можна праверыць, т. е. абыйсці ўсе магчымыя паводзін у невялікай мадэлі. У нашым выпадку гэтай мадэллю будуць пэўныя значэнні M и N. Гэта вельмі эфэктыўны і просты спосаб праверкі, які цалкам выконваецца аўтаматычна. Акрамя таго, можна напісаць фармальныя доказы праўдзівасці і праверыць іх механічна, але для гэтага трэба шмат часу, таму так амаль ніхто не робіць.
Галоўны недахоп TLA+ у тым, што гэта матэматыка, а праграмісты і computer scientists баяцца матэматыкі. На першы погляд гэта гучыць як жарт, але, нажаль, я кажу гэта на поўным сур'ёзе. Мой калега толькі што расказваў мне, як ён спрабаваў растлумачыць TLA+ некалькім распрацоўшчыкам. Як толькі на экране з'явіліся формулы, у іх адразу ж зрабіліся шкляныя вочы. Так што калі TLA+ палохае, можна выкарыстоўваць , гэта свайго роду цацачны мову праграмавання. Выраз у PlusCal можа быць любым выразам TLA+, гэта значыць, па вялікім рахунку, любым матэматычным выразам. Акрамя таго, у PlusCal ёсць сінтаксіс для недэтэрміністычных алгарытмаў. Дзякуючы таму, што ў PlusCal можна запісаць любы выраз TLA+, ён з'яўляецца значна больш выразным любой рэальнай мовы праграмавання. Далей, PlusCal кампілюецца ў лёгка чытэльную спецыфікацыю TLA+. Гэта не значыць, вядома, што складаная спецыфікацыя PlusCal ператворыцца ў простую на TLA+ - проста адпаведнасць паміж імі відавочная, не з'явіцца дадатковай складанасці. Нарэшце, гэтую спецыфікацыю можна будзе праверыць прыладамі TLA+. Увогуле, PlusCal можа дапамагчы пераадолець фобію матэматыкі, яго лёгка зразумець нават праграмістам і computer scientists. У мінулым я нейкі час (каля 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