See artikkel on tõlge . Kuid enne seda väike sissejuhatus. Kuidas tekivad zombid? Igal inimesel on olnud olukordi, kus tahaks tõsta sõpra või kolleegi oma tasemele, aga see ei õnnestu. Ja tegelikult ei õnnestu see mitte ainult sinul, vaid ka temal: ühel tasandil on normaalne palk, ülesanded ja nii edasi, teisel tasandil aga vajadus mõelda. Mõtlema sundimine on ebameeldiv ja valus. Ta loobub kiiresti ja jätkab kodeerimist, täiesti mõistust mitte kasutades. Sa suudad ette kujutada, kui palju energiat tuleb kulutada õpetatud abituse barjääri ületamiseks, ja lihtsalt ei tee seda. Nii tekivad zombid, keda võiks nagu ravida, aga tunduvalt ei tegeleta sellega.
Kui ma nägin, et (jah, jah, see sama mees õpikutes) ja teeb mitte ettekande, vaid küsimuste-vastuste sessiooni, siis ma veidi ärevaks jäin. Igaks juhuks, Leslie on maailmakuulus teadlane, kes on põhiteoste autor jaotatud arvutustes, ja te võite teda ehk tunda La-tähtede poolest LaTeX-is — „Lamport TeX“. Teiseks murettekitavaks faktoriks on tema nõudmine: igaühel, kes tuleb, tuleb (täiesti tasuta) eelnevalt kuulata paar tema ettekannet, välja mõelda vähemalt üks küsimus ja siis juba tulla. Otsustasin vaadata, mida Lamport räägib — ja see on suurepärane! See on täpselt see asi, maagiline link-tablett zombituse raviks. Hoian ette: tekst võib „põleda“ neile, kes armastavad ülipainduvaid meetodeid ja ei armasta testida kirjutatut.
Pärast hublukat algabki seminar tõlge. Head lugemist!
Ükskõik, millise ülesande te endale võtate, peate alati läbima kolm sammu:
- otsustamine, millist eesmärki soovite saavutada;
- otsustamine, kuidas te täpselt oma eesmärk ära täidate;
- oma eesmärgi saavutamine.
See kehtib ka programmeerimise kohta. Kui me kirjutame koodi, peame meie:
- otsustama, mida programm tegema peab;
- mõtlema, kuidas ta oma ülesannet täitma peab;
- sobiva koodi kirjutama.
Viimane samm on loomulikult väga oluline, kuid sellest ma täna rääkima ei hakka. Selle asemel arutame esimesi kahte. Iga arendaja teeb need enne alustamist. Te ei istu kirjutama, kui te ei ole otsustanud, mida täpselt kirjutate: brauser või andmebaas. Teie eesmärgi mõte peab kindlasti olema olemas. Ja te peate kindlasti läbi mõtlema, mida programm täpselt tegema hakkab, mitte kirjutama lihtsalt lohistically lootuses, et kood kuidagi muutub brauseriks.
Kuidas tegelikult toimub see esmase koodi planeerimine? Kui palju pingutust peaksime sellele kulutama? Kõik sõltub sellest, kui keerulist probleemi me lahendame. Eeldame, et soovime kirjutada tõrkeresistentset jaotatud süsteemi. Sellisel juhul peaksime kõike hoolikalt läbi mõtlema enne, kui hakkame koodiga tegelema. Aga kui peame lihtsalt suurendama tervet muutuja väärtust 1 võrra? Esmapilgul tundub see triviaalne ja mõtlemist ei vajata, kuid siis me meenutame, et võib juhtuda ülevu. Seetõttu, et mõista, kas probleem on lihtne või keeruline — tuleb alguses mõelda.
Kui eelnevalt läbi mõelda võimalikke lahendusi probleemile, saab vältida vigu. Kuid selleks peab teie mõtlemine olema selge. Selle saavutamiseks tuleb oma mõtted kirja panna. Mulle meeldib väga Dick Gindoni ütlus: "Kui sa kirjutad, näitab loodus sulle, kui lohakalt sa mõtled." Kui te ei kirjuta, siis tundub teile lihtsalt, et te mõtletemis. Ja oma mõtteid tuleb kirja panna spetsifikatsioonide kujul.
Spetsifikatsioonid täidavad mitmeid funktsioone, eriti suurtes projektides. Kuid ma räägin ainult ühest neist: nad aitavad meil selgelt mõelda. Selgelt mõelda on väga oluline ja üsna keeruline, seega vajame siin igasugust abi. Millisel keeles peaksime spetsifikatsioone kirjutama? See on alati esimene küsimus arendajatele: millises keeles kirjutame. Ühte õigesti vastust sellele ei ole: probleemid, mida me lahendame, on liiga mitmekesised. Mõnedele on kasulik TLA+ — see on spetsifikatsioonide keel, mille ma välja töötasin. Teistele on mugavam kasutada hiina keelt. Kõik sõltub olukorrast.
Küsimus on selles: kuidas saavutada selgemat mõtlemist? Vastus: me peame mõtlema nagu teadlased. See mõtlemisviis on viimase 500 aasta jooksul hästi toiminud. Teaduses loome me matemaatilisi mudeleid reaalsusest. Astronoomia oli ilmselt esimene teadus rangemas mõttes. Astronoomias kasutatavates matemaatilistes mudelites kujutatakse taevakehi punktidena, millel on mass, asukoht ja impulss, kuigi tegelikkuses on nad äärmiselt keerulised objektid koos mägede ja ookeanidega, tõusude ja mõõnadega. See mudel, nagu iga teine, on loodud konkreetsete probleemide lahendamiseks. See sobib suurepäraselt määramaks, kuhu suunata teleskoop, kui tuleb leida planeet. Kuid kui soovite prognoosida selle planeedi ilma, siis see mudel ei sobi.
Matemaatika võimaldab meil määrata mudeli omadusi. Ja teadus näitab, kuidas need omadused seostuvad reaalsusega. Räägime meie teadusest, arvutiteadusest. Reaalsus, millega me töötame, on väga erinevad arvutisüsteemid: protsessorid, mängukonsoolid, arvutid, mis käitavad programme jne. Räägin programmi käivitamisest arvutis, kuid, üldiselt, kehtivad kõik need järeldused igasuguste arvutisüsteemide kohta. Meie teaduses kasutame palju erinevaid mudeleid: Turingi masin, osaliselt järjestatud sündmustega kogud ja paljud teised.
Mis on programm? See on iga kood, mida saab käsitleda iseseisvalt. Oletame, et peame kirjutama brauseri. Me täidame kolm ülesannet: projekteerime programmi esitluse kasutajale, seejärel kirjutame programmi kõrge taseme skeemi ja lõpuks 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 alauuend: liite õigesti sõnadesse. Selle alateema lahendame samuti kolmes etapis — nagu näeme, need korduvad mitmel tasandil.
Vaatame lähemalt esimese sammu: millist probleemi programm lahendab. Siin modellime programmi tihti kui funktsiooni, mis võtab sisse teatud sisendandmed ja annab välja teatud väljundandmed. Matemaatikas kirjeldatakse funktsiooni tavaliselt kui järjestatud paaride hulka. Näiteks, ruutfunktsioon naturaalarvude jaoks on kirjeldatud kui hulk {, , , , ...}. Selle funktsiooni määramispiirkond on paaride esimeste elementide hulk, see tähendab naturaalarve. Funktsiooni määratlemiseks peame näitama selle määramispiirkonna ja valemi.
Aga matemaatikas olevad funktsioonid ei ole samad, mis programmeerimiskeeltes. Matemaatika on oluliselt lihtsam. Kuna mul pole aega keerukate näidete jaoks, vaatame lihtsat: funktsioon C keeles või staatiline meetod Java keeles, mis tagastab kahe täisarvu suurima ühise jagaja. Selle meetodi spetsifikatsioonis kirjutame: arvutab GCD(M,N) argumentide jaoks M ja N, kus GCD(M,N) — funktsioon, mille määramispiirkond on täisarvude paaride hulk, ja tagastatav väärtus on suurim täisarv, millesse jagub M ja N. Kuidas see mudel reaalsusega seondub? Mudel opereerib täisarvudega, kuid C-s või Java-s on meil 32-bitised int. See mudel võimaldab meil otsustada, kas algoritm GCD, on õige, kuid see ei takista ülevoolu vigu. Selleks oleks vajalik keerulisem mudel, mille jaoks pole aega.
Räägime funktsiooni piirangutest mudelina. Mõnede programmide (nt operatsioonisüsteemide) töö ei ole lihtsalt kindlatele argumentidele kindla väärtuse tagastamine, need võivad töötada pidevalt. Lisaks on funktsioon mudelina kehva sobivuse tõttu teise sammu jaoks: probleemi lahendamise plaani koostamine. Kiirusortimine ja mullisortimine arvutavad sama funktsiooni, kuid need on täiesti erinevad algoritmid. Seetõttu kasutan programmi eesmärgi saavutamise viisi kirjeldamiseks teist mudelit, nimetame seda standardselt käitumismudeliks. Programm on selles esitatud kõikide lubatud käitumiste koguna, millest igaüht saab omakorda vaadelda seisundite järjestikuse kogumina, kus seisund on muutuja väärtuste määramine.
Vaadakem, kuidas näeb välja teise sammu protsess Euclide algoritmis. Peame arvutama GCD(M, N). Algatame M kuidas x, vaid N kuidas y, seejärel lahutame suuremast muutujast väiksema, kuni need on võrdsed. Näiteks, kui M = 12, vaid 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õrvaleviide tootlikkusele. Seda mõõdetakse sageli päevade jooksul kirjutatud koodiread. Kuid teie töö on palju kasulik, kui olete kõrvaldada teatud arvu ridu, kuna teil on vähem avastatav viga. Ja koodist vabanemine on kõige lihtsam just esimesel sammul. On täiesti võimalik, et kõik need nipsud, mida proovite rakendada, pole tegelikult vajalikud. Kiireim viis programmi lihtsustamiseks ja aja säästmiseks on mitte teha asju, mida ei maksa teha. Teine samm on teisel kohal ajasäästu potentsiaaliga. Kui mõõdate tootlikkust kirjutatud ridade arvu järgi, siis ülesande täitmise viisi mõtlemine muudab teid vähem tootlikuks, kuna saate sama ülesande lahendada väiksema koodihulgaga. Täpset statistikat ma siin anda ei saa, kuna mul pole võimalik loendada ridade arvu, mille ma ei kirjutanud just seetõttu, et kulutasin aega spetsifikatsioonile, st esimest ja teist sammu. Ja eksperimenti ei saa ka läbi viia, sest eksperimentides ei tohi me esimest sammu läbi viia, ülesanne on eelnevalt määratud.
Mitteformaalsete spetsifikatsioonide koostamisel on lihtne jätta arvesse paljusid raskusi. Pole midagi keerulist rangete spetsifikatsioonide kirjutamisel funktsioonide jaoks, sellest ma ei räägi. Selle asemel arutame rangete spetsifikatsioonide kirjutamist standardsete käitumismudelite jaoks. On teoreem, mis ütleb, et iga käitumiste kogumit saab kirjeldada koos ohutuse omadusega (safety) ja elujõudluse omadusega (liveness). Turvalisus tähendab, et midagi halba ei juhtu, programm ei anna vale vastust. Jätkusuutlikkus tähendab, et varem või hiljem juhtub midagi head, st programm annab varem või hiljem õige vastuse. Üldiselt on turvalisus olulisem näitaja, vead tekivad kõige sagedamini just siin. Seega, ajakulu säästmiseks ei hakka ma jätkusuutlikkusele keskenduma, kuigi see on samuti oluline.
Me saavutame turvalisuse, koostades kõigepealt palju võimalikke algtingimusi. Teiseks, seosed kõigi võimalike järgneva seisundiga iga olukorra jaoks. Käitume nagu teadlased ja määratleme seisundeid matemaatiliselt. Algtingimuste kogumit kirjeldatakse valemiga, näiteks Euclidi algoritmi puhul: (x = M) ∧ (y = N). Teatud väärtuste korral M ja N on ainult üks algne seisund. Seos järgmise seisundiga kirjeldatakse valemiga, kus järgmise seisundi muutujad kantakse üle kriipsudena, samas kui käesoleva seisundi muutujad jäävad ilma kriipsudeta. Euclidi algoritmi puhul käsitleme kahte valemit, millest ühes x on suurim väärtus, ja teises — y:
Esimesel juhul on uus väärtus y vana väärtuse y ega ole muutunud, samas kui uus väärtus x saadakse suurest muutujast väiksema lahutamisega. Teisel juhul teeme vastupidi.
Naaseme Euclidi algoritmi juurde. Oletame taas, et M = 12, N = 18. See määratleb 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 saame käitumise: [x = 12, y = 18]. Sama moodi saame kirjeldada kõiki olekuid meie käitumises: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Viimases seisundis [x = 6, y = 6] kui mõlemad lauseosad on vale, siis järgnevat seisundit ei ole. Nii et meil on täielik spetsifikatsioon teise sammu kohta — nagu näeme, on see täiesti tavaline matemaatika, nagu inseneride ja teadlaste seas, mitte midagi imelikku, nagu arvutiteaduses.
Need two formulae can be combined into a single temporal logic formula. It is elegant and easy to explain, but there is currently no time for that. Temporal logic may only be necessary for the liveness property; it is not needed for security. Temporal logic as such is not appreciated; it is not quite conventional 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, the Euclidean algorithm is deterministic. To model a nondeterministic algorithm, the current state must have several possible future states, and each value of the variable without a stroke must have several values of the variable with a stroke for which the relation with the next state holds true. This is not difficult to do, but I will not provide examples now.
To create a working tool, formal mathematics is needed. How to make a formal specification? For this, we will need a formal language, for example, . The specification of Euclid's algorithm will look as follows in this language:
The equality sign with a triangle indicates that the value on the left side of the sign is defined as equal to the value on the right side of the sign. Essentially, a specification is a definition, in our case, two definitions. To the TLA+ specification, declarations and some syntax need to be added, as shown in the slide above. In ASCII it looks like this:
As we can see, nothing complicated. The specification in TLA+ can be verified, i.e. check all possible behaviors in a small model. In our case, this model will be defined values M ja N. This is a very efficient and straightforward verification method that is entirely automated. Moreover, formal proofs of validity can be written and checked mechanically, but this takes a lot of time, which is why almost no one does it.
TLA+ peamine puudus on see, et see on matemaatika, ja programmeerijad ning arvutiteadlastel on matemaatika ees hirm. Esmapilgul võib see kõlada naljakalt, kuid kahjuks räägin ma seda täiesti tõsiselt. Minu kolleeg rääkis just sellest, kuidas ta üritas selgitada TLA+d mitmele arendajale. Kui ekraanile ilmusid valemid, sai neil kohe klaasist pilk. Nii et kui TLA+ tundub hirmuäratav, siis on võimalik kasutada , mis on omamoodi mängurakendusprogrammeerimise keel. PlusCalis võib väljend olla mis tahes TLA+ väljend, see tähendab, et sisuliselt on see mis tahes matemaatiline väljend. Lisaks on PlusCalis süntaks mittedeterministlikele algoritmidele. Kuna PlusCalis saab kirjutada mis tahes TLA+ väljendi, on see oluliselt väljendusrikkam kui ükski reaalne programmeerimiskeel. Edasi, PlusCal kompileeritakse kergesti loetavaks TLA+ spetsifikatsiooniks. See ei tähenda muidugi, et keeruline PlusCal spetsifikatsioon muutub lihtsaks TLA+-iks — lihtsalt vastavus nende vahel on ilmselge, ei toimu lisakompleksuse teket. Lõpuks saab seda spetsifikatsiooni kontrollida TLA+ tööriistade abil. Üldiselt võib PlusCal aidata ületada matemaatika foobiat, seda on isegi programmeerijatel ja arvutiteadlastel lihtne mõista. Minevikus olin ma umbes 10 aastat aktiivne PlusCali algoritmide avaldamisel.
Võib-olla leidub keegi, kes väidab, et TLA+ ja PlusCal on matemaatika, ja matemaatika töötab ainult väljamõeldud näidetes. Praktikas on aga vajalik reaalne keel, mis sisaldab tüüpe, protseduure, objekte ja nii edasi. See ei ole nii. Siin on, mida kirjutab Chris Newcomb, kes töötas Amazonis: „Kasutame TLA+ kümnes suures projektis, ja igal juhul andis selle kasutamine olulise panuse arendusse, kuna suutsime ohtlikud vead kinni püüda enne, kui need jõudsid tootmisse, ja kuna see andis meile arusaama ja kindlust, mis oli vajalik agressiivsete jõudluse optimeerimiste jaoks, mis ei mõjutanud programmi tõelisust". Tihti võib kuulda, et formaalsete meetodite kasutamisel sünnib ebaefektiivne kood — praktikas on aga kõike just vastupidi. Lisaks on levinud arvamus, et juhte on võimatu veenda formaalsete meetodite vajalikkuses, isegi kui programmeerijad on veendunud nende kasulikkuses. Ja Newcomb kirjutab: „Juhtijad näevad nüüd kõiki võimalusi, et kirjutada TLA+ spetsiifikasid ning eraldavad selleks spetsiaalselt aega“. Nii et kui juhtijad näevad, et TLA+ töötab, võtavad nad selle rõõmuga vastu. Chris Newcomb kirjutas seda umbes kuus kuud tagasi (oktoobris 2014), kuid nüüd, kui ma tean, kasutatakse TLA+ 14 projektis, mitte 10. Teine näide puudutab XBox 360 kavandamist. Charles Tecker sai praktikandi, kes kirjutas mälusüsteemi spetsiifikatsiooni. Tänu sellele spetsiifikatsioonile avastati viga, mida muidu ei oleks märgatud, ja mille tõttu oleks iga XBox 360 nelja tunni pärast crashinud. IBM-i insenerid kinnitasid, et nende testid ei oleks seda viga avastanud.
TLA+ kohta saate internetis rohkem lugeda, aga nüüd räägime mitteformaalsetest spetsiifikatsioonidest. Me ei pea sageli kirjutama programme, mis arvutavad maassima jagaja ja sarnaseid asju. Oluliselt sagedamini kirjutame programme, nagu näiteks struktuuriprindimise tööriist (pretty-printer), mille ma kirjutasin TLA+-le. Pärast kõige lihtsamat töötlemist näeks TLA+ kood välja järgnev:
Aga antud näites tahtis kasutaja tõenäoliselt, et konjunktiivsete ja võrdsusmärkide joondus oleks ühtlane. Nii et õige vormindamine näeks pigem välja nii:
Vaatame teist näidet:
Siin oli vastupidi, võrdsus-, liitmis- ja korrutamismärkide joondus allikas juhuslik, seega oli kõige lihtsam töötlemine täiesti piisav. Üldiselt pole täpset matemaatilist määratlust õigele vormindusele, sest „õige“ tähenduses tähendab „nagu kasutaja soovib“, mida matemaatiliselt määratleda ei saa.
Tundub, et kui meil ei ole tõeväärtuse määratlust, siis on spetsiifikatsioon kasutu. Aga see ei ole nii. Kui me ei tea, mida programm täpselt tegema peab, ei tähenda see, et me ei peaks selle töö peale mõtlema – vastupidi, peaksime sellele rohkem aega kulutama. Spetsiifikatsioon on sel juhul eriti oluline. Optimaalse programmi määramine struktuuriprinterile on võimatu, aga see ei tähenda, et me ei peaks sellega tegelema, ja koodi kirjutamine vooluna ei ole õige lähenemine. Lõpuks kirjutasin kuue reegli ja määratlustega spetsiifikatsiooni kommentaaride kujul Java-failis. Siin on üks näide reeglitest: left-comment token on LeftComment, mis on joondatud selle katva tokeniga. See reegel on kirjutatud, ütleme, matemaatilises inglise keeles: LeftComment joondatud, left-comment ja kattev token — terminid koos määratlustega. See on see, kuidas matemaatikud matemaatikat kirjeldavad: nad kirjutavad terminite määratlusi ja nende põhjal reeglid. Sellise spetsifikatsiooni kasu on see, et kuue reegli mõistmine ja silumine on oluliselt lihtsam kui 850 koodi rida. Pean ütlema, et nende reeglite kirjutamine ei olnud kerge, nende silumiseks kulus üsna palju aega. Just selle eesmärgi nimel kirjutasin koodi, mis teatas, millist reeglit kasutatakse. Tänu sellele, et ma kontrollisin neid kuut reeglit mitmete näidete peal, ei pidanud ma siluma 850 koodi rida, ja vigade leidmine osutus üsna lihtsaks. Java jaoks on selleks suurepärased tööriistad. Kui ma lihtsalt koodi kirjutanud oleksin, oleks see mulle oluliselt kauem aega võtnud ja vormindamine oleks olnud halvem.
Miks ei saanud kasutusele võtta formaalset spetsifikatsiooni? Ühelt poolt ei ole õigsuse tagamine siin liiga oluline. Struktuurne printimine ei sobi kindlasti kellelegi, seega ei pidanud ma tagama, et see töötas kõigis ebatavalistes olukordades. Veel olulisem on see, et mul ei olnud adekvaate tööriistu. TLA+ mudelite kontrollimisvahend siin ei tööta, seega oleksin pidanud näidised käsitsi kirjutama.
Antud spetsifikatsioonil on omad jooned, mis on tavalised kõigi spetsifikatsioonide puhul. See on kõrgemal tasemel kui kood. Seda saab rakendada mistahes keeles. Selle kirjutamiseks ei ole kasu mistahes tööriikudest või meetoditest. Ükski programmeerimise kursus ei aita teil seda spetsifikatsiooni kirjutada. Ja ei ole olemas tööriistu, mis võiksid selle spetsifikatsiooni vajaduse kaotada, kui just ei kirjuta keelt, mis on mõeldud struktuurse printimise programmide kirjutamiseks TLA+ abil. Lõpuks, see spetsifikatsioon ei ütle midagi selle kohta, kuidas me koodi kirjutame, see näitab ainult, mida see kood teeb. Me kirjutame spetsifikatsiooni, et aidata meil probleemile mõelda, enne kui hakkame koodist mõtlema.
Kuid sellel spetsifikatsioonil on ka omadused, mis eristavad seda teistest spetsifikatsioonidest. 95% teistest spetsifikatsioonidest on oluliselt lühemad ja lihtsamad:
Edasi, see spetsifikatsioon on reeglite kogum. Üldiselt on see halbade spetsifikatsioonide tunnus. Reeglite kogumi tagajärgede mõistmine on üsna keeruline ja seepärast pidin ma nende tõrkeotsimiseks palju aega kulutama. Sellegipoolest ei leidnud ma sellisel juhul paremat lahendust.
Tasub öelda paar sõna programmidest, mis töötavad pidevalt. Üldiselt töötavad need paralleelselt, nagu näiteks operatsioonisüsteemid või jaotatud süsteemid. Väga vähesed saavad nendega vaimselt või paberil toime, ja ma ei kuulu nende hulka, ehkki kunagi suutsin. Seepärast on vajalikud tööriistad, mis kontrollivad meie tööd — näiteks TLA+ või PlusCal.
Miks pidin kirjutama spetsifikatsiooni, kui ma juba teadsin, mida kood peaks tegema? Tegelikult tundus mulle lihtsalt, et ma tean seda. Lisaks, kui olemas on spetsifikatsioon, ei pea võõras inimene enam koodi süüvima, et mõista, mida see täpselt teeb. Mul on reegel: üldiselt ei peaks olema mingeid üldisi reegleid. Sellel reeglil on muidugi erand, see on ainus üldine reegel, millele ma toetun: koodi spetsifikatsioon peab edastama inimestele kõik, mis neile on vajalik selle koodi kasutamiseks.
Nii et, mida peavad programmeerijad teadma mõtlemisest? Esiteks, sama, mis kõik: kui sa ei kirjuta, siis tundub sul ainult, et sa mõtled. Lisaks tuleb mõelda enne kodeerimist, mis tähendab, et tuleb kirjutada enne kodeerimist. Spetsifikatsioon on see, mida me kirjutame enne, kui hakkame kodeerima. Spetsifikatsioon on vajalik igasuguse koodi jaoks, mida keegi teine võib kasutada või muuta. Ja see 'keegi' võib olla ka koodi autor üks kuu pärast kirjutamist. Spetsifikatsioon on vajalik suurte programmide ja süsteemide, klasside, meetodite ja mõnikord isegi keeruliste osade jaoks üksiku meetodi sees. Mida täpselt tuleb koodi kohta kirjutada? Tuleb kirjeldada, mida see teeb, st mida võib-olla on kasulik teada igal inimesel, kes seda koodi kasutab. Mõnikord võib olla vajalik ka märkida, kuidas täpselt kood oma eesmärgini jõuab. Kui see meetod on läbi käidud algoritmide kursusel, siis nimetame seda algoritmiks. Kui see aga on midagi spetsiifilisemat ja uut, siis nimetame seda kõrgetasemeliseks projekteerimiseks. Formaalset vahet siin ei ole: mõlemad on abstraktsed programmimudelid.
Kuidas täpselt peaks kirjutama koodi spetsifikatsiooni? Peamine: see peab olema tasemelt kõrgem kui ise kood. See peab kirjeldama olekuid ja käitumisi. See peab olema nii rangelt, kui probleem nõuab. Kui kirjutate spetsifikatsiooni ülesande teostamise kohta, siis saab selle kirjutada pseudokoodina või PlusCal abil. Spetsifikatsioonide kirjutamist tuleb õppida formaalsetest spetsifikatsioonidest. See annab teile vajalikud oskused, mis aitavad ka mitteformaalsetes. Ja kuidas õppida kirjutama formaalseid spetsifikatsioone? Kui me õppisime programmeerimist, siis kirjutasime programme ja seejärel tõrkeotsisime neid. Sama kehtib siin: peate kirjutama spetsifikatsiooni, kontrollima seda mudeli kontrollimise vahendi abil ja parandama vea. TLA+ ei pruugi olla kõige parem keel formaalseks spetsifikatsiooniks, ja teie spetsiifiliste vajaduste jaoks sobib tõenäoliselt hoopis muu keel. TLA+ eeliseks on see, et see õpetab suurepäraselt matemaatilist mõtlemist.
Kuidas siduda spetsifikatsiooni ja koodi? Selleks on vajalikud kommentaarid, mis seovad matemaatilisi mõisteid ja nende rakendust. Kui töötate graafikute kallal, siis programmitasandil on teil sõlmede massiivid ja seoste massiivid. Seetõttu peate kirjutama, kuidas graaf neid programmise struktuure rakendab.
Oluline on märkida, et eelpool räägitu ei puuduta koodi kirjutamise protsessi. Kui kirjutate koodi, ehk täidate kolmandat sammu, peate samuti mõtlema ja kavandama programmi. Kui osaülesanne osutub keeruliseks või ebaselgeks, tuleb kirjutada selle jaoks spetsifikatsioon. Kuid koodi endast ma siin ei räägi. Te võite kasutada ükskõik millist programmeerimiskeelt või metoodikat, asi ei ole nendes. Lisaks ei vabasta eelnevast räägitu teid koodi testimise ja tõrkeotsingu vajadusest. Isegi kui abstraktne mudel on õigesti kirjutatud, võivad selle rakenduses esineda vead.
Spetsifikatsioonide kirjutamine on lisasamm koodi kirjutamise protsessis. Selle kaudu on võimalik paljusid vigu tuvastada vähemate pingutustega - me teame seda Amazonist pärit programmeerijate kogemuse põhjal. Spetsifikatsioonide abil tõuseb programmide kvaliteet. Miks me siis nii sageli ilma nendeta läbi saame? Sest kirjutamine on keeruline. Ja kirjutamine on keeruline, sest see nõuab mõtlemist, aga mõtlemine on samuti keeruline. Alati on lihtsam näida, et mõtleme. Siin saab tuua analoogia jooksmisega - mida rohkem te jooksete, seda kiiremini te jooksete. Peate oma lihaseid treenima ja kirjutamise harjutusi tegema. Praktika on vajalik.
Spetsifikatsioon võib olla vale. Te võisite kuskil eksida, võimalik, et nõuded on muutunud või on vajalikud täiustused. Iga kood, mida keegi kasutab, tuleb muuta, seega aeg-ajalt lakkab spetsifikatsioon vastamast programmale. Ideaalis peaks sellisel juhul kirjutama uue spetsifikatsiooni ja koodi täielikult ümber. Me teame hästi, et keegi seda ei tee. Praktiliselt me 'patch' koodi ja ehk värskendame spetsifikatsiooni. Kui see paratamatult varem või hiljem juhtub, siis miks üldse spetsifikatsioone kirjutada? Esiteks, inimese jaoks, kes teie koodi muudab, on iga liigne sõna spetsifikatsioonis kuldaväärt, ja see inimene võite olla ka teile endale. Ma kritiseerin end sageli seetõttu, et spetsifikatsioon on ebapiisav, kui muudan oma koodi. Ning kirjutad rohkem spetsifikatsioone kui koodi. Seega, kui te muudate koodi, tuleb spetsifikatsiooni alati värskendada. Teiseks, iga muutmisega muutub kood halvemaks, seda on järjest raskem lugeda ja hooldada. See on entropia suurenemine. Kuid kui te ei alusta spetsifikatsioonist, siis iga kirjutatud rida on muutmine ja kood on algusest peale kohmakas ja raskesti loetav.
Nagu ütles , ei ole ühtki lahingut võidetud plaani järgi ja ei ole ühtki lahingut võidetud ilma plaanita. Ja ta teadis lahingutest midagi. On arvamus, et spetsifikatsioonide kirjutamine on ajaraiskamine. Mõnikord on see tõsi ja ülesanne on nii lihtne, et pole mõtet sellele mõelda. Kuid alati tuleb meeles pidada, et kui teil soovitatakse spetsifikatsioone mitte kirjutada, tähendab see, et teile soovitatakse mitte mõelda. Ja sellest tuleb iga kord mõelda. Ülesande läbi mõtlemine ei garanteeri, et te eksite. Nagu me teame, ei ole keegi leiutanud imetootlat ja programmeerimine on keeruline tegevus. Kuid kui te ei mõtle ülesanne läbi, siis teete kindlalt vigu.
Rohkem TLA+ ja PlusCal kohta saab lugeda spetsiaalselt veebilehelt, kuhu pääseb minu isikliku lehe kaudu. . Sellega olen lõpetanud, aitäh tähelepanu eest.
Tulet meelde, et see on tõlge. Kui kirjutate kommentaare, pidage meeles, et autor neid ei loe. Kui tõeliselt soovite autoriga suhelda, siis ta on Hydra 2019 konverentsil, mis toimub 11.-12. juulil 2019 Peterburis. Piletid on saadaval ostmiseks. .
Allikas: habr.com
