Þetta er þýðingargrein . En þar á undan er stutt kynning. Hvernig myndast zombie? Allir hafa lent í aðstæðum þar sem þeir vilja koma vini eða samstarfsmanni upp á sitt stig, en það gengur ekki upp. Þar að auki, "það gengur ekki upp" ekki svo mikið fyrir þig, heldur fyrir hann: á annarri hlið skalans eru eðlileg laun, verkefni og svo framvegis, og á hinni er þörfin fyrir að hugsa. Hugsun er óþægileg og sársaukafull. Hann gefst fljótt upp og heldur áfram að skrifa kóða án þess að nota heilann. Þú áttar þig á því hversu mikla áreynslu það þarf til að yfirstíga hindrun lærðs hjálparleysis og þú gerir það einfaldlega ekki. Svona myndast uppvakningar sem virðast vera hægt að lækna, en svo virðist sem enginn muni gera þetta.
Þegar ég sá það (já, þessi sami vinur úr kennslubókunum) og er ekki að gefa skýrslu, heldur spurninga-og-svar fundur, ég var svolítið varkár. Svona til öryggis, Leslie er heimsþekktur vísindamaður, höfundur frumkvöðlaverka í dreifðri tölvuvinnslu, og þú gætir líka þekkt hann með stöfunum La í LaTeX - "Lamport TeX". Annað ógnvekjandi atriðið er krafan hans: allir sem koma verða (alveg ókeypis) að hlusta á nokkrar skýrslur hans fyrirfram, koma með að minnsta kosti eina spurningu um þær og koma þá fyrst. Ég ákvað að sjá hvað Lamport var að senda út þarna - og það er frábært! Þetta er nákvæmlega þessi hlutur, töfralinkpilla til að meðhöndla zombie. Ég vara þig við: textinn gæti brennt alvarlega þá sem elska ofur-lipur aðferðafræði og sem líkar ekki að prófa það sem þeir hafa skrifað.
Eftir habrokatið hefst eiginlega þýðing málþingsins. Njóttu þess að lesa!
Hvaða verkefni sem þú tekur að þér þarftu alltaf að fara í gegnum þrjú skref:
- ákveða hvaða markmið þú vilt ná;
- ákveða hvernig nákvæmlega þú munt ná markmiði þínu;
- ná markmiði þínu.
Þetta á líka við um forritun. Þegar við skrifum kóða þurfum við:
- ákveða hvað forritið ætti að gera nákvæmlega;
- ákvarða nákvæmlega hvernig það ætti að framkvæma verkefni sitt;
- skrifaðu viðeigandi kóða.
Síðasta skrefið er auðvitað mjög mikilvægt, en ég ætla ekki að tala um það í dag. Í staðinn munum við ræða fyrstu tvo. Sérhver forritari framkvæmir þær áður en byrjað er að vinna. Þú sest ekki niður til að skrifa nema þú hafir ákveðið hvað þú ert að skrifa: vafra eða gagnagrunn. Ákveðin hugmynd um markmiðið verður að vera til staðar. Og þú hugsar örugglega um hvað nákvæmlega forritið mun gera og skrifar það ekki af tilviljun í von um að kóðinn sjálfur muni einhvern veginn breytast í vafra.
Hvernig nákvæmlega gerist þessi forhugsun um kóða? Hversu mikið ættum við að leggja í þetta? Það veltur allt á því hversu flókið vandamálið við erum að leysa. Segjum að við viljum skrifa bilanaþolið dreift kerfi. Í þessu tilfelli ættum við að hugsa hlutina vandlega áður en við setjumst niður til að kóða. Hvað ef við þurfum bara að hækka heiltölubreytu um 1? Við fyrstu sýn er hér allt léttvægt og ekki þörf á umhugsun, en svo minnumst við að yfirfall getur orðið. Þess vegna, jafnvel til að skilja hvort vandamál er einfalt eða flókið, þarftu fyrst að hugsa.
Ef þú hugsar í gegnum mögulegar lausnir á vandamáli fyrirfram geturðu forðast mistök. En þetta krefst þess að hugsun þín sé skýr. Til að ná þessu þarftu að skrifa niður hugsanir þínar. Ég elska Dick Guindon tilvitnunina: „Þegar þú skrifar sýnir náttúran þér hversu slök hugsun þín er. Ef þú skrifar ekki heldurðu bara að þú sért að hugsa. Og þú þarft að skrifa niður hugsanir þínar í formi forskrifta.
Forskriftir þjóna mörgum aðgerðum, sérstaklega í stórum verkefnum. En ég mun aðeins tala um eina þeirra: þeir hjálpa okkur að hugsa skýrt. Að hugsa skýrt er mjög mikilvægt og frekar erfitt, svo við þurfum á hjálp að halda hér. Á hvaða tungumáli eigum við að skrifa forskriftir? Almennt séð er þetta alltaf fyrsta spurningin fyrir forritara: á hvaða tungumáli munum við skrifa? Það er ekkert eitt rétt svar: vandamálin sem við leysum eru of fjölbreytt. Fyrir sumt fólk er TLA+ gagnlegt - það er forskriftartungumál sem ég þróaði. Fyrir aðra er þægilegra að nota kínversku. Það fer allt eftir aðstæðum.
Mikilvægari spurningin er: hvernig getum við náð skýrari hugsun? Svar: Við verðum að hugsa eins og vísindamenn. Þetta er hugsunarháttur sem hefur gefist vel á síðustu 500 árum. Í vísindum byggjum við stærðfræðileg líkön af veruleikanum. Stjörnufræði voru kannski fyrstu vísindin í ströngum skilningi þess orðs. Í stærðfræðilíkaninu sem notað er í stjörnufræði birtast himintunglar sem punktar með massa, stöðu og skriðþunga, þó að í raun séu þeir afar flóknir hlutir með fjöll og höf, lægðir og flæði. Þetta líkan, eins og hvert annað, var búið til til að leysa ákveðin vandamál. Það er frábært til að ákvarða hvert á að beina sjónauka ef þú vilt finna plánetu. En ef þú vilt spá fyrir um veðrið á þessari plánetu, mun þetta líkan ekki virka.
Stærðfræði gerir okkur kleift að ákvarða eiginleika líkans. Og vísindin sýna hvernig þessir eiginleikar tengjast raunveruleikanum. Við skulum tala um vísindin okkar, tölvunarfræði. Raunveruleikinn sem við vinnum með er tölvukerfi af mörgum mismunandi gerðum: örgjörvum, leikjatölvum, tölvum sem keyra forrit og svo framvegis. Ég mun tala um að keyra forrit í tölvu, en í stórum dráttum eiga allar þessar ályktanir við um hvaða tölvukerfi sem er. Í vísindum okkar notum við margar mismunandi gerðir: Turing vélina, að hluta til röð atburða og margar aðrar.
Hvað er forritið? Þetta er hvaða kóða sem er sem hægt er að skoða einn og sér. Segjum að við þurfum að skrifa vafra. Við framkvæmum þrjú verkefni: hanna kynningu notandans á forritinu, skrifa síðan háþróaða skýringarmyndina af forritinu og að lokum skrifa kóðann. Þegar við skrifum kóðann gerum við okkur grein fyrir því að við þurfum að skrifa textasnið. Hér þurfum við aftur að leysa þrjú vandamál: ákvarða hvaða texta þetta tól mun skila; veldu reiknirit fyrir snið; skrifa kóða. Þetta verkefni hefur sitt eigið undirverkefni: að setja bandstrik á réttan hátt í orð. Við leysum þetta undirverkefni líka í þremur skrefum - eins og við sjáum eru þau endurtekin á mörgum stigum.
Lítum nánar á fyrsta skrefið: hvaða vandamál forritið leysir. Hér fyrirmyndum við oftast forrit sem fall sem tekur eitthvað inntak og gefur eitthvað úttak. Í stærðfræði er falli venjulega lýst sem röðuðu setti af pörum. Til dæmis er veldningsfalli fyrir náttúrulegar tölur lýst sem menginu {<0,0>, <1,1>, <2,4>, <3,9>, …}. Skilgreiningarsvið slíkrar falls er mengi fyrstu þátta hvers pars, það er náttúrulegar tölur. Til að skilgreina fall þurfum við að tilgreina lén þess og formúlu.
En föll í stærðfræði eru ekki það sama og föll í forritunarmálum. Stærðfræðin er miklu einfaldari. Þar sem ég hef ekki tíma fyrir flókin dæmi, skulum við íhuga einfalt: fall í C eða kyrrstöðu aðferð í Java sem skilar stærstu sameiginlegu deili tveggja heiltalna. Í forskrift þessarar aðferðar munum við skrifa: reiknar GCD(M,N) fyrir rök M и Nhvar GCD(M,N) - fall þar sem lénið er sett af heiltölupörum og skilagildið er stærsta heiltalan sem er deilt með M и N. Hvernig er raunveruleikinn í samanburði við þetta líkan? Líkanið starfar með heiltölum og í C eða Java höfum við 32 bita int. Þetta líkan gerir okkur kleift að ákveða hvort reikniritið sé rétt GCD, en það kemur ekki í veg fyrir yfirfallsvillur. Til þess þyrfti flóknara líkan, sem enginn tími gefst til.
Við skulum tala um takmarkanir aðgerðarinnar sem fyrirmynd. Sum forrit (eins og stýrikerfi) skila ekki bara tilteknu gildi fyrir ákveðin rök; þau geta keyrt stöðugt. Að auki hentar aðgerðin sem fyrirmynd illa fyrir annað skrefið: að skipuleggja hvernig eigi að leysa vandamálið. Quicksort og bubble sort reikna sömu aðgerðina, en þetta eru gjörólík reiknirit. Þess vegna, til að lýsa leiðinni til að ná markmiði forritsins, nota ég annað líkan, við skulum kalla það staðlað hegðunarlíkan. Forritið er táknað í því sem safn af allri gildri hegðun, sem hvert um sig er röð af ríkjum og ástand er úthlutun gilda á breytur.
Við skulum sjá hvernig annað skrefið fyrir Euclidean algrím myndi líta út. Við þurfum að reikna GCD(M, N). Við frumstillum M sem xOg N sem y, dragðu síðan ítrekað þá minni af þessum breytum frá þeirri stærri þar til þær eru jafnar. Til dæmis, ef M = 12Og N = 18, getum við lýst eftirfarandi hegðun:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Og ef M = 0 и N = 0? Núll er deilanlegt með öllum tölum, þannig að það er enginn stærsti deilirinn í þessu tilviki. Í þessari stöðu þurfum við að fara aftur í fyrsta skrefið og spyrja: þurfum við virkilega að reikna út GCD fyrir ójákvæðar tölur? Ef þetta er ekki nauðsynlegt, þá þarftu bara að breyta forskriftinni.
Hér er rétt að gera stutta útrás um framleiðni. Það er oft mælt í fjölda kóðalína sem skrifaðar eru á dag. En vinnan þín er miklu gagnlegri ef þú losnar við ákveðinn fjölda af línum, því þú hefur minna pláss fyrir pöddur. Og auðveldasta leiðin til að losna við kóða er í fyrsta skrefi. Það er mögulegt að þú þurfir einfaldlega ekki allar bjöllurnar og flauturnar sem þú ert að reyna að framkvæma. Fljótlegasta leiðin til að einfalda forrit og spara tíma er að gera ekki hluti sem ætti ekki að gera. Annað skrefið hefur næsthæstu tímasparnaðarmöguleikana. Ef þú mælir framleiðni í skilmálar af skrifuðum línum, þá mun hugsa um hvernig á að klára verkefni gera þig minna afkastamikill, vegna þess að þú getur leyst sama vandamál með minni kóða. Ég get ekki gefið nákvæma tölfræði hér, vegna þess að ég hef enga leið til að telja fjölda lína sem ég skrifaði ekki vegna tímans sem ég eyddi í forskriftina, það er í fyrsta og öðru skrefi. Og við getum ekki gert tilraun hér heldur, vegna þess að í tilraun höfum við ekki rétt til að klára fyrsta skrefið, verkefnið er ákveðið fyrirfram.
Það er auðvelt að horfa framhjá mörgum erfiðleikum í óformlegum forskriftum. Það er ekkert erfitt að skrifa strangar forskriftir fyrir aðgerðir; ég mun ekki ræða þetta. Í staðinn munum við tala um að skrifa sterkar forskriftir fyrir staðlaða hegðun. Það er til setning sem segir að hægt sé að lýsa hvaða mengi hegðunar sem er með því að nota öryggiseiginleikann (öryggi) og lifunarhæfni (lifandi). Öryggi þýðir að ekkert slæmt mun gerast, forritið mun ekki gefa rangt svar. Lifun þýðir að fyrr eða síðar mun eitthvað gott gerast, þ.e.a.s. forritið mun fyrr eða síðar gefa rétt svar. Að jafnaði er öryggi mikilvægari vísbending, villur eiga sér oftast stað hér. Þess vegna, til að spara tíma, mun ég ekki tala um lifun, þó að það sé auðvitað líka mikilvægt.
Við náum öryggi með því að tilgreina fyrst möguleg upphafsástand. Og í öðru lagi, tengsl við öll möguleg næstu ríki fyrir hvert ríki. Við skulum haga okkur eins og vísindamenn og skilgreina ríki stærðfræðilega. Upphafsástandinu er lýst með formúlunni, til dæmis þegar um er að ræða evklíðsku reikniritið: (x = M) ∧ (y = N). Fyrir ákveðin gildi M и N það er aðeins eitt upphafsástand. Tengslinu við næsta ástand er lýst með formúlu þar sem breytur næsta ástands eru skrifaðar með frumtölu og breytur núverandi ástands eru skrifaðar án frumtölu. Þegar um evklíðsku reikniritið er að ræða, munum við fást við sundrun tveggja formúla, í annarri þeirra x er stærsta gildið, og í öðru - y:
Í fyrra tilvikinu er nýtt gildi y jafnt fyrra gildi y og við fáum nýja gildið á x með því að draga minni breytuna frá þeirri stærri. Í öðru tilvikinu gerum við hið gagnstæða.
Snúum okkur aftur að evklíðsku reikniritinu. Segjum aftur að það M = 12, N = 18. Þetta skilgreinir eitt upphafsástand, (x = 12) ∧ (y = 18). Við stingum síðan þessum gildum inn í formúluna hér að ofan og fáum:
Hér er eina mögulega lausnin: x' = 18 - 12 ∧ y' = 12, og við fáum hegðunina: [x = 12, y = 18]. Á sama hátt getum við lýst öllum ríkjum í hegðun okkar: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Í síðasta ríki [x = 6, y = 6] báðir hlutar tjáningarinnar verða rangir, þess vegna hefur hún ekki næsta ástand. Þannig að við höfum fullkomna forskrift um annað skrefið - eins og við sjáum er þetta alveg venjuleg stærðfræði, eins og hjá verkfræðingum og vísindamönnum, og ekki skrítið, eins og í tölvunarfræði.
Þessar tvær formúlur er hægt að sameina í eina formúlu tímalegrar rökfræði. Það er glæsilegt og auðvelt að útskýra, en það er enginn tími til þess núna. Við gætum þurft tímanlega rökfræði aðeins fyrir eignina lífleika; fyrir öryggi er það ekki þörf. Mér líkar ekki tímarökfræði sem slík, þetta er ekki alveg venjuleg stærðfræði, en ef um lífleika er að ræða er það nauðsynlegt mein.
Í Euclidean algrím fyrir hvert gildi x и y það eru einstök gildi x' и y', sem gera sambandið við næsta ástand satt. Með öðrum orðum, Euclidean reiknirit er ákvarðandi. Til að móta óákveðinn reiknirit verður núverandi ástand að hafa mörg möguleg framtíðarástand og hvert gildi óforsettu breytunnar verður að hafa mörg gildi frumbreytunnar þannig að sambandið við næsta ástand sé satt. Þetta er ekki erfitt að gera, en ég ætla ekki að nefna dæmi núna.
Til að búa til vinnutæki þarftu formlega stærðfræði. Hvernig á að gera forskrift formlega? Til þess þurfum við formlegt tungumál, t.d. . Forskrift evklíðska algrímsins á þessu tungumáli mun líta svona út:
Jafnréttistáknið með þríhyrningi þýðir að gildið vinstra megin við táknið er ákveðið að vera jafnt gildinu hægra megin við táknið. Í meginatriðum er forskrift skilgreining, í okkar tilviki tvær skilgreiningar. Við forskriftina í TLA+ þarftu að bæta við yfirlýsingum og einhverri setningafræði, eins og á glærunni hér að ofan. Í ASCII myndi það líta svona út:
Eins og þú sérð, ekkert flókið. Hægt er að sannreyna forskriftina á TLA+, þ.e.a.s. það er hægt að komast framhjá allri mögulegri hegðun í litlu líkani. Í okkar tilviki mun þetta líkan vera ákveðin gildi M и N. Þetta er mjög áhrifarík og einföld sannprófunaraðferð sem er algjörlega sjálfvirk. Auk þess er hægt að skrifa formlegar sannanir og athuga þær vélrænt, en þetta tekur mikinn tíma, þannig að nánast enginn gerir þetta.
Helsti ókosturinn við TLA+ er að þetta er stærðfræði og forritarar og tölvunarfræðingar eru hræddir við stærðfræði. Við fyrstu sýn hljómar þetta eins og grín, en því miður segi ég þetta í fullri alvöru. Samstarfsmaður minn var bara að segja mér hvernig hann reyndi að útskýra TLA+ fyrir nokkrum hönnuðum. Um leið og formúlurnar birtust á skjánum urðu augu þeirra strax gljáandi. Svo ef TLA+ er skelfilegt geturðu notað , er eins konar leikfangaforritunarmál. Tjáning í PlusCal getur verið hvaða TLA+ tjáning sem er, það er í rauninni hvaða stærðfræðilega tjáning sem er. Að auki hefur PlusCal setningafræði fyrir óákveðin reiknirit. Vegna þess að PlusCal getur skrifað hvaða TLA+ tjáningu sem er, er það verulega tjáningarmeira en nokkurt raunverulegt forritunarmál. Næst er PlusCal sett saman í TLA+ forskrift sem auðvelt er að lesa. Þetta þýðir auðvitað ekki að flókna PlusCal forskriftin muni breytast í einfaldan á TLA+ - bara að samsvörunin á milli þeirra sé augljós, engin frekari flókin birtast. Að lokum er hægt að sannreyna þessa forskrift með TLA+ verkfærum. Almennt séð getur PlusCal hjálpað til við að sigrast á stærðfræðifælni; það er auðvelt að skilja það jafnvel fyrir forritara og tölvunarfræðinga. Ég birti reiknirit á það í nokkurn tíma (um 10 ár) í fortíðinni.
Kannski mun einhver mótmæla því að TLA+ og PlusCal séu stærðfræði og stærðfræði virkar bara með tilbúnum dæmum. Í reynd þarftu raunverulegt tungumál með gerðum, verklagi, hlutum og svo framvegis. Þetta er rangt. Hér er það sem Chris Newcomb, sem starfaði hjá Amazon, skrifar: „Við höfum notað TLA+ í tíu stórum verkefnum og í öllum tilfellum skipti notkun þess verulegan mun á þróun vegna þess að okkur tókst að ná hættulegum villum áður en þær komu í framleiðslu og vegna þess að það gaf okkur innsýn og sjálfstraust sem við þurftum til að gera árásargjarn hagræðingu árangurs án þess að hafa áhrif á sannleika forritsins". Oft heyrir maður að þegar formlegar aðferðir eru notaðar fáum við óhagkvæman kóða - í reynd er allt öfugt. Auk þess ríkir sú skoðun að stjórnendur geti ekki verið sannfærðir um nauðsyn formlegra aðferða, jafnvel þótt forritarar séu sannfærðir um gagnsemi þeirra. Og Newcomb skrifar: „Stjórnendur eru nú að þrýsta á á allan mögulegan hátt að skrifa forskriftir í TLA+ og úthluta sérstaklega tíma fyrir þetta“. Þannig að þegar stjórnendur sjá að TLA+ virkar, þá faðma þeir það. Chris Newcomb skrifaði þetta fyrir um hálfu ári (október 2014) en núna, eftir því sem ég best veit, er TLA+ notað í 14 verkefnum, ekki 10. Annað dæmi tengist hönnun XBox 360. Nemi kom til Charles Thacker og skrifaði forskrift fyrir minniskerfið. Þökk sé þessari forskrift fannst villa sem annars hefði ekki fundist og myndi valda því að hver Xbox 360 hrundi eftir fjögurra klukkustunda notkun. Verkfræðingar frá IBM staðfestu að próf þeirra hefðu ekki greint þessa villu.
Þú getur lesið meira um TLA+ á netinu, en nú skulum við tala um óformlegar forskriftir. Við þurfum sjaldan að skrifa forrit sem reikna minnstu samdeilara og þess háttar. Miklu oftar skrifum við forrit eins og fallega prentara tólið sem ég skrifaði fyrir TLA+. Eftir einföldustu vinnslu myndi TLA+ kóðinn líta svona út:
En í dæminu hér að ofan vildi notandinn líklegast að samtengingar- og jöfnunarmerkin yrðu samræmd. Þannig að rétt snið myndi líta meira svona út:
Við skulum skoða annað dæmi:
Hér var þvert á móti röðun jafnmerkja, samlagningar og margföldunar í upprunanum tilviljunarkennd, þannig að einfaldasta úrvinnslan dugar alveg. Almennt séð er engin nákvæm stærðfræðileg skilgreining á réttu sniði, því „rétt“ þýðir í þessu tilfelli „það sem notandinn vill,“ og það er ekki hægt að ákvarða það stærðfræðilega.
Það virðist sem ef við höfum ekki skilgreiningu á sannleika, þá er forskriftin gagnslaus. En það er ekki satt. Þó að við vitum ekki hvað forrit á að gera þýðir það ekki að við þurfum ekki að hugsa um hvernig það ætti að virka – þvert á móti ættum við að eyða enn meiri vinnu í það. Forskriftin er sérstaklega mikilvæg hér. Það er ómögulegt að ákvarða ákjósanlegasta forritið fyrir skipulagða prentun, en það þýðir ekki að við ættum alls ekki að ráðast í það og að skrifa kóða sem meðvitundarstraum er ekki raunin. Ég endaði á því að skrifa forskrift með sex reglum með skilgreiningum í formi athugasemda í Java skrá. Hér er dæmi um eina af reglunum: a left-comment token is LeftComment aligned with its covering token. Þessi regla er skrifuð á, við skulum segja, stærðfræðilegri ensku: LeftComment aligned, left-comment и covering token — hugtök með skilgreiningum. Þannig lýsa stærðfræðingar stærðfræði: þeir skrifa skilgreiningar á hugtökum og búa til reglur út frá þeim. Ávinningurinn af þessari forskrift er að sex reglur eru mun auðveldari að skilja og kemba en 850 línur af kóða. Ég verð að segja að það var ekki auðvelt að skrifa þessar reglur; það tók töluverðan tíma að kemba þær. Ég skrifaði kóða sérstaklega í þessum tilgangi sem sagði mér hvaða reglu var verið að nota. Vegna þess að ég prófaði þessar sex reglur með nokkrum dæmum þurfti ég ekki að kemba 850 línur af kóða og það var frekar auðvelt að finna villurnar. Java hefur frábær verkfæri fyrir þetta. Ef ég hefði bara skrifað kóðann hefði það tekið mig miklu lengri tíma og sniðið hefði verið af lakari gæðum.
Af hverju var ekki hægt að nota formlega forskrift? Annars vegar er rétt framkvæmd ekki of mikilvæg hér. Skipulögð útprentun hlýtur að vera ófullnægjandi fyrir suma, svo ég þurfti ekki að fá hana til að virka rétt við allar óvenjulegar aðstæður. Enn mikilvægara er sú staðreynd að ég var ekki með fullnægjandi verkfæri. TLA+ módelafgreiðslumaðurinn er ónýtur hér, svo ég þyrfti að skrifa dæmin í höndunum.
Tilgreind forskrift hefur eiginleika sem eru sameiginlegir öllum forskriftum. Það er hærra stig en kóða. Það er hægt að útfæra það á hvaða tungumáli sem er. Það eru engin tæki eða aðferðir til að skrifa það. Ekkert forritunarnámskeið mun hjálpa þér að skrifa þessa forskrift. Og það eru engin verkfæri sem gætu gert þessa forskrift óþarfa, nema auðvitað að þú sért að skrifa tungumál sérstaklega til að skrifa skipulögð útprentunarforrit í TLA+. Að lokum segir þessi forskrift ekkert um nákvæmlega hvernig við munum skrifa kóðann, hún segir bara hvað kóðinn gerir. Við skrifum forskrift til að hjálpa okkur að hugsa í gegnum vandamálið áður en við byrjum að hugsa um kóðann.
En þessi forskrift hefur einnig eiginleika sem aðgreina hana frá öðrum forskriftum. 95% annarra forskrifta eru miklu styttri og einfaldari:
Ennfremur er þessi forskrift sett af reglum. Þetta er venjulega merki um lélega forskrift. Það er frekar erfitt að skilja afleiðingar setts reglna og þess vegna þurfti ég að eyða miklum tíma í að kemba þær. Hins vegar, í þessu tilfelli, gat ég ekki fundið betri leið.
Það er þess virði að segja nokkur orð um forrit sem keyra stöðugt. Venjulega starfa þau samhliða, svo sem stýrikerfi eða dreifð kerfi. Örfáir geta skilið þau í huganum eða á blaði og ég er ekki einn af þeim þó ég hafi einu sinni getað það. Þess vegna þurfum við verkfæri sem athuga vinnu okkar - til dæmis TLA+ eða PlusCal.
Af hverju þurfti ég að skrifa forskrift ef ég vissi nú þegar hvað kóðinn ætti að gera? Reyndar hélt ég bara að ég vissi það. Þar að auki, með forskrift til staðar, þarf utanaðkomandi ekki lengur að skoða kóðann til að skilja hvað hann gerir nákvæmlega. Ég hef reglu: það eiga ekki að vera almennar reglur. Það er undantekning frá þessari reglu að sjálfsögðu, þetta er eina almenna reglan sem ég fylgi: forskriftin á því hvað kóðinn gerir ætti að segja fólki allt sem það þarf að vita þegar það notar kóðann.
Svo hvað nákvæmlega þurfa forritarar að vita um hugsun? Til að byrja með, það sama og fyrir alla: ef þú skrifar ekki, þá virðist þér bara vera að hugsa. Einnig þarftu að hugsa áður en þú kóðar, sem þýðir að þú þarft að skrifa áður en þú kóðar. Forskrift er það sem við skrifum áður en við byrjum að kóða. Forskrift er nauðsynleg fyrir hvaða kóða sem er hægt að nota eða breyta af hverjum sem er. Og þessi „einhver“ gæti reynst höfundur kóðans mánuði eftir að hann var skrifaður. Forskrift er nauðsynleg fyrir stór forrit og kerfi, fyrir flokka, fyrir aðferðir og stundum jafnvel fyrir flókna hluta einni aðferð. Hvað nákvæmlega ættir þú að skrifa um kóðann? Þú þarft að lýsa því hvað það gerir, það er eitthvað sem getur verið gagnlegt fyrir alla sem nota þennan kóða. Stundum getur líka verið nauðsynlegt að tilgreina hvernig nákvæmlega kóðinn nær markmiði sínu. Ef við fórum í gegnum þessa aðferð í algrímanáminu, þá köllum við það reiknirit. Ef það er eitthvað sérhæfðara og nýtt, þá köllum við það hönnun á háu stigi. Það er enginn formlegur munur hér: bæði eru óhlutbundin líkön af forritinu.
Hvernig nákvæmlega ættir þú að skrifa kóðaforskrift? Aðalatriðið: það ætti að vera einu stigi hærra en kóðinn sjálfur. Það verður að lýsa ástandi og hegðun. Það ætti að vera eins strangt og verkefnið krefst. Ef þú ert að skrifa forskrift um hvernig á að útfæra verkefni, þá er hægt að skrifa það í gervikóða eða nota PlusCal. Þú þarft að læra að skrifa forskriftir með formlegum forskriftum. Þetta mun veita þér nauðsynlega færni sem mun einnig hjálpa við óformlega. Hvernig geturðu lært að skrifa formlegar forskriftir? Þegar við lærðum að forrita skrifuðum við forrit og kemdum síðan í villu. Sama hlutur hér: þú þarft að skrifa forskrift, athuga það með módelafgreiðslumanni og laga villurnar. TLA+ er kannski ekki besta tungumálið fyrir formlega forskrift og annað tungumál myndi líklega henta betur fyrir sérstakar þarfir þínar. Það frábæra við TLA+ er að það gerir frábært starf við að kenna stærðfræðilega hugsun.
Hvernig á að tengja forskrift og kóða? Nota athugasemdir sem tengja saman stærðfræðileg hugtök og útfærslu þeirra. Ef þú vinnur með línurit, þá muntu á forritastigi hafa fylki af hnútum og fylki af tenglum. Svo þú þarft að skrifa nákvæmlega hvernig línuritið er útfært með þessum forritunarmannvirkjum.
Það skal tekið fram að ekkert af ofangreindu á við um ferlið við að skrifa kóða sjálft. Þegar þú skrifar kóða, það er að gera þriðja skrefið, þarftu líka að hugsa og hugsa í gegnum forritið. Ef undirverkefni reynist flókið eða ekki augljóst þarf að skrifa forskrift fyrir það. En ég er ekki að tala um kóðann sjálfan hér. Þú getur notað hvaða forritunarmál sem er, hvaða aðferðafræði sem er, þetta snýst ekki um þau. Ekkert af ofangreindu útilokar líka þörfina á að prófa og kemba kóðann þinn. Jafnvel þótt abstrakt líkanið sé rétt skrifað, gætu verið gallar í útfærslu þess.
Að skrifa forskriftir er viðbótarskref í kóðunarferlinu. Þökk sé því er hægt að grípa margar villur með minni fyrirhöfn - við vitum þetta af reynslu forritara frá Amazon. Með forskriftum verða gæði forrita meiri. Svo hvers vegna förum við svo oft án þeirra? Vegna þess að það er erfitt að skrifa. En það er erfitt að skrifa, því til þess þarf að hugsa og hugsunin er líka erfið. Það er alltaf auðveldara að láta eins og þú sért að hugsa. Hér er hægt að draga upp líkingu við hlaup - því minna sem þú hleypur, því hægar hleypur þú. Þú þarft að þjálfa vöðvana og æfa þig í að skrifa. Það þarf æfingu.
Forskriftin gæti verið röng. Þú gætir hafa gert mistök einhvers staðar, eða kröfurnar gætu hafa breyst eða það gæti þurft að bæta úr. Öllum kóða sem einhver notar þarf að breyta, svo fyrr eða síðar mun forskriftin ekki lengur passa við forritið. Helst, í þessu tilfelli, þarftu að skrifa nýja forskrift og endurskrifa kóðann alveg. Við vitum vel að enginn gerir þetta. Í reynd plástum við kóðann og uppfærum kannski forskriftina. Ef þetta hlýtur að gerast fyrr eða síðar, hvers vegna þá að skrifa forskriftir? Í fyrsta lagi, fyrir þann sem mun breyta kóðanum þínum, mun hvert aukaorð í forskriftinni vera gulls virði og þessi manneskja gæti vel verið þú. Ég sparka oft í sjálfan mig fyrir að vera ekki nógu nákvæm þegar ég breyti kóðanum mínum. Og ég skrifa fleiri forskriftir en kóða. Þess vegna, þegar þú breytir kóðanum, þarf alltaf að uppfæra forskriftina. Í öðru lagi, með hverri breytingu verður kóðinn verri, það verður erfiðara að lesa og viðhalda honum. Þetta er aukning á óreiðu. En ef þú byrjar ekki með forskrift, þá verður hver lína sem þú skrifar breyting og kóðinn verður fyrirferðarmikill og erfitt að lesa frá upphafi.
Sem sagt , engin orrusta var unnin samkvæmt áætlun, og engin orrusta vannst án áætlunar. Og hann vissi eitthvað um bardaga. Það er skoðun að það sé tímasóun að skrifa forskriftir. Stundum er þetta rétt og verkefnið er svo einfalt að það þýðir ekkert að hugsa það til enda. En þú ættir alltaf að muna að þegar þér er ráðlagt að skrifa ekki forskriftir þýðir það að þér er ráðlagt að hugsa ekki. Og þú ættir að hugsa um þetta í hvert skipti. Að hugsa í gegnum verkefni tryggir ekki að þú gerir ekki mistök. Eins og við vitum fann enginn upp töfrasprota og forritun er erfitt verkefni. En ef þú hugsar ekki um verkefnið ertu viss um að þú gerir mistök.
Þú getur lesið meira um TLA+ og PlusCal á sérstakri vefsíðu, þú getur farið þangað af heimasíðunni minni . Þetta er allt fyrir mig, takk fyrir athyglina.
Vinsamlegast mundu að þetta er þýðing. Þegar þú skrifar athugasemdir skaltu muna að höfundurinn mun ekki lesa þær. Ef þú vilt virkilega spjalla við höfundinn verður hann á Hydra 2019 ráðstefnunni sem haldin verður 11. – 12. júlí 2019 í St. Hægt er að kaupa miða .
Heimild: www.habr.com