Šis straipsnis yra vertimas . Bet prieš ją maža įžanga. Kaip formuojasi zombiai? Kiekvienas pateko į situaciją, kai nori pakelti draugą ar kolegą į savo lygį, bet tai neišeina. Ir ne tiek su tavimi, kiek su juo „neišeina“: vienoje svarstyklių pusėje yra normalus atlyginimas, užduotys ir panašiai, o kitoje – poreikis galvoti. Mąstymas yra nemalonus ir skausmingas. Jis greitai pasiduoda ir toliau rašo kodą visiškai neįjungdamas smegenų. Įsivaizduoji, kiek pastangų reikia, kad įveiktum išmokto bejėgiškumo barjerą, ir tiesiog to nedarai. Taip formuojasi zombiai, kuriuos, rodos, galima išgydyti, bet panašu, kad niekas to nepadarys.
Kai aš tai pamačiau (taip, tas pats bendražygis iš vadovėlių) ir daro ne reportažą, o klausimų-atsakymų sesiją, buvau šiek tiek atsargus. Tik tuo atveju, Leslie yra visame pasaulyje žinomas mokslininkas, pagrindinių paskirstytojo skaičiavimo darbų autorius, taip pat galite jį pažinti pagal raides La žodyje LaTeX - „Lamport TeX“. Antras nerimą keliantis veiksnys – jo reikalavimas: kiekvienas atėjęs privalo (visiškai nemokamai) iš anksto išklausyti porą jo pranešimų, sugalvoti apie juos bent vieną klausimą ir tik tada ateiti. Nusprendžiau pažiūrėti, ką ten transliuoja Lamportas – ir tai puiku! Būtent tai yra stebuklinga nuorodos piliulė zombiams gydyti. Perspėju: nuo teksto itin lanksčių metodikų mėgėjai ir nemėgstantys tikrinti to, kas parašyta, gali itin perdegti.
Po habrokato, tiesą sakant, prasideda seminaro vertimas. Mėgaukitės skaitymu!
Kad ir kokios užduoties imtumėtės, visada turite atlikti tris veiksmus:
- nuspręsti, kokį tikslą norite pasiekti;
- nuspręsti, kaip pasieksite savo tikslą;
- ateik į savo tikslą.
Tai taip pat taikoma programavimui. Kai rašome kodą, turime:
- nuspręsti, ką programa turi daryti;
- nustatyti, kaip ji turėtų atlikti savo užduotį;
- parašyti atitinkamą kodą.
Paskutinis žingsnis, žinoma, labai svarbus, bet šiandien apie jį nekalbėsiu. Vietoj to, mes aptarsime pirmuosius du. Kiekvienas programuotojas juos atlieka prieš pradėdamas dirbti. Nesėdi rašyti, kol nenusprendei, ar rašai naršyklę, ar duomenų bazę. Turi būti tam tikra tikslo idėja. Ir jūs tikrai pagalvokite, ką tiksliai programa darys, ir nerašykite kažkaip tikėdamiesi, kad kodas kažkaip pavirs naršykle.
Kaip tiksliai vyksta šio kodo išankstinis mąstymas? Kiek pastangų turėtume įdėti į tai? Viskas priklauso nuo to, kiek sudėtingą problemą mes sprendžiame. Tarkime, kad norime parašyti gedimams atsparią paskirstytą sistemą. Tokiu atveju, prieš sėsdami prie kodo, turėtume viską gerai apgalvoti. Ką daryti, jei mums tiesiog reikia padidinti sveikąjį kintamąjį 1? Iš pirmo žvilgsnio čia viskas banalu, ir nereikia galvoti, bet paskui prisimename, kad gali įvykti perpildymas. Todėl net ir norint suprasti, ar problema paprasta, ar sudėtinga, pirmiausia reikia pagalvoti.
Jei iš anksto apgalvosite galimus problemos sprendimus, galite išvengti klaidų. Tačiau tam reikia, kad jūsų mąstymas būtų aiškus. Norėdami tai padaryti, turite užsirašyti savo mintis. Man labai patinka Dicko Guindono citata: „Kai tu rašai, gamta parodo, koks aplaidus tavo mąstymas. Jei nerašote, tik galvojate, kad galvojate. O mintis reikia užrašyti specifikacijų forma.
Specifikacijos atlieka daug funkcijų, ypač dideliuose projektuose. Bet pakalbėsiu tik apie vieną iš jų: jie padeda mums aiškiai mąstyti. Aiškiai mąstyti yra labai svarbu ir gana sunku, todėl čia mums reikia bet kokios pagalbos. Kokia kalba turėtume rašyti specifikacijas? Apskritai tai visada yra pirmasis programuotojų klausimas: kokia kalba rašysime. Vieno teisingo atsakymo į jį nėra: mūsų sprendžiamos problemos yra per daug įvairios. Kai kuriems žmonėms TLA+ yra specifikacijų kalba, kurią sukūriau. Kitiems patogiau naudoti kinų kalbą. Viskas priklauso nuo situacijos.
Svarbesnis kitas klausimas: kaip pasiekti aiškesnį mąstymą? Atsakymas: Turime mąstyti kaip mokslininkai. Tai mąstymo būdas, kuris pasitvirtino per pastaruosius 500 metų. Moksle mes kuriame matematinius tikrovės modelius. Astronomija buvo bene pirmasis mokslas griežtąja to žodžio prasme. Astronomijoje naudojamame matematiniame modelyje dangaus kūnai atrodo kaip taškai, turintys masę, padėtį ir impulsą, nors iš tikrųjų tai yra labai sudėtingi objektai su kalnais ir vandenynais, potvyniais ir potvyniais. Šis modelis, kaip ir bet kuris kitas, buvo sukurtas tam tikroms problemoms spręsti. Tai puikiai tinka norint nustatyti, kur nukreipti teleskopą, jei reikia rasti planetą. Bet jei norite nuspėti orą šioje planetoje, šis modelis neveiks.
Matematika leidžia mums nustatyti modelio savybes. Ir mokslas parodo, kaip šios savybės yra susijusios su tikrove. Pakalbėkime apie mūsų mokslą, informatiką. Realybė, su kuria mes dirbame, yra įvairios kompiuterinės sistemos: procesoriai, žaidimų konsolės, kompiuteriai, vykdančios programas ir pan. Kalbėsiu apie programos paleidimą kompiuteryje, bet apskritai visos šios išvados galioja bet kuriai kompiuterinei sistemai. Savo moksle naudojame daugybę skirtingų modelių: Tiuringo mašiną, iš dalies užsakytus įvykių rinkinius ir daugelį kitų.
Kas yra programa? Tai yra bet koks kodas, kuris gali būti nagrinėjamas atskirai. Tarkime, mums reikia parašyti naršyklę. Atliekame tris užduotis: projektuojame vartotojo vaizdą apie programą, tada parašome aukšto lygio programos diagramą ir galiausiai parašome kodą. Rašydami kodą suprantame, kad turime parašyti teksto formatuotoją. Čia vėl turime išspręsti tris problemas: nustatyti, kokį tekstą grąžins šis įrankis; pasirinkti formatavimo algoritmą; parašyti kodą. Ši užduotis turi savo antrinę užduotį: teisingai įterpti brūkšnelį į žodžius. Šią antrinę užduotį taip pat sprendžiame trimis žingsniais – kaip matote, jie kartojasi daugeliu lygių.
Išsamiau apsvarstykime pirmąjį žingsnį: kokią problemą programa išsprendžia. Čia mes dažniausiai modeliuojame programą kaip funkciją, kuri paima tam tikrą įvestį ir sukuria tam tikrą išvestį. Matematikoje funkcija paprastai apibūdinama kaip tvarkinga porų rinkinys. Pavyzdžiui, natūraliųjų skaičių kvadrato funkcija apibūdinama kaip aibė {<0,0>, <1,1>, <2,4>, <3,9>, …}. Tokios funkcijos sritis yra kiekvienos poros pirmųjų elementų, tai yra natūraliųjų skaičių, rinkinys. Norėdami apibrėžti funkciją, turime nurodyti jos apimtį ir formulę.
Tačiau funkcijos matematikoje nėra tas pats, kas funkcijos programavimo kalbomis. Matematika daug lengvesnė. Kadangi neturiu laiko sudėtingiems pavyzdžiams, panagrinėkime paprastą: funkciją C arba statinį Java metodą, kuris grąžina didžiausią bendrą dviejų sveikųjų skaičių daliklį. Šio metodo specifikacijoje rašysime: skaičiuoja GCD(M,N) už argumentus M и NKur GCD(M,N) - funkcija, kurios domenas yra sveikųjų skaičių porų rinkinys, o grąžinama reikšmė yra didžiausias sveikasis skaičius, kuris dalijasi iš M и N. Kaip šis modelis siejasi su realybe? Modelis veikia sveikaisiais skaičiais, o C arba Java mes turime 32 bitų int. Šis modelis leidžia mums nuspręsti, ar algoritmas yra teisingas GCD, bet tai neapsaugos nuo perpildymo klaidų. Tam reikėtų sudėtingesnio modelio, kuriam nėra laiko.
Pakalbėkime apie funkcijos, kaip modelio, apribojimus. Kai kurios programos (pvz., operacinės sistemos) ne tik grąžina tam tikrą tam tikrų argumentų reikšmę, jos gali veikti nuolat. Be to, funkcija kaip modelis nelabai tinka antrajam žingsniui: planuoti, kaip išspręsti problemą. Greitasis rūšiavimas ir burbulų rūšiavimas apskaičiuoja tą pačią funkciją, tačiau tai yra visiškai skirtingi algoritmai. Todėl norėdamas aprašyti, kaip pasiekiamas programos tikslas, naudoju kitokį modelį, pavadinkime jį standartiniu elgesio modeliu. Jame esanti programa vaizduojama kaip visų leistinų elgsenų rinkinys, iš kurių kiekvienas savo ruožtu yra būsenų seka, o būsena yra reikšmių priskyrimas kintamiesiems.
Pažiūrėkime, kaip atrodytų antrasis Euklido algoritmo žingsnis. Turime paskaičiuoti GCD(M, N). Mes inicijuojame M kaip xIr N kaip y, tada pakartotinai atimkite mažesnįjį iš šių kintamųjų iš didesniųjų, kol jie bus lygūs. Pavyzdžiui, jei M = 12Ir N = 18, galime apibūdinti tokį elgesį:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Ir jei M = 0 и N = 0? Nulis dalijasi iš visų skaičių, todėl šiuo atveju nėra didžiausio daliklio. Esant tokiai situacijai, turime grįžti prie pirmojo žingsnio ir paklausti: ar tikrai reikia skaičiuoti GCD neteigiamiems skaičiams? Jei tai nėra būtina, tereikia pakeisti specifikaciją.
Čia turėtume padaryti nedidelį nukrypimą nuo produktyvumo. Jis dažnai matuojamas per dieną parašytų kodo eilučių skaičiumi. Tačiau jūsų darbas yra daug naudingesnis, jei atsikratote tam tikro skaičiaus eilučių, nes turite mažiau vietos klaidoms. Lengviausias būdas atsikratyti kodo yra pirmasis žingsnis. Visiškai įmanoma, kad jums tiesiog nereikia visų varpų ir švilpukų, kuriuos bandote įgyvendinti. Greičiausias būdas supaprastinti programą ir sutaupyti laiko – nedaryti to, ko nereikėtų daryti. Antrasis žingsnis yra antras pagal galimybes sutaupyti laiko. Jei produktyvumą matuojate pagal parašytas eilutes, tada mąstysite, kaip atlikti užduotį mažiau produktyvus, nes tą pačią problemą galite išspręsti naudodami mažiau kodo. Čia negaliu pateikti tikslios statistikos, nes neturiu galimybės suskaičiuoti, kiek eilučių neparašiau dėl to, kad praleidau laiką prie specifikacijos, tai yra pirmam ir antram žingsniui. Ir eksperimento čia taip pat negalima nustatyti, nes eksperimente mes neturime teisės atlikti pirmojo žingsnio, užduotis yra iš anksto nustatyta.
Neoficialiose specifikacijose lengva nepastebėti daugelio sunkumų. Nėra nieko sunku parašyti griežtas funkcijų specifikacijas, apie tai nekalbėsiu. Vietoj to kalbėsime apie griežtų standartinio elgesio specifikacijų rašymą. Yra teorema, kuri sako, kad bet koks elgsenos rinkinys gali būti aprašytas naudojant saugumo ypatybę (saugumas) ir išgyvenamumo savybės (gyvumas). Saugumas reiškia, kad nieko blogo nenutiks, programa nepateiks neteisingo atsakymo. Išgyvenamumas reiškia, kad anksčiau ar vėliau atsitiks kažkas gero, t.y. programa anksčiau ar vėliau pateiks teisingą atsakymą. Paprastai saugumas yra svarbesnis rodiklis, čia dažniausiai pasitaiko klaidų. Todėl taupydamas laiką nekalbėsiu apie išgyvenamumą, nors tai, žinoma, irgi svarbu.
Mes pasiekiame saugumą, pirmiausia nurodydami galimų pradinių būsenų rinkinį. Ir antra, santykiai su visomis įmanomomis kiekvienos valstybės būsimomis būsenomis. Elkimės kaip mokslininkai ir apibrėžkime būsenas matematiškai. Pradinių būsenų rinkinys aprašomas formule, pavyzdžiui, Euklido algoritmo atveju: (x = M) ∧ (y = N). Tam tikroms vertybėms M и N yra tik viena pradinė būsena. Ryšys su kita būsena apibūdinamas formule, kurioje kitos būsenos kintamieji rašomi su pirminiu, o esamos būsenos kintamieji – be pirminio. Euklido algoritmo atveju nagrinėsime dviejų formulių disjunkciją, iš kurių vienoje x yra didžiausia vertė, o antroje - y:
Pirmuoju atveju nauja y reikšmė lygi ankstesnei y reikšmei, o naują x reikšmę gauname iš didesnio kintamojo atėmę mažesnį kintamąjį. Antruoju atveju elgiamės priešingai.
Grįžkime prie Euklido algoritmo. Dar kartą manykime, kad M = 12, N = 18. Tai apibrėžia vieną pradinę būseną, (x = 12) ∧ (y = 18). Tada mes įtraukiame šias reikšmes į aukščiau pateiktą formulę ir gauname:
Štai vienintelis galimas sprendimas: x' = 18 - 12 ∧ y' = 12ir mes gauname elgesį: [x = 12, y = 18]. Panašiai galime apibūdinti visas savo elgesio būsenas: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Paskutinėje būsenoje [x = 6, y = 6] abi išraiškos dalys bus klaidingos, todėl ji neturi kitos būsenos. Taigi, turime išsamią antrojo žingsnio specifikaciją - kaip matote, tai yra gana įprasta matematika, kaip inžinieriams ir mokslininkams, o ne keista, kaip kompiuterių moksle.
Šios dvi formulės gali būti sujungtos į vieną laiko logikos formulę. Ji elegantiška ir lengvai paaiškinama, bet dabar jai nėra laiko. Laikinosios logikos mums gali prireikti tik gyvumo savybėms, jos nereikia saugumui. Laikinoji logika kaip tokia man nepatinka, tai ne visai eilinė matematika, bet gyvumo atveju tai būtinas blogis.
Euklido algoritme kiekvienai reikšmei x и y turi unikalių vertybių x' и y', dėl kurių ryšys su kita būsena yra tikras. Kitaip tariant, Euklido algoritmas yra deterministinis. Norint modeliuoti nedeterministinį algoritmą, dabartinė būsena turi turėti keletą galimų ateities būsenų ir kad kiekviena neparengta kintamojo reikšmė turėtų kelias pradėtas kintamojo reikšmes, kad ryšys su kita būsena būtų teisingas. Tai lengva padaryti, bet dabar nepateiksiu pavyzdžių.
Norint sukurti darbo įrankį, reikia formalios matematikos. Kaip specifikaciją padaryti formalią? Norėdami tai padaryti, mums reikia oficialios kalbos, pavyzdžiui, . Euklido algoritmo specifikacija šia kalba atrodytų taip:
Lygybės ženklo simbolis su trikampiu reiškia, kad reikšmė, esanti ženklo kairėje, yra lygi reikšmei, esančiai ženklo dešinėje. Iš esmės specifikacija yra apibrėžimas, mūsų atveju du apibrėžimai. Prie TLA+ specifikacijos turite pridėti deklaracijas ir tam tikrą sintaksę, kaip parodyta aukščiau esančioje skaidrėje. ASCII tai atrodytų taip:
Kaip matote, nieko sudėtingo. TLA+ specifikaciją galima išbandyti, ty apeiti visas galimas elgsenas mažame modelyje. Mūsų atveju šis modelis bus tam tikros vertybės M и N. Tai labai efektyvus ir paprastas tikrinimo metodas, kuris yra visiškai automatinis. Taip pat galima rašyti formalius tiesos įrodymus ir patikrinti juos mechaniškai, tačiau tai užima daug laiko, todėl beveik niekas to nedaro.
Pagrindinis TLA+ trūkumas – tai matematika, o programuotojai ir informatikai bijo matematikos. Iš pirmo žvilgsnio tai skamba kaip pokštas, bet, deja, turiu galvoje tai visiškai rimtai. Mano kolega man tiesiog pasakojo, kaip jis bandė paaiškinti TLA+ keliems kūrėjams. Vos tik formulės pasirodė ekrane, jos iškart tapo stiklinėmis akimis. Taigi, jei TLA+ jus gąsdina, galite naudoti , tai savotiška žaislų programavimo kalba. „PlusCal“ išraiška gali būti bet kokia TLA+ išraiška, ty iš esmės bet kokia matematinė išraiška. Be to, „PlusCal“ turi nedeterministinių algoritmų sintaksę. Kadangi „PlusCal“ gali parašyti bet kokią TLA+ išraišką, „PlusCal“ yra daug išraiškingesnė nei bet kuri tikra programavimo kalba. Be to, „PlusCal“ sukompiliuojama į lengvai skaitomą TLA+ specifikaciją. Tai, žinoma, nereiškia, kad sudėtinga „PlusCal“ specifikacija pavirs į paprastą TLA + – tiesiog jų atitikimas akivaizdus, papildomo sudėtingumo nebus. Galiausiai šią specifikaciją galima patikrinti TLA+ įrankiais. Apskritai, „PlusCal“ gali padėti įveikti matematikos fobiją ir yra lengvai suprantama net programuotojams ir kompiuterių mokslininkams. Anksčiau kurį laiką (apie 10 metų) skelbdavau jo algoritmus.
Galbūt kas nors paprieštaraus, kad TLA + ir PlusCal yra matematika, o matematika veikia tik pagal sugalvotus pavyzdžius. Praktiškai reikia tikros kalbos su tipais, procedūromis, objektais ir pan. Tai yra blogai. Štai ką rašo Chrisas Newcombas, dirbęs „Amazon“: „Naudojome TLA+ dešimčiai didelių projektų ir kiekvienu atveju jos naudojimas padarė didelę įtaką plėtrai, nes galėjome sugauti pavojingas klaidas dar prieš pradėdami gaminti, ir tai suteikė mums įžvalgos ir pasitikėjimo. Atlikite agresyvų našumo optimizavimą, nepaveikdami programos tikrovės". Dažnai galima išgirsti, kad naudojant formalius metodus gauname neefektyvų kodą – praktiškai viskas yra visiškai priešingai. Be to, vyrauja nuomonė, kad vadovai negali būti įsitikinę formalių metodų reikalingumu, net jei programuotojai yra įsitikinę jų naudingumu. Ir Newcomb rašo: „Vadovai dabar labai stengiasi rašyti TLA+ specifikacijas ir konkrečiai tam skirti laiko“. Taigi vadovai, pamatę, kad TLA+ veikia, mielai tai priima. Chrisas Newcombas tai parašė maždaug prieš šešis mėnesius (2014 m. spalį), bet dabar, kiek žinau, TLA+ naudojamas 14 projektų, o ne 10. Kitas pavyzdys yra „XBox 360“ konstrukcijoje. Stažuotojas atvyko pas Charlesą Thackerį ir parašė atminties sistemos specifikaciją. Dėl šios specifikacijos buvo rasta klaida, kuri kitu atveju liktų nepastebėta ir dėl kurios kiekvienas „XBox 360“ sugenda po keturių valandų naudojimo. IBM inžinieriai patvirtino, kad jų bandymai šios klaidos nebūtų radę.
Daugiau apie TLA + galite pasiskaityti internete, bet dabar pakalbėkime apie neformalias specifikacijas. Retai tenka rašyti programas, kurios apskaičiuoja mažiausiai bendrą daliklį ir panašiai. Daug dažniau rašome tokias programas kaip gražus spausdintuvo įrankis, kurį parašiau TLA+. Po paprasčiausio apdorojimo TLA + kodas atrodys taip:
Tačiau aukščiau pateiktame pavyzdyje vartotojas greičiausiai norėjo, kad jungtukas ir lygybės ženklai būtų suderinti. Taigi teisingas formatavimas atrodytų taip:
Apsvarstykite kitą pavyzdį:
Čia, priešingai, lygybės, sudėjimo ir daugybos ženklų išlygiavimas šaltinyje buvo atsitiktinis, todėl pakanka paprasčiausio apdorojimo. Apskritai nėra tikslaus matematinio teisingo formatavimo apibrėžimo, nes „teisinga“ šiuo atveju reiškia „ko nori vartotojas“, o to matematiškai nustatyti negalima.
Atrodytų, jei neturime tiesos apibrėžimo, tada specifikacija yra nenaudinga. Bet taip nėra. Tai, kad nežinome, ką programa turi daryti, nereiškia, kad mums nereikia galvoti, kaip ji veikia – priešingai, turime įdėti dar daugiau pastangų. Specifikacija čia ypač svarbi. Neįmanoma nustatyti optimalios struktūrinio spausdinimo programos, tačiau tai nereiškia, kad jos apskritai neturėtume imtis, o kodo rašymas kaip sąmonės srautas nėra geras dalykas. Pabaigoje parašiau šešių taisyklių specifikaciją su apibrėžimais komentarų forma java faile. Štai vienos iš taisyklių pavyzdys: a left-comment token is LeftComment aligned with its covering token. Ši taisyklė parašyta, sakykime, matematine anglų kalba: LeftComment aligned, left-comment и covering token - terminai su apibrėžimais. Taip matematikai apibūdina matematiką: rašo terminų apibrėžimus ir, remdamiesi jais, taisykles. Tokios specifikacijos pranašumas yra tas, kad šešias taisykles yra daug lengviau suprasti ir derinti nei 850 kodo eilučių. Turiu pasakyti, kad parašyti šias taisykles nebuvo lengva, jų derinimas užtruko gana daug laiko. Specialiai šiam tikslui parašiau kodą, kuriame pranešama, kuri taisyklė buvo naudojama. Dėl to, kad išbandžiau šias šešias taisykles keliuose pavyzdžiuose, man nereikėjo derinti 850 kodo eilučių, o klaidas rasti buvo gana lengva. „Java“ turi puikių įrankių tam. Jei tik būčiau parašęs kodą, tai būtų užtrukę daug ilgiau, o formatavimas būtų buvęs prastesnis.
Kodėl negalima naudoti oficialios specifikacijos? Viena vertus, teisingas vykdymas čia nėra labai svarbus. Struktūriniai spaudiniai niekam nepatiks, todėl man nereikėjo, kad jie veiktų tinkamai visose keistose situacijose. Dar svarbiau yra tai, kad neturėjau tinkamų įrankių. TLA+ modelių tikrintuvas čia nenaudingas, todėl pavyzdžius turėčiau rašyti rankiniu būdu.
Aukščiau pateikta specifikacija turi visoms specifikacijoms bendrų savybių. Tai aukštesnis lygis nei kodas. Jis gali būti įgyvendintas bet kuria kalba. Bet kokios priemonės ar metodai yra nenaudingi jį rašant. Joks programavimo kursas nepadės parašyti šios specifikacijos. Ir nėra įrankių, dėl kurių ši specifikacija taptų nereikalinga, nebent, žinoma, rašote kalbą, skirtą struktūrizuotoms spausdinimo programoms rašyti TLA+. Galiausiai šioje specifikacijoje nieko nepasakoma apie tai, kaip tiksliai parašysime kodą, tik nurodoma, ką šis kodas daro. Rašome specifikaciją, kad padėtų mums pagalvoti apie problemą prieš pradedant galvoti apie kodą.
Tačiau ši specifikacija turi ir savybių, išskiriančių ją iš kitų specifikacijų. 95 % kitų specifikacijų yra žymiai trumpesnės ir paprastesnės:
Be to, ši specifikacija yra taisyklių rinkinys. Paprastai tai yra prastos specifikacijos požymis. Suprasti taisyklių rinkinio pasekmes yra gana sunku, todėl turėjau praleisti daug laiko jų derinimui. Tačiau šiuo atveju neradau geresnio būdo.
Verta pasakyti keletą žodžių apie programas, kurios veikia nuolat. Paprastai jie veikia lygiagrečiai, pavyzdžiui, operacinės sistemos arba paskirstytos sistemos. Labai mažai žmonių gali juos suprasti mintyse ar popieriuje, o aš nesu iš jų, nors kažkada galėjau tai padaryti. Todėl mums reikia įrankių, kurie patikrins mūsų darbą – pavyzdžiui, TLA + arba PlusCal.
Kodėl reikėjo rašyti specifikaciją, jei jau žinojau, ką tiksliai kodas turi daryti? Tiesą sakant, aš tiesiog maniau, kad tai žinau. Be to, turint specifikaciją, pašaliniui nebereikia įsigilinti į kodą, kad suprastų, ką tiksliai jis daro. Turiu taisyklę: bendrų taisyklių neturi būti. Žinoma, yra šios taisyklės išimtis, tai vienintelė bendra taisyklė, kurios laikausi: kodo veikimo specifikacija turėtų pasakyti žmonėms viską, ką jie turi žinoti naudodami kodą.
Taigi ką tiksliai programuotojai turi žinoti apie mąstymą? Pradžiai tas pats, kaip ir visi: jei nerašai, tai tau tik atrodo, kad tu galvoji. Be to, prieš koduodami turite pagalvoti, o tai reiškia, kad prieš koduodami turite parašyti. Specifikacija yra tai, ką mes parašome prieš pradėdami koduoti. Specifikacija reikalinga bet kuriam kodui, kurį gali naudoti ar keisti bet kas. Ir šis „kažkas“ gali būti pats kodo autorius praėjus mėnesiui po jo parašymo. Specifikacija reikalinga didelėms programoms ir sistemoms, klasėms, metodams ir kartais net sudėtingoms vieno metodo sekcijoms. Kas tiksliai turėtų būti parašyta apie kodą? Turite apibūdinti, ką jis daro, tai yra, kas gali būti naudinga bet kuriam šį kodą naudojančiam asmeniui. Kartais taip pat gali prireikti nurodyti, kaip kodas pasiekia savo tikslą. Jei mes perėjome šį metodą algoritmų eigoje, vadinsime jį algoritmu. Jei tai kažkas ypatingesnio ir naujo, tai vadiname aukšto lygio dizainu. Formalaus skirtumo čia nėra: abu yra abstraktus programos modelis.
Kaip tiksliai turėtumėte parašyti kodo specifikaciją? Svarbiausia: jis turėtų būti vienu lygiu aukštesnis už patį kodą. Ji turėtų apibūdinti būsenas ir elgesį. Ji turėtų būti tokia griežta, kiek reikalauja užduotis. Jei rašote specifikaciją, kaip užduotis turi būti įgyvendinta, galite ją parašyti pseudokodu arba naudodami PlusCal. Turite išmokti rašyti specifikacijas ant oficialių specifikacijų. Tai suteiks jums reikalingų įgūdžių, kurie padės ir neformaliems. Kaip išmokti rašyti oficialias specifikacijas? Kai išmokome programuoti, rašėme programas ir tada jas derinome. Čia tas pats: parašyk specifikaciją, patikrink su modelio tikrintuvu ir ištaisyk klaidas. TLA+ gali būti ne pati geriausia kalba formaliai specifikacijai, o kita kalba gali būti geresnė jūsų konkretiems poreikiams. TLA+ privalumas yra tas, kad ji labai gerai moko matematinio mąstymo.
Kaip susieti specifikaciją ir kodą? Matematines sąvokas ir jų įgyvendinimą siejančių komentarų pagalba. Jei dirbate su grafikais, tada programos lygiu turėsite mazgų ir nuorodų masyvus. Todėl reikia tiksliai parašyti, kaip grafiką įgyvendina šios programavimo struktūros.
Reikėtų pažymėti, kad nė vienas iš aukščiau išvardytų dalykų netaikomas tikram kodo rašymo procesui. Kai rašote kodą, tai yra, atliekate trečią veiksmą, taip pat turite galvoti ir apgalvoti programą. Jei antrinė užduotis yra sudėtinga arba neaiški, turite parašyti jos specifikaciją. Bet aš čia nekalbu apie patį kodą. Galite naudoti bet kurią programavimo kalbą, bet kokią metodiką, tai ne apie juos. Be to, nė vienas iš aukščiau paminėtų dalykų nepanaikina poreikio išbandyti ir derinti kodą. Net jei abstraktus modelis parašytas teisingai, jo įgyvendinime gali būti klaidų.
Specifikacijų rašymas yra papildomas kodavimo proceso žingsnis. Jo dėka daug klaidų galima užfiksuoti mažiau pastangų – tai žinome iš „Amazon“ programuotojų patirties. Atsižvelgiant į specifikacijas, programų kokybė tampa aukštesnė. Tad kodėl taip dažnai apsieiname be jų? Nes rašyti sunku. Ir rašyti sunku, nes tam reikia galvoti, o mąstyti taip pat sunku. Visada lengviau apsimesti, ką galvoji. Čia galima nubrėžti analogiją su bėgimu – kuo mažiau bėgi, tuo lėčiau. Reikia treniruoti raumenis ir rašyti. Reikia praktikos.
Specifikacija gali būti neteisinga. Galbūt kažkur padarėte klaidą arba pasikeitė reikalavimai, o gal reikėjo patobulinti. Bet koks kodas, kurį kas nors naudoja, turi būti pakeistas, todėl anksčiau ar vėliau specifikacija nebeatitiks programos. Idealiu atveju šiuo atveju turite parašyti naują specifikaciją ir visiškai perrašyti kodą. Puikiai žinome, kad niekas to nedaro. Praktiškai pataisome kodą ir galbūt atnaujiname specifikaciją. Jei anksčiau ar vėliau tai įvyks, kam tada iš viso rašyti specifikacijas? Pirma, asmeniui, kuris redaguos jūsų kodą, kiekvienas papildomas žodis specifikacijoje bus aukso vertės, ir šis asmuo gali būti jūs pats. Dažnai priekaištauju, kad redaguodamas kodą negaunu pakankamai specifikacijų. Ir aš rašau daugiau specifikacijų nei kodo. Todėl, kai redaguojate kodą, specifikaciją visada reikia atnaujinti. Antra, su kiekviena peržiūra kodas blogėja, jį skaityti ir prižiūrėti darosi vis sunkiau. Tai yra entropijos padidėjimas. Bet jei nepradėsite nuo specifikacijos, kiekviena jūsų parašyta eilutė bus redaguojama, o kodas bus nelengvas ir sunkiai skaitomas nuo pat pradžių.
Kaip sakė , nė vienas mūšis nebuvo laimėtas pagal planą ir nė vienas mūšis nebuvo laimėtas be plano. Ir jis ką nors žinojo apie mūšius. Yra nuomonė, kad specifikacijų rašymas yra laiko švaistymas. Kartais tai tiesa, o užduotis yra tokia paprasta, kad nėra apie ką galvoti. Tačiau visada turėtumėte atsiminti, kad kai jums sakoma nerašyti specifikacijų, jums sakoma negalvoti. Ir jūs turėtumėte apie tai galvoti kiekvieną kartą. Užduoties apgalvojimas negarantuoja, kad nepadarysite klaidų. Kaip žinome, stebuklingos lazdelės niekas neišrado, o programuoti – sunki užduotis. Bet jei negalvojate apie problemą, garantuotai padarysite klaidų.
Daugiau apie TLA + ir PlusCal galite perskaityti specialioje svetainėje, ten galite patekti iš mano pagrindinio puslapio . Tai viskas, ačiū už dėmesį.
Atkreipkite dėmesį, kad tai yra vertimas. Rašydami komentarus atminkite, kad autorius jų neskaitys. Jei tikrai norite pabendrauti su autoriumi, tuomet jis bus „Hydra 2019“ konferencijoje, kuri vyks 11 metų liepos 12-2019 dienomis Sankt Peterburge. Bilietus galima įsigyti .
Šaltinis: www.habr.com