See on tõlkeartikkel . Aga enne seda on lühike tutvustus. Kuidas zombisid moodustuvad? Igaüks on leidnud end olukorrast, kus ta soovib sõpra või kolleegi oma tasemele viia, kuid see ei õnnestu. Veelgi enam, "see ei tule välja" mitte niivõrd teile, vaid temale: skaala ühel pool on normaalne palk, ülesanded ja nii edasi ning teisel pool on vajadus mõelda. Mõtlemine on ebameeldiv ja valus. Ta annab kiiresti alla ja jätkab koodi kirjutamist ilma aju üldse kasutamata. Sa mõistad, kui palju pingutust nõuab õpitud abituse barjääri ületamine, ja sa lihtsalt ei tee seda. Nii moodustuvadki zombid, keda näib olevat võimalik ravida, kuid tundub, et seda ei tee keegi.
Kui ma seda nägin (jah, see sama sõber õpikutest) ja ei anna ettekannet, vaid küsimuste-vastuste sessiooni, olin veidi ettevaatlik. Leslie on igaks juhuks maailmas tunnustatud teadlane, hajutatud andmetöötluse põhjapanevate tööde autor ja võite teda LaTeXis La-tähtede järgi tunda – “Lamport TeX”. Teine murettekitav tegur on tema nõue: kõik, kes tulevad, peavad (täiesti tasuta) eelnevalt kuulama paar tema ettekannet, esitama nende kohta vähemalt ühe küsimuse ja alles siis tulema. Otsustasin näha, mida Lamport seal edastab – ja see on suurepärane! See on täpselt see asi, maagiline link-pill zombide raviks. Hoiatan: tekst võib tõsiselt kõrvetada neid, kes armastavad üliagarat metoodikat ja kellele ei meeldi oma kirjutatut testida.
Peale habrokat algab tegelikult ka seminari tõlkimine. Nautige lugemist!
Ükskõik, millise ülesande te ette võtate, peate alati läbima kolm sammu:
- otsustada, millist eesmärki soovid saavutada;
- otsustada, kuidas täpselt oma eesmärgi saavutad;
- jõuda oma eesmärgini.
See kehtib ka programmeerimise kohta. Koodi kirjutamisel vajame:
- otsustada, mida programm täpselt tegema peaks;
- määrata täpselt, kuidas ta peaks oma ülesannet täitma;
- kirjutage sobiv kood.
Viimane samm on muidugi väga oluline, kuid ma ei räägi sellest täna. Selle asemel arutame kahte esimest. Iga programmeerija teeb need enne tööle asumist. Sa ei istu maha kirjutama, kui pole otsustanud, mida kirjutad: brauseris või andmebaasis. Teatud ettekujutus eesmärgist peab olema olemas. Ja kindlasti mõtlete sellele, mida programm täpselt teeb, ja ärge kirjutage seda juhuslikult, lootes, et kood ise muutub kuidagi brauseriks.
Kuidas see koodi eelmõtlemine täpselt toimub? Kui palju peaksime selle nimel pingutama? Kõik sõltub sellest, kui keerulist probleemi me lahendame. Oletame, et tahame kirjutada tõrketaluvusega hajutatud süsteemi. Sel juhul peaksime enne kodeerima asumist asjad hoolikalt läbi mõtlema. Mis siis, kui peame lihtsalt täisarvu muutujat 1 võrra suurendama? Esmapilgul on siin kõik tühine ja pole vaja mõelda, kuid siis meenub, et võib tekkida ülevool. Seega, isegi selleks, et mõista, kas probleem on lihtne või keeruline, tuleb kõigepealt mõelda.
Kui mõtlete probleemile eelnevalt läbi võimalikud lahendused, saate vigu vältida. Kuid see nõuab, et teie mõtlemine oleks selge. Selle saavutamiseks peate oma mõtted kirja panema. Mulle meeldib Dick Guindoni tsitaat: "Kui kirjutate, näitab loodus teile, kui lohakas on teie mõtlemine." Kui sa ei kirjuta, siis arvad vaid, et mõtled. Ja peate oma mõtted spetsifikatsioonide kujul kirja panema.
Spetsifikatsioonid täidavad paljusid funktsioone, eriti suurte projektide puhul. Kuid ma räägin neist ainult ühest: need aitavad meil selgelt mõelda. Selgelt mõtlemine on väga oluline ja üsna raske, seega vajame siin igasugust abi. Mis keeles peaksime spetsifikatsioonid kirjutama? Üldiselt on see programmeerijate jaoks alati esimene küsimus: mis keeles me kirjutame? Ühte õiget vastust pole: meie lahendatavad probleemid on liiga erinevad. Mõne inimese jaoks on TLA+ minu välja töötatud spetsifikatsioonikeel. Teiste jaoks on mugavam kasutada hiina keelt. Kõik oleneb olukorrast.
Olulisem küsimus on: kuidas saavutada selgem mõtlemine? Vastus: Me peame mõtlema nagu teadlased. See on mõtteviis, mis on viimase 500 aasta jooksul hästi toiminud. Teaduses ehitame reaalsuse matemaatilisi mudeleid. Astronoomia oli võib-olla esimene teadus selle sõna otseses tähenduses. Astronoomias kasutatavas matemaatilises mudelis paistavad taevakehad massi, asukoha ja impulsiga punktidena, kuigi tegelikkuses on tegemist äärmiselt keerukate objektidega mägede ja ookeanide, mõõnade ja voogudega. See mudel, nagu iga teine, loodi teatud probleemide lahendamiseks. See on suurepärane, et määrata, kuhu teleskoop suunata, kui soovite planeeti leida. Aga kui soovite ennustada ilma selle planeedi kohta, siis see mudel ei tööta.
Matemaatika võimaldab meil määrata mudeli omadusi. Ja teadus näitab, kuidas need omadused on tegelikkusega seotud. Räägime oma teadusest, arvutiteadusest. Reaalsus, millega me töötame, on mitut erinevat tüüpi arvutisüsteemid: protsessorid, mängukonsoolid, programme käitavad arvutid jne. Ma räägin programmi käivitamisest arvutis, kuid üldiselt kehtivad kõik need järeldused iga arvutisüsteemi kohta. Oma teaduses kasutame palju erinevaid mudeleid: Turingi masin, osaliselt järjestatud sündmuste komplektid ja paljud teised.
Mis on programm? See on mis tahes kood, mida saab käsitleda eraldi. Oletame, et peame kirjutama brauseri. Teostame kolme ülesannet: kujundame programmi kasutajapoolse esitluse, seejärel kirjutame programmi kõrgetasemelise diagrammi ja lõpuks kirjutame koodi. Koodi kirjutades mõistame, et peame kirjutama tekstivormingu. Siin peame taas lahendama kolm probleemi: määrake, millise teksti see tööriist tagastab; valige vormindamise algoritm; kirjutada kood. Sellel ülesandel on oma alamülesanne: sidekriipsude õige sisestamine sõnadesse. Ka selle alamülesande lahendame kolmes etapis – nagu näeme, korduvad need mitmel tasandil.
Vaatame lähemalt esimest sammu: millise probleemi programm lahendab. Siin modelleerime kõige sagedamini programmi funktsioonina, mis võtab teatud sisendi ja annab väljundi. Matemaatikas kirjeldatakse funktsiooni tavaliselt kui järjestatud paaride kogumit. Näiteks naturaalarvude ruudustamist kirjeldatakse hulgana {<0,0>, <1,1>, <2,4>, <3,9>, …}. Sellise funktsiooni määratluspiirkond on iga paari esimeste elementide kogum, see tähendab naturaalarvud. Funktsiooni määratlemiseks peame määrama selle domeeni ja valemi.
Kuid matemaatika funktsioonid ei ole samad, mis programmeerimiskeelte funktsioonid. Matemaatika on palju lihtsam. Kuna mul pole aega keeruliste näidete jaoks, kaalume lihtsat: C-funktsiooni või Java staatilise meetodi, mis tagastab kahe täisarvu suurima ühise jagaja. Selle meetodi spetsifikatsioonis kirjutame: arvutab GCD(M,N) argumentide jaoks M и NKus GCD(M,N) - funktsioon, mille domeen on täisarvude paaride kogum ja tagastatav väärtus on suurim täisarv, mis jagatakse M и N. Kuidas on tegelikkus selle mudeliga võrreldes? Mudel töötab täisarvudega ja C või Java puhul on meil 32-bitine int. See mudel võimaldab meil otsustada, kas algoritm on õige GCD, kuid see ei hoia ära ülevooluvigu. Selleks oleks vaja keerulisemat mudelit, mille jaoks pole aega.
Räägime funktsiooni kui mudeli piirangutest. Mõned programmid (nt operatsioonisüsteemid) ei tagasta teatud argumentidele ainult konkreetset väärtust, vaid võivad töötada pidevalt. Lisaks sobib funktsioon mudelina halvasti teise sammu jaoks: probleemi lahendamise planeerimine. Kiirsortimine ja mulli sortimine arvutavad sama funktsiooni, kuid need on täiesti erinevad algoritmid. Seetõttu kasutan programmi eesmärgi saavutamise viisi kirjeldamiseks teist mudelit, nimetagem seda standardseks käitumismudeliks. Programm on selles esitatud kõigi kehtivate käitumiste kogumina, millest igaüks on omakorda olekute jada ja olek on muutujatele väärtuste määramine.
Vaatame, milline näeks välja Eukleidilise algoritmi teine samm. Peame arvutama GCD(M, N). Initsialiseerime M kui xJa N kui y, seejärel lahutage neist muutujatest korduvalt väiksemast suuremast, kuni need on võrdsed. Näiteks kui M = 12Ja N = 18, saame kirjeldada järgmist käitumist:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Ja kui M = 0 и N = 0? Null jagub kõigi arvudega, seega suurimat jagajat sel juhul pole. Sellises olukorras peame minema tagasi esimese sammu juurde ja küsima: kas me tõesti peame arvutama GCD mittepositiivsete arvude jaoks? Kui see pole vajalik, peate lihtsalt spetsifikatsiooni muutma.
Siinkohal on õige lühike kõrvalepõik tootlikkusest. Seda mõõdetakse sageli päevas kirjutatud koodiridade arvus. Kuid teie töö on palju kasulikum, kui vabanete teatud arvust ridadest, sest teil on vähem ruumi vigadele. Ja kõige lihtsam viis koodist vabanemiseks on esimene samm. Võimalik, et te lihtsalt ei vaja kõiki kellasid ja vilesid, mida proovite rakendada. Kiireim viis programmi lihtsustamiseks ja aja säästmiseks on mitte teha asju, mida ei tohiks teha. Teisel etapil on ajasäästu potentsiaali poolest teine. Kui mõõta tootlikkust kirjutatud ridade järgi, siis mõtlemine, kuidas ülesannet täita, paneb sind vähem produktiivne, sest saate sama probleemi lahendada vähema koodiga. Täpset statistikat ma siin anda ei saa, sest mul pole võimalust kokku lugeda ridade arvu, mida ma spetsifikatsioonile, st esimesele ja teisele sammule kulutatud aja tõttu ei kirjutanud. Ja siin ei saa ka katset teha, sest eksperimendis ei ole meil õigust esimest sammu teha, ülesanne on ette määratud.
Mitteametlike spetsifikatsioonide paljudest raskustest on lihtne mööda vaadata. Funktsioonide rangete spetsifikatsioonide kirjutamises pole midagi rasket; ma ei hakka seda arutama. Selle asemel räägime standardkäitumise tugevate spetsifikatsioonide kirjutamisest. On olemas teoreem, mis väidab, et turvaomaduste abil saab kirjeldada mis tahes käitumist (ohutus) ja ellujäämisomadused (elavus). Ohutus tähendab, et midagi hullu ei juhtu, programm ei anna valet vastust. Ellujäämine tähendab, et varem või hiljem juhtub midagi head, st programm annab varem või hiljem õige vastuse. Turvalisus on reeglina olulisem näitaja, siin tekivadki vead kõige sagedamini. Seetõttu ei hakka ma aja säästmiseks rääkima ellujäämisest, kuigi see on muidugi ka oluline.
Me saavutame ohutuse, määrates esmalt võimalike algseisundite komplekti. Ja teiseks suhted iga osariigi kõigi võimalike järgmiste olekutega. Käitugem nagu teadlased ja defineerigem olekuid matemaatiliselt. Algolekute komplekti kirjeldatakse valemiga, näiteks Eukleidilise algoritmi puhul: (x = M) ∧ (y = N). Teatud väärtuste jaoks M и N on ainult üks algseisund. Seost järgmise olekuga kirjeldatakse valemiga, milles järgmise oleku muutujad kirjutatakse algarvuga ja praeguse oleku muutujad ilma algarvuta. Eukleidilise algoritmi puhul käsitleme kahe valemi disjunktsiooni, millest ühes x on suurim väärtus ja teises - y:
Esimesel juhul on y uus väärtus võrdne y eelmise väärtusega ja uue x väärtuse saame lahutades väiksema muutuja suuremast. Teisel juhul teeme vastupidi.
Tuleme tagasi Eukleidilise algoritmi juurde. Oletame jälle, et M = 12, N = 18. See määratleb ühe algoleku, (x = 12) ∧ (y = 18). Seejärel ühendame need väärtused ülaltoodud valemiga ja saame:
Siin on ainus võimalik lahendus: x' = 18 - 12 ∧ y' = 12ja saame käitumise: [x = 12, y = 18]. Samamoodi saame kirjeldada kõiki oma käitumise olekuid: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Viimases olekus [x = 6, y = 6] avaldise mõlemad osad on väärad, seetõttu pole sellel järgmist olekut. Niisiis, meil on teise sammu täielik kirjeldus - nagu näeme, on see üsna tavaline matemaatika, nagu inseneride ja teadlaste oma, ja mitte kummaline, nagu arvutiteaduses.
Need kaks valemit saab ühendada üheks ajaloogika valemiks. See on elegantne ja lihtsalt seletatav, aga praegu pole selleks aega. Ajalikku loogikat võime vajada ainult elavuse jaoks, turvalisuse huvides pole seda vaja. Ajaline loogika kui selline mulle ei meeldi, see pole päris tavaline matemaatika, aga elavuse puhul on see vajalik pahe.
Eukleidilises algoritmis iga väärtuse jaoks x и y on ainulaadsed väärtused x' и y', mis muudavad seose järgmise olekuga tõeseks. Teisisõnu, Eukleidiline algoritm on deterministlik. Mittedeterministliku algoritmi modelleerimiseks peab praegusel olekul olema mitu võimalikku tulevast olekut ja igal praimimata muutuja väärtusel peab olema praimitud muutuja mitu väärtust, nii et seos järgmise olekuga oleks tõene. Seda pole raske teha, kuid ma ei hakka nüüd näiteid tooma.
Tööriista valmistamiseks on vaja formaalset matemaatikat. Kuidas muuta spetsifikatsioon ametlikuks? Selleks vajame ametlikku keelt, nt. . Eukleidilise algoritmi spetsifikatsioon selles keeles näeb välja järgmine:
Võrdsusmärgi sümbol kolmnurgaga tähendab, et märgist vasakul olev väärtus määratakse võrdseks märgist paremal oleva väärtusega. Sisuliselt on spetsifikatsioon definitsioon, meie puhul kaks määratlust. TLA+ spetsifikatsioonile peate lisama deklaratsioonid ja süntaksi, nagu ülaltoodud slaidil. ASCII-s näeks see välja selline:
Nagu näete, pole midagi keerulist. TLA+ spetsifikatsiooni saab kontrollida, st väikeses mudelis on võimalik mööda minna kõigist võimalikest käitumisviisidest. Meie puhul on see mudel teatud väärtused M и N. See on väga tõhus ja lihtne kontrollimismeetod, mis on täiesti automaatne. Lisaks on võimalik kirjutada formaalseid tõetõestusi ja neid mehaaniliselt kontrollida, kuid see võtab palju aega, nii et peaaegu keegi ei tee seda.
TLA+ peamiseks puuduseks on see, et tegemist on matemaatikaga ning programmeerijad ja arvutiteadlased kardavad matemaatikat. Esmapilgul kõlab see naljana, kuid kahjuks ütlen ma seda täie tõsidusega. Mu kolleeg rääkis mulle just, kuidas ta üritas TLA+ mitmele arendajale selgitada. Niipea kui valemid ekraanile ilmusid, muutusid nende silmad kohe klaasjaks. Nii et kui TLA+ on hirmutav, võite seda kasutada , on omamoodi mänguasjade programmeerimiskeel. PlusCali avaldis võib olla mis tahes TLA+ avaldis, st põhimõtteliselt mis tahes matemaatiline avaldis. Lisaks on PlusCal mittedeterministlike algoritmide süntaks. Kuna PlusCal suudab kirjutada mis tahes TLA+ avaldise, on see oluliselt väljendusrikkam kui mis tahes päris programmeerimiskeel. Järgmisena koostatakse PlusCal kergesti loetavaks TLA+ spetsifikatsiooniks. See ei tähenda muidugi, et keeruline PlusCal spetsifikatsioon muutuks TLA+-s lihtsaks – lihtsalt nendevaheline vastavus on ilmne, täiendavat keerukust ei teki. Lõpuks saab seda spetsifikatsiooni kontrollida TLA+ tööriistade abil. Üldiselt võib PlusCal aidata üle saada matemaatikafoobiast; seda on lihtne mõista isegi programmeerijatele ja arvutiteadlastele. Varem avaldasin selle kohta algoritme mõnda aega (umbes 10 aastat).
Võib-olla vaidleb keegi vastu, et TLA+ ja PlusCal on matemaatika ning matemaatika töötab ainult väljamõeldud näidetega. Praktikas on vaja päris keelt, kus on tüübid, protseduurid, objektid jne. See on vale. Amazonis töötanud Chris Newcomb kirjutab järgmiselt: "Oleme kasutanud TLA+ kümnes suures projektis ja igal juhul muutis selle kasutamine arengut oluliselt, sest suutsime tabada ohtlikud vead enne nende tootmisse jõudmist ja kuna see andis meile agressiivseks muutmiseks vajaliku ülevaate ja enesekindluse. jõudluse optimeerimine, ilma et see mõjutaks programmi tõesust". Tihti võib kuulda, et formaalsete meetodite kasutamisel saame ebaefektiivse koodi – praktikas on kõik täpselt vastupidine. Lisaks on levinud arusaam, et juhte ei saa veenda formaalsete meetodite vajalikkuses, isegi kui programmeerijad on nende kasulikkuses veendunud. Ja Newcomb kirjutab: "Juhid pingutavad nüüd igal võimalikul viisil TLA+ spetsifikatsioonide kirjutamise nimel ja eraldavad selleks spetsiaalselt aega.". Nii et kui juhid näevad, et TLA+ töötab, võtavad nad selle omaks. Chris Newcomb kirjutas selle umbes kuus kuud tagasi (oktoober 2014), kuid nüüd on minu teada TLA+ kasutusel 14 projektis, mitte 10. Teine näide on seotud XBox 360 disainiga. Praktikant tuli Charles Thackeri juurde ja kirjutas mälusüsteemi spetsifikatsiooni. Tänu sellele spetsifikatsioonile leiti viga, mida muidu poleks tuvastatud ja mis põhjustaks iga XBox 360 krahhi pärast neljatunnist kasutamist. IBM-i insenerid kinnitasid, et nende testid poleks seda viga tuvastanud.
Lisateavet TLA+ kohta saate lugeda Internetist, kuid nüüd räägime mitteametlikest spetsifikatsioonidest. Harva peame kirjutama programme, mis arvutavad välja vähima ühise jagaja jms. Palju sagedamini kirjutame selliseid programme nagu ilus-printeritööriist, mille kirjutasin TLA+ jaoks. Pärast kõige lihtsamat töötlemist näeb TLA+ kood välja selline:
Kuid ülaltoodud näites soovis kasutaja suure tõenäosusega, et side ja võrdusmärgid oleksid joondatud. Seega näeks õige vorming välja selline:
Mõelge veel ühele näitele:
Vastupidi, siin oli võrdusmärkide joondamine, liitmine ja korrutamine allikas juhuslik, seega piisab kõige lihtsamast töötlemisest. Üldiselt pole õige vormingu täpset matemaatilist määratlust, sest "õige" tähendab antud juhul "mida kasutaja soovib" ja seda ei saa matemaatiliselt määrata.
Näib, et kui meil pole tõe definitsiooni, siis on täpsustus kasutu. Aga see pole tõsi. See, et me ei tea, mida programm tegema peaks, ei tähenda, et me ei peaks mõtlema, kuidas see peaks töötama – vastupidi, peaksime sellele veelgi rohkem pingutama. Spetsifikatsioon on siin eriti oluline. Struktureeritud printimiseks on võimatu määrata optimaalset programmi, kuid see ei tähenda, et me ei peaks seda üldse ette võtma ja koodi kirjutamine teadvuse vooluna pole nii. Kirjutasin lõpuks kuue reegli spetsifikatsiooni koos määratlustega kommentaaride näol Java failis. Siin on näide ühest reeglist: a left-comment token is LeftComment aligned with its covering token. See reegel on kirjutatud näiteks matemaatilises inglise keeles: LeftComment aligned, left-comment и covering token — mõisted koos määratlustega. Matemaatikud kirjeldavad matemaatikat nii: nad kirjutavad terminite määratlusi ja loovad nende põhjal reegleid. Selle spetsifikatsiooni eeliseks on see, et kuut reeglit on palju lihtsam mõista ja siluda kui 850 koodirida. Pean ütlema, et nende reeglite kirjutamine ei olnud lihtne, nende silumine võttis üsna palju aega. Kirjutasin spetsiaalselt selleks otstarbeks koodi, mis ütles mulle, millist reeglit kasutatakse. Kuna testisin neid kuut reeglit mõne näitega, ei pidanud ma siluma 850 koodirida ja vigu oli üsna lihtne leida. Java-l on selleks suurepärased tööriistad. Kui ma oleksin just koodi kirjutanud, oleks mul kulunud palju rohkem aega ja vorming oleks olnud kehvema kvaliteediga.
Miks ei saanud kasutada ametlikku spetsifikatsiooni? Ühest küljest pole korrektne täitmine siin liiga oluline. Struktureeritud väljatrükk on kindlasti mõne jaoks ebarahuldav, nii et ma ei pidanud seda kõigis ebatavalistes olukordades õigesti töötama. Veelgi olulisem on asjaolu, et mul polnud piisavaid tööriistu. TLA+ mudelikontroll on siin kasutu, seega peaksin näited käsitsi kirjutama.
Antud spetsifikatsioonil on kõikidele spetsifikatsioonidele ühised omadused. See on kõrgemal tasemel kui kood. Seda saab rakendada mis tahes keeles. Selle kirjutamiseks pole tööriistu ega meetodeid. Ükski programmeerimiskursus ei aita teil seda spetsifikatsiooni kirjutada. Ja pole tööriistu, mis võiksid selle spetsifikatsiooni tarbetuks muuta, välja arvatud juhul, kui kirjutate spetsiaalselt keelt TLA+ struktureeritud väljatrükiprogrammide kirjutamiseks. Lõpuks ei ütle see spetsifikatsioon midagi selle kohta, kuidas täpselt koodi kirjutame, vaid lihtsalt kirjas, mida kood teeb. Kirjutame spetsifikatsiooni, mis aitab meil probleemist läbi mõelda, enne kui hakkame koodile mõtlema.
Kuid sellel spetsifikatsioonil on ka funktsioone, mis eristavad seda teistest spetsifikatsioonidest. 95% muudest spetsifikatsioonidest on palju lühemad ja lihtsamad:
Lisaks on see spetsifikatsioon reeglite kogum. Tavaliselt on see märk halvast spetsifikatsioonist. Reeglite kogumi tagajärgede mõistmine on üsna keeruline, mistõttu pidin kulutama palju aega nende silumisele. Kuid antud juhul ei leidnud ma paremat viisi.
Pidevalt töötavate programmide kohta tasub öelda paar sõna. Tavaliselt töötavad need paralleelselt, näiteks operatsioonisüsteemid või hajutatud süsteemid. Väga vähesed suudavad neist oma mõtetes või paberil aru saada ja mina nende hulka ei kuulu, kuigi kunagi sain hakkama. Seetõttu vajame tööriistu, mis meie tööd kontrollivad – näiteks TLA+ või PlusCal.
Miks ma pidin spetsifikatsiooni kirjutama, kui ma juba teadsin, mida kood peaks tegema? Tegelikult ma ainult arvasin, et tean seda. Lisaks, kui spetsifikatsioon on paigas, ei pea kõrvalseisja enam koodi uurima, et mõista, mida see täpselt teeb. Mul on reegel: üldisi reegleid ei tohiks olla. Sellest reeglist on muidugi erand, see on ainus üldreegel, mida järgin: koodi spetsifikatsioon peaks ütlema inimestele kõike, mida nad selle koodi kasutamisel teadma peavad.
Mida siis täpselt peavad programmeerijad mõtlemise kohta teadma? Alustuseks sama, mis kõigiga: kui sa ei kirjuta, siis tundub sulle ainult, et sa mõtled. Samuti peate enne kodeerimist mõtlema, mis tähendab, et peate enne koodi kirjutamist kirjutama. Spetsifikatsioon on see, mille me kirjutame enne kodeerimise alustamist. Spetsifikatsiooni on vaja iga koodi jaoks, mida igaüks saab kasutada või muuta. Ja see “keegi” võib osutuda koodi autoriks kuu aega pärast selle kirjutamist. Spetsifikatsiooni on vaja suurte programmide ja süsteemide, klasside, meetodite ja mõnikord isegi ühe meetodi keerukate osade jaoks. Mida täpselt peaksite koodi kohta kirjutama? Peate kirjeldama, mida see teeb, st midagi, mis võib olla kasulik kõigile, kes seda koodi kasutavad. Mõnikord võib osutuda vajalikuks ka täpsustada, kuidas täpselt kood oma eesmärgi saavutab. Kui me läbisime selle meetodi algoritmide kursusel, siis nimetame seda algoritmiks. Kui see on midagi spetsialiseeritumat ja uut, siis nimetame seda kõrgetasemeliseks disainiks. Siin pole formaalset erinevust: mõlemad on programmi abstraktsed mudelid.
Kuidas täpselt peaksite koodi spetsifikatsiooni kirjutama? Peaasi: see peaks olema ühe taseme võrra kõrgem kui kood ise. See peab kirjeldama seisundeid ja käitumist. See peaks olema nii range, kui ülesanne nõuab. Kui kirjutate ülesande rakendamise spetsifikatsiooni, saab selle kirjutada pseudokoodis või PlusCali abil. Peate õppima kirjutama spetsifikatsioone ametlike spetsifikatsioonide abil. See annab teile vajalikud oskused, mis on abiks ka mitteametlike oskuste puhul. Kuidas õppida ametlikke spetsifikatsioone kirjutama? Kui õppisime programmeerima, kirjutasime programme ja seejärel silusime neid. Sama asi siin: peate kirjutama spetsifikatsiooni, kontrollima seda mudelikontrolliga ja parandama vead. TLA+ ei pruugi olla ametliku spetsifikatsiooni jaoks parim keel ja tõenäoliselt sobiks mõni muu keel paremini teie konkreetsetele vajadustele. TLA+ suurepärane asi on see, et see õpetab matemaatilist mõtlemist suurepäraselt.
Kuidas siduda spetsifikatsiooni ja koodi? Kommentaaride kasutamine, mis seovad matemaatilisi mõisteid ja nende rakendamist. Kui töötate graafikutega, on teil programmi tasemel sõlmede massiive ja linkide massiive. Seega peate kirjutama, kuidas täpselt graafikut need programmeerimisstruktuurid rakendavad.
Tuleb märkida, et ükski ülaltoodust ei kehti koodi kirjutamise protsessi enda kohta. Koodi kirjutades ehk kolmandat sammu sooritades tuleb ka programm läbi mõelda ja läbi mõelda. Kui alamülesanne osutub keeruliseks või pole ilmne, peate kirjutama selle spetsifikatsiooni. Aga ma ei räägi siin koodist endast. Võite kasutada mis tahes programmeerimiskeelt, mis tahes metoodikat, see ei puuduta neid. Samuti ei välista ükski ülaltoodust koodi testimise ja silumise vajadust. Isegi kui abstraktne mudel on õigesti kirjutatud, võib selle rakendamisel esineda vigu.
Spetsifikatsioonide kirjutamine on kodeerimisprotsessi täiendav samm. Tänu sellele saab palju vigu tabada väiksema vaevaga – teame seda Amazoni programmeerijate kogemusest. Spetsifikatsioonidega muutub programmide kvaliteet kõrgemaks. Miks me siis nii sageli ilma nendeta läheme? Sest kirjutamine on raske. Aga kirjutamine on raske, sest selleks on vaja mõelda ja ka mõtlemine on raske. Alati on lihtsam teeselda, et mõtled. Siin võib tuua analoogia jooksmisega – mida vähem jooksed, seda aeglasemalt jooksed. Peate treenima oma lihaseid ja harjutama kirjutamist. See nõuab harjutamist.
Spetsifikatsioon võib olla vale. Võib-olla tegite kuskil vea või nõuded on muutunud või vajate täiustamist. Iga kood, mida keegi kasutab, tuleb muuta, nii et varem või hiljem ei vasta spetsifikatsioon enam programmile. Ideaalis peate sel juhul kirjutama uue spetsifikatsiooni ja kirjutama koodi täielikult ümber. Teame väga hästi, et keegi seda ei tee. Praktikas parandame koodi ja võib-olla värskendame spetsifikatsiooni. Kui see juhtub varem või hiljem, siis milleks üldse spetsifikatsioone kirjutada? Esiteks on selle isiku jaoks, kes teie koodi redigeerib, iga lisasõna spetsifikatsioonis kulda väärt ja see inimene võib olla teie. Ma löön ennast sageli selle pärast, et ma pole koodi muutmisel piisavalt konkreetne. Ja ma kirjutan rohkem spetsifikatsioone kui koodi. Seetõttu tuleb koodi muutmisel spetsifikatsiooni alati värskendada. Teiseks muutub kood iga redigeerimisega aina hullemaks, seda on raskem lugeda ja hooldada. See on entroopia suurenemine. Kuid kui te ei alusta spetsifikatsiooniga, on iga kirjutatud rida muudatus ja kood on mahukas ja algusest peale raskesti loetav.
Nagu öeldud , ühtki lahingut ei võidetud plaani järgi ja ühtegi lahingut ei võidetud ilma plaanita. Ja ta teadis midagi lahingutest. Arvatakse, et spetsifikatsioonide kirjutamine on ajaraisk. Mõnikord on see tõsi ja ülesanne on nii lihtne, et pole mõtet seda lõpuni mõelda. Kuid peaksite alati meeles pidama, et kui teil soovitatakse spetsifikatsioone mitte kirjutada, tähendab see, et teil ei soovitata mõelda. Ja sa peaksid sellele iga kord mõtlema. Ülesande läbimõtlemine ei garanteeri, et sa vigu ei tee. Nagu me teame, ei leiutanud keegi võlukeppi ja programmeerimine on keeruline ülesanne. Aga kui te ülesannet läbi ei mõtle, on teil kindlasti vigu.
TLA+ ja PlusCali kohta saad täpsemalt lugeda spetsiaalselt kodulehelt, sinna saad minna minu kodulehelt . See on minu jaoks kõik, tänan tähelepanu eest.
Pidage meeles, et see on tõlge. Kommentaare kirjutades pidage meeles, et autor neid ei loe. Kui soovite tõesti autoriga vestelda, on ta kohal Hydra 2019 konverentsil, mis toimub 11.-12 Peterburis. Pileteid saab osta .
Allikas: www.habr.com