See artikkel on tõlge . Kuid enne seda väike sissejuhatus. Kuidas tekivad zombid? Igaüks on sattunud olukorda, kus tahaks tõsta sõbra või kolleegi oma tasemele, aga ei õnnestu. Ja see "ei õnnestu" pole mitte niivõrd sinust, kuivõrd temast: ühel kaalul on normaalne palk, ülesanded ja nii edasi, teisel - vajadus mõelda. Mõelda on ebamugav ja valus. Ta loobub kiiresti ja jätkab koodi kirjutamist, mitte oma aju täiesti kaasates. Sa kujutad ette, kui palju energiat on vaja, et ületada õppinud abituse barjäär, ja lihtsalt ei tee seda. Nii tekivad zombid, keda võiks nagu ravida, kuid samas ei paista kellelgi selle kallal töötamise soov.
Kui ma nägin, et (jah, jah, see sama tegelane õpikutes) ja teeb ta mitte ettekande, vaid küsimuste ja vastuste sessiooni, ma olin natuke ettevaatlik. Igaks juhuks, Leslie on maailmakuulus teadlane, kes on välja andnud olulisi töid hajutatud arvutustes, ja te võite teda tunda ka La tähtede järgi sõnas LaTeX — "Lamport TeX". Teine ettevaatlikkuse põhjustaja on tema nõudmine: igaühel, kes tuleb, peab (täiesti tasuta) eelnevalt kuulama paar tema ettekannet, välja mõtlema vähemalt ühe küsimuse ja alles siis võib tulla. Otsustasin vaadata, mida Lamport räägib — ja see on suurepärane! See on täpselt see asi, maagiline linktablet, mis ravib zombiteadlikkust. Hoiatab: tekst võib tõsiselt ärritada neid, kes armastavad ülimoodi metoodikaid ja neid, kes ei armasta testida kirjutatut.
Pärast habroki algab tõeliselt seminar. Head lugemist!
Olgu mis tahes ülesanne, millega te tegelete, peate alati läbima kolm sammu:
- otsustada, millist eesmärki soovite saavutada;
- otsustada, kuidas te oma eesmärgi saavutate;
- jõuda oma eesmärgini.
See kehtib ka programmeerimise kohta. Kui kirjutame koodi, peab meil olema:
- otsustada, mida programm täpselt tegema peab;
- määra, kuidas see täpselt oma ülesannet täitma peab;
- kirjutada vastav kood.
Viimane samm on muidugi väga oluline, kuid sellest ma täna rääkida ei kavatse. Selle asemel arutame esimest kahte. Need peab iga programmeerija tegema enne, kui ta tööle asub. Te ei istu kirjutama, kui te ei ole otsustanud, mida täpselt kirjutate: kas brauserit või andmebaasi. Kindel arusaam eesmärgist peab olema olemas. Ja te peaksite kindlasti mõtlema, mida programm tegelikult tegema hakkab, mitte kirjutama ükskõikselt, lootes, et kood aina kuidagi muutub brauseriks.
Kuidas täpselt toimub koodi eelnev mõtlemine? Kui palju pingutusi peaksime selleks kulutama? Kõik sõltub sellest, kui keerulist probleemi me lahendame. Oletame, et tahame kirjutada tõrkeõhtiva jagatud süsteemi. Sellisel juhul peaksime kõike korralikult läbi mõtlema enne koodi kirjutamist. Aga kui peame lihtsalt täisarvu muutma ühe võrra? Esmapilgul tundub see triviaalne ja ei vajaks mingit mõtlemist, kuid siis meenutame, et võib tekkida ülevool. Seega, isegi et mõista, kas probleem on lihtne või keeruline, tuleb alguses mõelda.
Kui kaaluda võimalikke lahendusi probleemile eelnevalt, on võimalik vältida vigu. Kuid selleks peab teie mõtlemine olema selge. Selle saavutamiseks on oluline oma mõtted kirja panna. Mulle meeldib väga Dick Hindoni tsitaat: «Kui sa kirjutad, näitab loodus sulle, kui hoolimatu on su mõtlemine.» Kui sa ei kirjuta, tundub lihtsalt, et sa mõtled. Oma mõtted tuleb kirja panna spetsifikatsioonide vormis.
Spetsifikatsioonid täidavad mitmeid funktsioone, eriti suurtes projektides. Aga ma räägin ainult ühest neist: nad aitavad meil selgelt mõelda. Selgelt mõelda on äärmiselt oluline ja suhteliselt keeruline, seega vajame siin igasuguseid abivahendeid. Millisel keeles peaksime spetsifikatsioone kirjutama? See on alati esmane küsimus programmeerijatele: millisel keeles me kirjutame. Õiget vastust sellele ei ole: lahendatavad probleemid on liiga mitmekesised. Mõne jaoks on kasulik TLA+ — see on spetsifikatsioone keel, mille ma olen välja arendanud. Teiste jaoks on mugavam kasutada hiina keelt. Kõik sõltub olukorrast.
Olulisem on hoopis teine küsimus: kuidas saavutada selgem mõtlemine? Vastus: me peame mõtlema nagu teadlased. See on mõtteviis, mis on viimase 500 aasta jooksul tõeliselt tõhusaks osutunud. Teaduses ehitame me matemaatilisi mudeleid reaalsusest. Astronoomia oli ilmselt esimene teadus sellises ranged tähenduses. Astronoomias kasutatav matemaatiline mudel kujutab taevakehasid punktidena, millel on mass, asukoht ja impulss, kuigi tegelikkuses on need äärmiselt keerulised objektid, millel on mäed ja ookeanid, ning tõusud ja mõõnad. See mudel, nagu kõik muudki, on loodud teatud probleemide lahendamiseks. See sobib suurepäraselt selleks, et määrata, kuhu teleskoop suunata, kui on vaja leida planeet. Kuid kui soovite sellel planeedil ilmaprognoosi ennustada, siis see mudel ei sobi.
Matemaatika võimaldab meil määratleda mudeli omadusi. Ja teadus näitab, kuidas need omadused reaalsusega seonduvad. Räägime meie teadusest, arvutiteadusest. Reaalsus, millega me tegeleme, on erinevat tüüpi arvutuslikud süsteemid: protsessorid, mängukonsoolid, arvutid, mis täidavad programme ja nii edasi. Ma räägin programmi täitmisest arvutis, kuid suures osas kehtivad kõik need järeldused igasuguste arvutuslike süsteemide kohta. Meie teaduses kasutame mitmesuguseid erinevaid mudeleid: Turingi masin, osaliselt järjestatud sündmuste kogumid ja palju muud.
Mis on programm? See on igasugune kood, mida saab käsitleda iseseisvana. Oletame, et peame kirjutama brauseri. Täidame kolm ülesannet: projekteerime programmi esituse kasutajale, seejärel kirjutame programmi kõrgema taseme skeemi ja viimaks kirjutame koodi. Koodi kirjutamise käigus mõistame, et peame kirjutama teksti vormindamise vahendi. Siin peame jälle lahendama kolm ülesannet: määratlema, millist teksti see vahend tagastab; valima vormindamise algoritmi; kirjutama koodi. Sellel ülesandel on oma alamülesanne: õigesti sisestada sidekriips sõnadesse. Lahendame ka selle alamülesande kolme sammuni — nagu näeme, korduvad need paljudel tasanditel.
Vaadake lähemalt esimest sammu: millist probleemi programm lahendab. Siin modelleerime programmi kõige sagedamini kui funktsiooni, mis võtab sisendina mõned andmed ja annab välja mõned tulemused. Matemaatikas kirjeldatakse funktsiooni tavaliselt kui järjestatud paaride kogumit. Näiteks ruutfunktsioon looduslike arvude jaoks on kirjeldatud kogumina {, , , , ...}. Selle funktsiooni määramisala on iga paari esimese elemendi kogum, st looduslikud numbrid. Funktsiooni määratlemiseks peame määrama selle määramisala ja valemi.
Aga funktsioonid matemaatikas ei ole samad, mis funktsioonid programmeerimiskeeltes. Matemaatika on oluliselt lihtsam. Kuna mul pole keerukate näidete jaoks aega, vaatame lihtsat: C keeles olev funktsioon või Java staatiline meetod, mis arvutab kahe täisarvu suurima ühisosa. Selle meetodi spetsifikatsioonis kirjutame: arvutab GCD(M,N) argumentide jaoks M ja N, kus GCD(M,N) — funktsioon, mille määramisala on täisarvude paaride kogum ja tagastatav väärtus on suurim täisarv, mille alusel jagatakse. M ja N. Kuidas see mudel reaalsusega seondub? Mudel opereerib täisarvudega, kuid C või Java's on meil 32-bitine int. See mudel võimaldab meil määrata, kas algoritm on korrektne GCD, kuid see ei takista ülevoolu vigu. Selleks oleks vajalik keerukam mudel, mille loomine ei ole hetkel võimalik.
Räägime funktsiooni piirangutest mudelina. Mõnede programmide (nt operatsioonisüsteemide) töö ei piirdu kindla väärtuse tagastamisega kindlate argumendide jaoks; need võivad töötada pidevalt. Lisaks ei sobi funktsioon mudelina hästi teiseks sammuks: probleemi lahendamise meetodi planeerimiseks. Kiire sorteerimine ja mullisorteerimine arvutavad sama funktsiooni, kuid need on täiesti erinevad algoritmid. Seetõttu kasutan programmi eesmärgi saavutamise viisi kirjeldamiseks teist mudelit, nimetame seda standardseks käitumismudeliks. Programm esitatakse selles kui hulk kõiki lubatud käitumisi, millest igaühel on omakorda seisundite järjekord, ja seisund on muutujate väärtuste määramine.
Vaadakem, kuidas näeb välja teine samm Eukleidese algoritmis. Me peame arvutama GCD(M, N). Me initsialiseerime M kuidas x, ja N kuidas y, seejärel lahutame väiksema neist muutujatest suuremast seni, kuni need on võrdsed. Näiteks, kui M = 12, ja N = 18, saame kirjeldada järgmist käitumist:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Ja kui M = 0 ja N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Siin tasub teha väike kõrvaleheide tootlikkusele. Seda mõõdetakse tihti päeva jooksul kirjutatud koodiridade arvu järgi. Kuid teie töö on oluliselt kasulikum, kui olete vabastanud teatud arvu ridu, sest teil on vähem ruumi vigade jaoks. Ja koodi eemaldamine on kõige lihtsam just esimesel sammul. On täiesti võimalik, et kõik need keerukused, mida proovite rakendada, ei ole teile lihtsalt vajalikud. Kiireim viis programmi lihtsustamiseks ja aja säästmiseks on mitte teha asju, mida pole mõtet teha. Teine samm on teisel kohal ajasäästu potentsiaali poolest. Kui mõõdate tootlikkust kirjutatud ridade arvu järgi, siis ülesande täitmise viisi väljamõtlemine muudab teid vähem tootlikuks, kuna sa saad lahendada sama ülesande vähem kodeerimise mahuga. Ma ei saa siin täpset statistikat esitada, kuna mul pole viisi arvestada neid ridu, mida ma ei kirjutanud, kuna kulutasin aega spetsifikatsioonile, see tähendab esimestele kahele astmele. Ja eksperimenti teha ei saa, sest eksperimentis ei tohi me teha esimest sammu, ülesanne on ette määratud.
Mitteformaalsetes spetsifikatsioonides on lihtne jätta tähelepanuta paljusid raskusi. Ükski rangete spetsifikatsioonide kirjutamine funktsioonide jaoks pole keeruline, sellest ma ei hakka rääkima. Selle asemel räägime rangete spetsifikatsioonide kirjutamisest standardsete käitumismudelite jaoks. On teoreem, mis väidab, et iga käitumiste kogumit saab kirjeldada turvalisuse omadusega (safety) ja elujõulisuse omadusega (liveness). Turvalisus tähendab, et midagi halba ei juhtu, programm ei anna vale vastust. Vastupidavus tähendab, et varem või hiljem juhtub midagi head, st programm lõpuks annab õige vastuse. Üldiselt on turvalisus olulisem näitaja, enim vigu juhtub just siin. Seetõttu ei hakka ma rääkima vastupidavusest, kuigi see on samuti oluline.
Me saavutame turvalisuse, määrates, esiteks, palju võimalikke algolekuid. Ja teiseks, suhted kõigi võimalike järgnevate olekute vahel iga oleku jaoks. Käitume nagu teadlased ja määratleme olekud matemaatiliselt. Algolekute kogum on kirjeldatud valemiga, näiteks, kui rääkida Eukleidese algoritmist: (x = M) ∧ (y = N). Teatud väärtuste korral M ja N olemas ainult üks algolek. Suhted järgmise olekuga on kirjeldatud valemiga, kus järgnevate olekute muutujad on kirjutatud kriipsuga, ja praeguse oleku muutujad ilma kriipsuta. Eukleidese algoritmi puhul käsitleme kahte valemit, milles üks on disjunktsioon. x on suurim väärtus, teine aga — y:
Esimesel juhul on uus y väärtus endise y väärtuse väärtuses, uus x väärtus saadakse, kui lahutame suuremalt muutujalt väiksema. Teisel juhul teeme me vastupidi.
Läheme tagasi Eukleidese algoritmi juurde. Oletame taas, et M = 12, N = 18. See määrab ainulaadse algseisundi, (x = 12) ∧ (y = 18). Siis asendame need väärtused ülaltoodud valemis ja saame:
Siin on ainus võimalik lahendus: x' = 18 - 12 ∧ y' = 12, ja me saame käitumise: [x = 12, y = 18]. Samuti saame kirjeldada kõiki seisundeid meie käitumises: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Viimases olekus [x = 6, y = 6] kumbki väljendi osa on vale, seega pole tal järgmist olekut. Nii et meil on täielik teise sammu spetsifikatsioon — nagu näeme, on see üsna tavaline matemaatika, nagu inseneride ja teadlaste seas, mitte imelik, nagu arvutiteaduses.
Need to combine these two formulas into a single temporal logic formula. It's elegant and easy to explain, but there's no time for that now. Temporal logic may only be necessary for the liveness property, as it's not required for safety. Temporal logic as such is not appealing; it isn't quite standard mathematics, but in the case of liveness, it is a necessary evil.
In Euclid's algorithm for each value x ja y there are unique values x' ja y', which make the relation with the next state true. In other words, Euclid's algorithm is deterministic. To model a nondeterministic algorithm, the current state must have several potential future states, and each unmarked variable must correspond to multiple marked variable values, where the relation with the next state is true. It's not difficult to do, but I won't go into examples right now.
To create a working tool, formal mathematics is needed. How do we create a formal specification? For this, we need a formal language, for example, . Eukliidi algoritmi spetsifikatsioon näeb välja järgmine:
Kolmnurgaga võrdsuse sümbol tähendab, et vasakul oleva väärtuse määratletakse võrdsena paremal oleva väärtusega. Eessõna on tegelikult määratlemine, meie puhul kaks määratlemist. TLA+ spetsifikatsioonile tuleb lisada avaldused ja teatud süntaks, nagu ülaltoodud slaidil. ASCII-s näeb see välja nii:
Nagu näeme, ei ole siin midagi keerulist. TLA+ spetsifikatsiooni saab kontrollida, st kõiki võimalikke käitumisi saab väikese mudeli kaudu jälgida. Meie puhul on see mudel kindlad väärtused M ja N. See on väga efektiivne ja lihtne kontrollimise meetod, mis toimub täielikult automaatselt. Lisaks on võimalik kirjutada formaalseid tõendusmaterjale ja neid mehaaniliselt kontrollida, kuid selleks on vaja palju aega, seega seda peaaegu keegi ei tee.
TLA+ peamine puudus on see, et see on matemaatika, ja programmeerijad ning arvutiteadlased kardavad matemaatikat. Esmapilgul kõlab see nagu nali, kuid kahjuks räägin ma seda täiesti tõsiselt. Minu kolleeg rääkis just, kuidas ta üritas selgitada TLA+ mitmele arendajale. Niipea kui ekraanile ilmusid valemid, said neil kohe klaassilmad. Seega, kui TLA+ hirmutab, võib kasutada , see on omamoodi mänguasi programmeerimise keel. PlusCal'is võib väljend olla iga TLA+ väljend, mis tähendab, et see on põhimõtteliselt iga matemaatiline väljend. Lisaks on PlusCal'is süntaks mittejärjekordsete algoritmide jaoks. Kuna PlusCal'is on võimalik kirjutada iga TLA+ väljend, on see oluliselt väljendusrikkam kui ükski reaalne programmeerimise keel. Edasi, PlusCal kompileeritakse kergesti loetavaks TLA+ spetsifikatsiooniks. See ei tähenda loomulikult, et keeruline PlusCal'i spetsifikatsioon muutub lihtsaks TLA+'ks — lihtsalt vastavus nende vahel on ilmne, lisaprobleeme ei teki. Lõpuks saab seda spetsifikatsiooni kontrollida TLA+ tööriistadega. Ühesõnaga, PlusCal võib aidata ületada matemaatika foobia, seda on lihtne mõista isegi programmeerijatele ja arvutiteadlastele. Minevikus olen ma umbes 10 aastat seda kasutanud algoritmide avaldamiseks.
Võib-olla vaieldakse, et TLA+ ja PlusCal on matemaatika, ja matemaatika töötab ainult välja mõeldud näidetel. Praktikas on aga vajalik reaalne keel, millel on tüübid, protseduurid, objektid jne. See ei saa olla tõsi. Siin on, mida kirjutab Kris Newcomb, kes töötas Amazonis: „Me oleme kasutanud TLA+ kümnes suures projektis ja igal juhul aitas selle kasutamine arenduses oluliselt, kuna suures plansis suutsime püüda ohtlikke vigu enne tootmisse jõudmist, ja see andis meile arusaama ning kindlust, mida vajasime jõudluse agressiivseteks optimeerimisteks, mõjutamata programmi tõelisust.”„Tihti kuuleb, et formaalsete meetodite kasutamine toob kaasa ebatõhusa koodi — praktikas on aga kõik vastupidi. Lisaks arvavad paljud, et juhte on võimatu veenda formaalsete meetodite vajalikkuses, isegi kui arendajad usuvad nende kasulikkusesse. Newcomb kirjutab:” „Juhid tõukavad nüüd igati, et kirjutatakse TLA+ spetsifikatsioone ning eraldavad selleks spetsiaalselt aega.”. Kui juhid näevad, et TLA+ töötab, võtavad nad selle rõõmuga kasutusele. Chris Newcomb kirjutas seda umbes kuus kuud tagasi (2014. aasta oktoobris), ja nüüd, kui ma tean, kasutatakse TLA+ 14 projektis, mitte 10. Teine näide on seotud XBox 360 projekteerimisega. Čarls Teckerile tuli praktikant ja kirjutas mälu süsteemi spetsifikatsiooni. Selle spetsifikatsiooni tõttu leiti viga, mida muidu ei oleks märgatud, ja mille tõttu iga XBox 360 oleks kukkunud pärast nelja tunni kasutamist. IBM-i insenerid kinnitasid, et nende testid ei oleks seda viga tuvastanud.
TLA+ kohta saate rohkem lugeda internetis, aga nüüd rääkigem mitteformaalsetest spetsifikatsioonidest. Meil on harva vaja kirjutada programme, mis arvutavad väikseimat ühistegurit ja sedasorti. Sageli kirjutame me programme, nagu näiteks TLA+ jaoks kirjutatud struktuurse printimise tööriist (pretty-printer). Pärast kõige lihtsamat töötlemist näeks TLA+ kood välja järgmine:
Kuid antud näites soovis kasutaja tõenäoliselt, et konjunktiivide ja võrdsuse märgid oleksid joondatud. Seega näeks õige vormindamine pigem välja nii:
Vaatame teist näidet:
Siin oli, vastupidiselt, võrdsuse, liitmise ja korrutamise märkide joondamine algses allikas juhuslik, seega piisab täiesti lihtsast töötlemisest. Üldiselt ei ole õige vormindamise täpset matemaatilist määratlust, sest "õige" tähendab sel juhul "selline, nagu kasutaja soovib", ja seda ei saa matemaatiliselt määratleda.
Tundub, et kui meil pole tõelisuse määratlust, siis on spetsifikatsioon kasutu. Kuid see pole nii. Kui me ei tea, mida täpselt programm tegema peab, ei tähenda see, et me ei peaks selle toimimist läbi mõtlema — vastupidi, me peame sellele veel rohkem tähelepanu pöörama. Spetsifikatsioon on siin eriti oluline. Optimaalse programmi määratlemine struktureeritud printimiseks on võimatu, kuid see ei tähenda, et me ei peaks seda üldse proovima, ja koodi kirjutamine nagu vool teadlikkusest pole õige. Lõpuks kirjutasin kuue reegli ja määratlustega spetsifikatsiooni. kommentaaride vormis Java-failis. Siin on näide ühest reeglist: left-comment token on LeftComment, mis on joondatud selle katva tokeniga. See reegel on kirjutatud, ütleme nii, matemaatilises inglise keeles: LeftComment joondatud, left-comment ja katva token — terminid koos definitsioonidega. Nii, nagu matemaatikud matemaatikat kirjeldavad: nad kirjutavad terminite definitsioonid ja nende põhjal — reeglid. Sellise spetsifikatsiooni eeliseks on see, et kuus reeglit on tunduvalt lihtsam mõista ja siluda kui 850 koodirida. Tuleb tunnistada, et nende reeglite kirjutamine ei olnud lihtne, kulus üsna palju aega nende silumiseks. Just selleks kirjutasin koodi, mis teatas, millist reeglit kasutatakse. Tänu sellele, et kontrollisin neid kuut reeglit mitmete näidete põhjal, ei pidanud ma siluma 850 koodirida ja vigade leidmine osutus üsna lihtsaks. Java jaoks on selleks suurepärased tööriistad. Kui ma oleksin lihtsalt koodi kirjutanud, oleks mul selleks palju rohkem aega kulunud ning formaadi kvaliteet oleks olnud halvem.
Miks ei saanud kasutada formaalset spetsifikatsiooni? Ühest küljest ei ole täpsus siin eriti oluline. Struktuurne väljatrükk pahandab kindlasti kedagi, seega ei olnud mul vaja proovida, et see töötaks õigesti kõigis ebatavalistes olukordades. Veelgi olulisem on see, et mul ei olnud adekvaatseid tööriistu. TLA+ mudelite kontrollimise vahend siin on kasutu, seega oleksin pidanud käsitsi näite kirjutama.
Antud spetsifikatsioonil on jooni, mis on ühised kõikidele spetsifikatsioonidele. See on kõrgemal tasemel kui kood. Seda saab rakendada mis tahes keeles. Selle kirjutamiseks pole mingisugused tööriistad või meetodid kasulikud. Ükski programmeerimiskursus ei aita teil seda spetsifikatsiooni kirjutada. Ja ei ole olemas tööriistu, mis võiksid selle spetsifikatsiooni asendamatuks muuta, välja arvatud juhul, kui kirjutate keelt, mis on spetsiaalselt loodud struktuursete väljatrükkide programmeerimiseks TLA+ keeles. Lõpuks ei ütle see spetsifikatsioon midagi selle kohta, kuidas me koodi kirjutame; see osutab ainult sellele, mida see kood teeb. Kirjutame spetsifikatsiooni, et aidata end probleemiga tegelemisel, enne kui hakkame koodi peale mõtlema.
Kuid see spetsifikatsioon omab ka omadusi, mis eristavad seda teistest spetsifikatsioonidest. 95% teistest spetsifikatsioonidest on oluliselt lühemad ja lihtsamad:
Edasi liikudes on see spetsifikatsioon reeglite kogum. Reeglina on see halvasti koostatud spetsifikatsiooni märk. Kogumi tulemuste mõistmine on üsna keeruline, just seetõttu kulutasin sellele palju aega. Siiski, antud juhul ei leidnud ma paremat viisi.
Tasub öelda paar sõna programmide kohta, mis töötavad pidevalt. Üldiselt toimivad need paralleelselt, näiteks operatsioonisüsteemid või jaotatud süsteemid. Neid mõista jälgides või paberil on väga vähestel võimalik, ning mina ei kuulu nende hulka, kuigi kunagi suutsin seda. Seetõttu on vajalikud tööriistad, mis kontrollivad meie tööd — näiteks TLA+ või PlusCal.
Miks oli vaja spetsifikatsiooni kirjutada, kui ma teadis juba, mida kood tegema peaks? Tegelikult tundus mulle lihtsalt, et ma tean seda. Lisaks, olemasoleva spetsifikatsiooni tõttu ei pea välismaalane koodi süvenema, et mõista, mida see täpselt teeb. Mul on reegel: ei tohi olla ühtegi üldist reeglit. Sellel reeglil on muidugi erandid — see on ainus üldine reegel, mida ma järgima pean: koodi tegevuse spetsifikatsioon peab inimestele selgitama kõike, mida nad peavad teadma selle koodi kasutamisel.
Nii et, mida peavad arendajad teadma mõtlemisest? Esiteks, sama, mis igaüks: kui sa ei kirjuta, siis arvad lihtsalt, et sa mõtled. Lisaks tuleb mõelda enne kodeerimist, mis tähendab, et tuleb kirjutada enne kodeerimist. Spetsifikatsioon on see, mida kirjutame enne kodeerimise alustamist. Spetsifikatsioon on vajalik igasuguse koodi jaoks, mida võib keegi kasutada või muuta. Ja see "keegi" võib olla isegi koodi autor kuu pärast selle kirjutamist. Spetsifikatsioon on vajalik suuremate programmide ja süsteemide, klasside, meetodite ja mõnikord isegi keeruliste osade jaoks üksikust meetodist. Mida täpselt peaks koodi kohta kirjutama? Tuleb kirjeldada, mida see teeb, st seda, mis võib olla kasulik igale inimesele, kes seda koodi kasutab. Mõnikord võib ka olla vajalik märkida, kuidas kood oma eesmärki saavutab. Kui me oleme selle meetodi läbinud algoritmide kursusel, nimetame seda algoritmiks. Kui aga tegemist on millegi spetsiifilise ja uuema, siis nimetame seda kõrgtaseme projekteerimiseks. Formaalset erinevust siin ei ole: mõlemad on programmi abstraktne mudel.
Kuidas tuleb koodispetsifikatsiooni kirjutada? Peamine: see peab olema kõrgemal tasemel kui kood ise. See peab kirjeldama olekuid ja käitumisi. See peab olema nii range, kui ülesanne nõuab. Kui kirjutate ülesande rakendamise meetodi spetsifikatsiooni, võib selle kirjutada pseudokoodina või PlusCal abil. Spetsifikatsioonide kirjutamist tuleb õppida formaalsete spetsifikatsioonide põhjal. See annab vajalikud oskused, mis aitavad ka mitteformaalsete kirjutamisel. Kuidas aga õppida kirjutama formaalseid spetsifikatsioone? Kui me õppisime programmeerimist, kirjutasime programme ja seejärel silusid neid. Sama kehtib siin: tuleb kirjutada spetsifikatsioon, kontrollida seda mudeli kontrollimise abivahendiga ja parandada vigu. TLA+ pole võib-olla parim keel formaalse spetsifikatsiooni jaoks, ja teie konkreetsete vajaduste jaoks sobib tõenäoliselt paremini mõni teine keel. TLA+ eelis on see, et see õpetab suurepäraselt matemaatilist mõtlemist.
Kuidas siduda spetsifikatsioon ja kood? Kommentaaride abil, mis seovad matemaatilisi kontseptsioone ja nende rakendusi. Kui töötate graafikutega, siis programmi tasandil on teil sõlmede massiivid ja sidemete massiivid. Seetõttu peate kirjutama, kuidas just graaf rakendatakse nende programmeerimistruktuuridega.
Oluline on märkida, et miski eelnevast ei puuduta koodi kirjutamise protsessi. Kui kirjutate koodi, st sooritate kolmanda sammu, peate ka mõtlema ja programmi läbi mõtlema. Kui alamülesanne osutub keeruliseks või ebaselgeks, peate selle jaoks kirjutama spetsifikatsiooni. Kuid ma ei räägi siin koodist. Võite kasutada mida iganes programmeerimiskeelt või metodoloogiat, jutt pole neist. Lisaks ei vabasta miski eelnevast vajadusest koodi testida ja siluda. Isegi kui abstraktne mudel on õigesti kirjutatud, võivad selle rakenduses olla vead.
Spetsifikatsioonide kirjutamine on lisasamm koodi kirjutamise protsessis. Tänu sellele on võimalik paljusid vigu kergemini tuvastada — me teame seda Amazonist pärit programmeerijate kogemuse põhjal. Spetsifikatsioonide abil tõuseb programmide kvaliteet. Nii et miks me ikkagi tihti ilma nendeta hakkama saame? Sest kirjutamine on keeruline. Ja kirjutamine on keeruline, sest selleks tuleb mõelda, ja mõtlemine on samuti raske. Alati on kergem näida, et mõtled. Siin saab tõmmata paralleeli jooksuga — mida vähem sa jooksed, seda aeglasemalt sa jooksed. Oma lihaseid tuleb treenida ja kirja kirjutamisel harjutada. Praktikat on vaja.
Spetsifikatsioon võib olla vale. Te võisite kuskil eksida või nõuded võisid muutuda või oli vaja teha täiustusi. Iga kood, millega keegi töötab, vajab muutmist, seega lõpuks spetsiifikatsioon ei vasta enam programmile. Ideaalis tuleks sel juhul kirjutada uus spetsifikatsioon ja kogu kood kirjutada ümber. Me teame hästi, et keegi ei tee seda. Praktikas me patšime koodi ja võib-olla värskendame spetsiifikatsiooni. Kui see on vältimatu, siis miks üldse kirjutada spetsifikatsioone? Esiteks, inimese jaoks, kes teie koodi parendab, on iga liigne sõna spetsifikatsioonis kulda väärt, ja see inimene võite olla ka teie ise. Ma sageli karistan end madala spetsifikatsiooniga, kui parendan oma koodi. Ja ma kirjutame rohkem spetsifikatsioone kui koodi. Seega, kui te parendate koodi, tuleb alati spetsifikatsiooni värskendada. Teiseks, iga parendusega kood halveneb, seda on aina raskem lugeda ja hooldada. See on entropia tõus. Kuid kui te ei alusta spetsifikatsioonist, siis iga kirjutatud rida on parendus, ja kood on algusest peale kohmakas ja raskesti loetav.
Nagu ütles , ei ühtki lahingut ei võidetud plaani järgi ja ühtki lahingut ei võidetud ilma plaanita. Ja tal oli lahingute kohta midagi öelda. Arvatakse, et spetsifikatsioonide kirjutamine on tuuleveskitega võitlemine. Vahel on see tõesti nii ja ülesanne on nii lihtne, et pole mõtet seda mõelda. Kuid alati tuleb meeles pidada, et kui soovitatakse spetsifikatsioone mitte kirjutada, tähendab see, et soovitatakse mitte mõelda. Ja selle üle peaks iga kord mõtlema. Ülesande läbimõtlemine ei garanteeri, et te ei eksige. Nagu me teame, pole keegi leiutanud võlupulka ja programmeerimine on keeruline tegevus. Kuid kui te ülesannet ei mõtle läbi, garanteerite, et teete vigu.
Rohkem TLA+ ja PlusCali kohta saab lugeda spetsiaalselt lehelt, sinna pääseb minu kodulehe kaudu . Sellega on mul kõik, aitäh tähelepanu eest.
Tuletan meelde, et see on tõlge. Kui kirjutate kommentaare - pidage meeles, et autor ei loe neid. Kui tõeliselt tahate autoriga suhelda, siis ta on konverentsil Hydra 2019, mis toimub 11.-12. juulil 2019 Peterburis. Pileteid on võimalik osta .
Allikas: habr.com
