Dan l-artikolu huwa traduzzjoni . Imma quddiemha ftit introduzzjoni. Kif huma ffurmati zombies? Kulħadd daħal f'sitwazzjoni fejn irid jiġbed ħabib jew kollega sal-livell tiegħu, iżda ma jaħdimx. U mhux tant miegħek daqs kemm miegħu li "ma taħdimx": fuq naħa waħda tal-iskala hemm salarju normali, kompiti, eċċ, u fuq l-oħra, il-ħtieġa li wieħed jaħseb. Il-ħsieb huwa spjaċevoli u bl-uġigħ. Huwa jċedi malajr u jkompli jikteb kodiċi mingħajr ma jixgħel moħħu xejn. Immaġina kemm hemm bżonn sforz biex tegħleb l-ostaklu tad-dgħufija mgħallma, u sempliċement ma tagħmilx dan. Hekk jiġu ffurmati zombies, li, jidher, jistgħu jitfejqu, iżda jidher li ħadd mhu se jagħmel dan.
Meta rajt dak (iva, l-istess sħabu mill-kotba) u ma jagħmilx rapport, iżda sessjoni ta 'mistoqsijiet u tweġibiet, kont ftit attenta. Fil-każ, Leslie huwa xjenzat famuż fid-dinja, l-awtur ta 'xogħlijiet fundamentali fil-kompjuters distribwiti, u tista' wkoll tkun taf bl-ittri La fil-kelma LaTeX - "Lamport TeX". It-tieni fattur allarmanti huwa l-ħtieġa tiegħu: kull min jiġi jrid (assolutament mingħajr ħlas) jisma 'koppja mir-rapporti tiegħu minn qabel, joħroġ b'mill-inqas mistoqsija waħda dwarhom, u mbagħad jiġi biss. Iddeċidejt li nara x'qed ixandar Lamport hemmhekk - u huwa kbir! Hija eżattament dik il-ħaġa, ir-rabta-pillola magica biex tfejjaq zombies. Inwissikom: mit-test, min iħobb metodoloġiji super-flessibbli u dawk li ma jħobbux jittestjaw dak li hu miktub jistgħu notevolment jaħarqu.
Wara l-habrokat, fil-fatt, tibda t-traduzzjoni tas-seminar. Igawdu l-qari!
Tkun xi tkun il-kompitu li tieħu, dejjem trid tgħaddi minn tliet passi:
- jiddeċiedi liema għan trid tilħaq;
- iddeċiedi kif se tikseb l-għan tiegħek;
- wasal għall-mira tiegħek.
Dan japplika wkoll għall-ipprogrammar. Meta niktbu kodiċi, għandna bżonn:
- jiddeċiedi x'għandu jagħmel il-programm;
- tiddetermina kif għandha twettaq il-kompitu tagħha;
- ikteb il-kodiċi korrispondenti.
L-aħħar pass, ovvjament, huwa importanti ħafna, imma mhux se nitkellem dwaru llum. Minflok, se niddiskutu l-ewwel tnejn. Kull programmatur iwettaqhom qabel ma jibda jaħdem. Ma toqgħodx bilqegħda biex tikteb sakemm ma tkunx iddeċidejt jekk tkunx qed tikteb browser jew database. Ċerta idea tal-għan trid tkun preżenti. U definittivament taħseb dwar x'se jagħmel eżattament il-programm, u ma tiktebx b'xi mod bit-tama li l-kodiċi b'xi mod jinbidel fi browser.
Kif jiġri eżattament dan il-pre-ħsieb tal-kodiċi? Kemm għandna nagħmlu sforz f’dan? Kollox jiddependi minn kemm qed insolvu l-problema kumplessa. Ejja ngħidu li rridu niktbu sistema distribwita li tollera l-ħsarat. F'dan il-każ, għandna naħsbu l-affarijiet bir-reqqa qabel ma noqogħdu bilqegħda għall-kodiċi. X'jiġri jekk irridu biss li nżidu varjabbli numru sħiħ b'1? L-ewwel daqqa t'għajn, kollox huwa trivjali hawn, u m'hemm bżonn l-ebda ħsieb, iżda mbagħad niftakru li jista 'jseħħ overflow. Għalhekk, anke sabiex tifhem jekk problema hijiex sempliċi jew kumplessa, l-ewwel trid taħseb.
Jekk taħseb dwar soluzzjonijiet possibbli għall-problema minn qabel, tista 'tevita żbalji. Iżda dan jeħtieġ li l-ħsieb tiegħek ikun ċar. Biex tikseb dan, trid tikteb il-ħsibijiet tiegħek. Jogħġobni ħafna l-kwotazzjoni ta’ Dick Guindon: “Meta tikteb, in-natura turik kemm il-ħsieb tiegħek huwa sloppy.” Jekk ma tiktebx, taħseb biss li qed taħseb. U għandek bżonn tikteb il-ħsibijiet tiegħek fil-forma ta 'speċifikazzjonijiet.
L-ispeċifikazzjonijiet iwettqu ħafna funzjonijiet, speċjalment fi proġetti kbar. Imma se nitkellem biss dwar wieħed minnhom: jgħinuna naħsbu b'mod ċar. Taħseb b'mod ċar huwa importanti ħafna u pjuttost diffiċli, għalhekk hawn għandna bżonn xi għajnuna. F'liema lingwa għandna niktbu l-ispeċifikazzjonijiet? B'mod ġenerali, din hija dejjem l-ewwel mistoqsija għall-programmaturi: f'liema lingwa se niktbu. M'hemm l-ebda tweġiba waħda korretta għaliha: il-problemi li qed insolvu huma wisq diversi. Għal xi wħud, TLA + hija lingwa ta 'speċifikazzjoni li żviluppajt. Għal oħrajn, huwa aktar konvenjenti li tuża ċ-Ċiniż. Kollox jiddependi mis-sitwazzjoni.
Aktar importanti hija mistoqsija oħra: kif tikseb ħsieb aktar ċar? Tweġiba: Irridu naħsbu bħal xjenzati. Dan huwa mod ta' ħsieb li wera ruħu matul l-aħħar 500 sena. Fix-xjenza, nibnu mudelli matematiċi tar-realtà. L-astronomija kienet forsi l-ewwel xjenza fis-sens strett tal-kelma. Fil-mudell matematiku użat fl-astronomija, il-korpi ċelesti jidhru bħala punti b'massa, pożizzjoni u momentum, għalkemm fir-realtà huma oġġetti estremament kumplessi b'muntanji u oċeani, mareat u mareat. Dan il-mudell, bħal kull ieħor, inħoloq biex isolvi ċerti problemi. Huwa kbir biex tiddetermina fejn tippunta t-teleskopju jekk ikollok bżonn issib pjaneta. Imma jekk trid tbassar it-temp fuq din il-pjaneta, dan il-mudell mhux se jaħdem.
Il-matematika tippermettilna niddeterminaw il-proprjetajiet ta 'mudell. U x-xjenza turi kif dawn il-proprjetajiet jirrelataw mar-realtà. Ejja nitkellmu dwar ix-xjenza tagħna, ix-xjenza tal-kompjuter. Ir-realtà li naħdmu magħha hija sistemi ta’ kompjuters ta’ diversi tipi: proċessuri, consoles tal-logħob, kompjuters, programmi ta’ eżekuzzjoni, eċċ. Se nitkellem dwar it-tħaddim ta 'programm fuq kompjuter, iżda b'mod ġenerali, dawn il-konklużjonijiet kollha japplikaw għal kwalunkwe sistema tal-kompjuter. Fix-xjenza tagħna, nużaw ħafna mudelli differenti: il-magna Turing, settijiet parzjalment ordnati ta 'avvenimenti, u ħafna oħrajn.
X'inhu programm? Dan huwa kwalunkwe kodiċi li jista 'jiġi kkunsidrat b'mod indipendenti. Ejja ngħidu li għandna bżonn niktbu browser. Aħna nwettqu tliet kompiti: aħna nfasslu l-fehma tal-utent tal-programm, imbagħad niktbu d-dijagramma ta 'livell għoli tal-programm, u finalment niktbu l-kodiċi. Hekk kif niktbu l-kodiċi, nindunaw li għandna bżonn niktbu formatter tat-test. Hawnhekk irridu nerġgħu nsolvu tliet problemi: tiddetermina liema test se terġa 'lura din l-għodda; agħżel algoritmu għall-ifformattjar; ikteb il-kodiċi. Dan il-kompitu għandu s-subkompitu tiegħu stess: daħħal b'mod korrett sing fil-kliem. Aħna nsolvu wkoll dan is-subtask fi tliet passi - kif tistgħu taraw, huma ripetuti f'ħafna livelli.
Ejja nikkunsidraw f'aktar dettall l-ewwel pass: liema problema jsolvi l-programm. Hawnhekk, ħafna drabi aħna nimudellaw programm bħala funzjoni li tieħu xi input u tipproduċi xi output. Fil-matematika, funzjoni hija normalment deskritta bħala sett ordnat ta 'pari. Pereżempju, il-funzjoni tal-kwadru għal numri naturali hija deskritta bħala s-sett {<0,0>, <1,1>, <2,4>, <3,9>, ...}. Id-dominju ta 'tali funzjoni huwa s-sett tal-ewwel elementi ta' kull par, jiġifieri, in-numri naturali. Biex niddefinixxu funzjoni, irridu nispeċifikaw l-ambitu u l-formula tagħha.
Iżda l-funzjonijiet fil-matematika mhumiex l-istess bħall-funzjonijiet fil-lingwi tal-ipprogrammar. Il-matematika hija ħafna aktar faċli. Peress li m'għandix ħin għal eżempji kumplessi, ejja nikkunsidraw wieħed sempliċi: funzjoni f'C jew metodu statiku f'Java li jirritorna l-akbar diviżur komuni ta 'żewġ interi. Fl-ispeċifikazzjoni ta 'dan il-metodu, aħna se niktbu: tikkalkula GCD(M,N) għall-argumenti M и Nfejn GCD(M,N) - funzjoni li d-dominju tagħha huwa s-sett ta’ pari ta’ numri interi, u l-valur tar-ritorn huwa l-akbar numru sħiħ li huwa diviżibbli b’ M и N. Dan il-mudell kif jirrelata mar-realtà? Il-mudell jopera fuq interi, filwaqt li f'C jew Java għandna 32-bit int. Dan il-mudell jippermettilna niddeċiedu jekk l-algoritmu huwiex korrett GCD, iżda mhux se jipprevjeni żbalji ta 'overflow. Dan ikun jeħtieġ mudell aktar kumpless, li għalih m'hemmx ħin.
Ejja nitkellmu dwar il-limitazzjonijiet ta 'funzjoni bħala mudell. Xi programmi (bħal sistemi operattivi) mhux biss jirritorna ċertu valur għal ċerti argumenti, jistgħu jaħdmu kontinwament. Barra minn hekk, il-funzjoni bħala mudell mhix adattata tajjeb għat-tieni pass: tippjana kif issolvi l-problema. Issortjar malajr u sort bużżieqa jikkalkulaw l-istess funzjoni, iżda huma algoritmi kompletament differenti. Għalhekk, biex tiddeskrivi kif jintlaħaq l-għan tal-programm, nuża mudell differenti, ejja nsejħulu l-mudell ta 'mġieba standard. Il-programm fih huwa rappreżentat bħala sett tal-imġieba permissibbli kollha, li kull wieħed minnhom, imbagħad, huwa sekwenza ta 'stati, u l-istat huwa l-assenjazzjoni ta' valuri għal varjabbli.
Ejja naraw kif ikun it-tieni pass għall-algoritmu Ewklide. Għandna bżonn nikkalkulaw GCD(M, N). Aħna initialize M kif xU N kif y, imbagħad ripetutament naqqas l-iżgħar minn dawn il-varjabbli mill-akbar sakemm ikunu ugwali. Per eżempju, jekk M = 12U N = 18, nistgħu niddeskrivu l-imġieba li ġejja:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
U jekk M = 0 и N = 0? Iż-żero huwa diviżibbli bin-numri kollha, għalhekk m'hemm l-ebda diviżur akbar f'dan il-każ. F'din is-sitwazzjoni, irridu mmorru lura għall-ewwel pass u nistaqsu: għandna verament bżonn nikkalkulaw GCD għal numri mhux pożittivi? Jekk dan ma jkunx meħtieġ, allura għandek bżonn biss li tibdel l-ispeċifikazzjoni.
Hawnhekk għandna nagħmlu digressjoni żgħira dwar il-produttività. Ħafna drabi titkejjel fin-numru ta 'linji ta' kodiċi miktuba kuljum. Imma x-xogħol tiegħek huwa ħafna aktar utli jekk teħles minn ċertu numru ta 'linji, għaliex għandek inqas spazju għall-bugs. U l-eħfef mod biex teħles mill-kodiċi huwa fl-ewwel pass. Huwa kompletament possibbli li inti sempliċiment m'għandekx bżonn il-qniepen u sfafar kollha li qed tipprova timplimenta. L-aktar mod mgħaġġel biex tissimplifika programm u tiffranka l-ħin huwa li ma tagħmilx affarijiet li m'għandhomx isiru. It-tieni pass huwa t-tieni l-aktar potenzjal li jiffranka l-ħin. Jekk tkejjel il-produttività f'termini ta 'linji miktuba, allura taħseb dwar kif twettaq kompitu se tagħmel inti inqas produttivi, għax tista 'ssolvi l-istess problema b'inqas kodiċi. Ma nistax nagħti statistika eżatta hawn, għax m'għandi l-ebda mod kif ngħodd in-numru ta' linji li ma ktibtx minħabba l-fatt li qattajt ħin fuq l-ispeċifikazzjoni, jiġifieri fuq l-ewwel u t-tieni pass. U l-esperiment ma jistax jiġi stabbilit hawn lanqas, għax fl-esperiment m'għandniex id-dritt li nlestu l-ewwel pass, il-kompitu huwa predeterminat.
Huwa faċli li tinjora ħafna diffikultajiet fl-ispeċifikazzjonijiet informali. M'hemm xejn diffiċli fil-kitba ta 'speċifikazzjonijiet stretti għall-funzjonijiet, mhux se niddiskuti dan. Minflok, nitkellmu dwar il-kitba ta 'speċifikazzjonijiet b'saħħithom għall-imgieba standard. Hemm teorema li tgħid li kwalunkwe sett ta 'mġieba jista' jiġi deskritt bl-użu tal-proprjetà tas-sigurtà (sigurtà) u proprjetajiet tas-sopravivenza (ħajja). Is-sigurtà tfisser li ma jiġri xejn ħażin, il-programm mhux se jagħti tweġiba żbaljata. Is-sopravivenza tfisser li llum jew għada se tiġri xi ħaġa tajba, jiġifieri l-programm se jagħti t-tweġiba t-tajba illum jew għada. Bħala regola, is-sigurtà hija indikatur aktar importanti, l-iżbalji ħafna drabi jseħħu hawn. Għalhekk, biex tiffranka l-ħin, mhux se nitkellem dwar is-sopravivenza, għalkemm hija, ovvjament, importanti wkoll.
Aħna niksbu s-sigurtà billi nippreskrivu, l-ewwel, is-sett ta 'stati inizjali possibbli. U t-tieni, relazzjonijiet mal-istati kollha possibbli li jmiss għal kull stat. Ejja naġixxu bħal xjenzati u niddefinixxu stati matematikament. Is-sett ta 'stati inizjali huwa deskritt b'formula, pereżempju, fil-każ tal-algoritmu Ewklide: (x = M) ∧ (y = N). Għal ċerti valuri M и N hemm stat inizjali wieħed biss. Ir-relazzjoni ma 'l-istat li jmiss hija deskritta b'formula li fiha l-varjabbli ta' l-istat li jmiss jinkitbu b'prim, u l-varjabbli ta 'l-istat kurrenti jinkitbu mingħajr prime. Fil-każ tal-algoritmu ta’ Ewklide, se nittrattaw id-disġunzjoni ta’ żewġ formuli, li waħda minnhom x huwa l-akbar valur, u fit-tieni - y:
Fl-ewwel każ, il-valur il-ġdid ta 'y huwa ugwali għall-valur preċedenti ta' y, u nġibu l-valur il-ġdid ta 'x billi nnaqqsu l-varjabbli iżgħar mill-varjabbli akbar. Fit-tieni każ, nagħmlu l-oppost.
Ejja mmorru lura għall-algoritmu ta 'Ewklide. Ejja nassumu mill-ġdid li M = 12, N = 18. Dan jiddefinixxi stat inizjali wieħed, (x = 12) ∧ (y = 18). Aħna mbagħad daħħal dawk il-valuri fil-formula ta 'hawn fuq u nikseb:
Hawn l-unika soluzzjoni possibbli: x' = 18 - 12 ∧ y' = 12u nġibu l-imġieba: [x = 12, y = 18]. Bl-istess mod, nistgħu niddeskrivu l-istati kollha fl-imġieba tagħna: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Fl-aħħar stat [x = 6, y = 6] iż-żewġ partijiet tal-espressjoni se jkunu foloz, għalhekk m'għandha l-ebda stat li jmiss. Allura, għandna speċifikazzjoni kompleta tat-tieni pass - kif tistgħu taraw, din hija matematika pjuttost ordinarja, bħal fl-inġiniera u x-xjenzati, u mhux stramba, bħal fix-xjenza tal-kompjuter.
Dawn iż-żewġ formuli jistgħu jingħaqdu f'formula waħda ta 'loġika temporali. Hija eleganti u faċli biex tispjega, iżda m'hemmx ħin għaliha issa. Jista 'jkollna bżonn loġika temporali biss għall-proprjetà tal-ħajja, mhix meħtieġa għas-sigurtà. Ma nħobbx il-loġika temporali bħala tali, mhix matematika pjuttost ordinarja, iżda fil-każ tal-ħajja hija ħażen meħtieġ.
Fl-algoritmu ta 'Ewklide, għal kull valur x и y għandhom valuri uniċi x' и y', li jagħmlu r-relazzjoni mal-istat li jmiss vera. Fi kliem ieħor, l-algoritmu ta 'Ewklide huwa deterministiku. Biex timmudella algoritmu mhux deterministiku, l-istat attwali jeħtieġ li jkollu diversi stati futuri possibbli, u li kull valur varjabbli mhux ipprajmat ikollu valuri varjabbli multipli ipprajtati b'tali mod li r-relazzjoni mal-istat li jmiss tkun vera. Dan huwa faċli li tagħmel, imma jien mhux se nagħti eżempji issa.
Biex tagħmel għodda ta 'ħidma, għandek bżonn matematika formali. Kif tagħmel l-ispeċifikazzjoni formali? Biex nagħmlu dan, għandna bżonn lingwa formali, pereżempju, . L-ispeċifikazzjoni tal-algoritmu Ewklide tidher bħal din f'din il-lingwa:
Simbolu tas-sinjal ugwali bi trijangolu jfisser li l-valur fuq ix-xellug tas-sinjal huwa definit bħala ugwali għall-valur fuq il-lemin tas-sinjal. Essenzjalment, l-ispeċifikazzjoni hija definizzjoni, fil-każ tagħna żewġ definizzjonijiet. Għall-ispeċifikazzjoni f'TLA+, trid iżżid dikjarazzjonijiet u xi sintassi, bħal fil-pjastra ta' hawn fuq. F'ASCII ikun jidher bħal dan:
Kif tistgħu taraw, xejn ikkumplikat. L-ispeċifikazzjoni għal TLA+ tista 'tiġi ttestjata, jiġifieri tevita l-imgieba kollha possibbli f'mudell żgħir. Fil-każ tagħna, dan il-mudell se jkun ċerti valuri M и N. Dan huwa metodu ta 'verifika effiċjenti ħafna u sempliċi li huwa kompletament awtomatiku. Huwa wkoll possibbli li tikteb provi tal-verità formali u tiċċekkjahom mekkanikament, iżda dan jieħu ħafna ħin, għalhekk kważi ħadd ma jagħmel dan.
L-iżvantaġġ ewlieni ta 'TLA+ huwa li huwa matematika, u l-programmaturi u x-xjenzati tal-kompjuter jibżgħu mill-matematika. L-ewwel daqqa t'għajn, din tinstema' qisha ċajta, iżda, sfortunatament, infisserha bis-serjetà kollha. Il-kollega tiegħi kien qed jgħidli kif ipprova jispjega TLA+ lil diversi żviluppaturi. Hekk kif il-formuli dehru fuq l-iskrin, immedjatament saru għajnejn tal-ħġieġ. Mela jekk TLA+ ibeżżalek, tista 'tuża , huwa tip ta 'lingwa ta' programmar tal-ġugarelli. Espressjoni f'PlusCal tista' tkun kwalunkwe espressjoni TLA+, jiġifieri, b'mod ġenerali, kwalunkwe espressjoni matematika. Barra minn hekk, PlusCal għandu sintassi għal algoritmi mhux deterministiċi. Minħabba li PlusCal jista 'jikteb kwalunkwe espressjoni TLA+, PlusCal huwa ħafna aktar espressiv minn kwalunkwe lingwa ta' programmar reali. Sussegwentement, PlusCal huwa miġbur fi speċifikazzjoni TLA+ li tinqara faċilment. Dan ma jfissirx, ovvjament, li l-ispeċifikazzjoni PlusCal kumplessa se tinbidel f'waħda sempliċi fuq TLA + - biss il-korrispondenza bejniethom hija ovvja, mhux se jkun hemm kumplessità addizzjonali. Fl-aħħarnett, din l-ispeċifikazzjoni tista 'tiġi vverifikata minn għodod TLA+. Kollox ma 'kollox, PlusCal jista' jgħin biex tingħeleb il-fobija tal-matematika u huwa faċli biex jinftiehem anke għal programmaturi u xjenzati tal-kompjuter. Fil-passat, ippublikajt algoritmi fuqha għal xi żmien (madwar 10 snin).
Forsi xi ħadd joġġezzjona li TLA + u PlusCal huma matematika, u l-matematika taħdem biss fuq eżempji ivvintati. Fil-prattika, għandek bżonn lingwa reali b'tipi, proċeduri, oġġetti, eċċ. Dan huwa ħażin. Hawn hu dak li jikteb Chris Newcomb, li ħadem fl-Amazon: “Użajna TLA+ fuq għaxar proġetti ewlenin, u f’kull każ, l-użu tiegħu għamel differenza sinifikanti għall-iżvilupp għax stajna naqbdu bugs perikolużi qabel ma nilqgħu l-produzzjoni, u għax tana l-għarfien u l-kunfidenza li kellna bżonn biex tagħmel ottimizzazzjonijiet aggressivi tal-prestazzjoni mingħajr ma taffettwa l-verità tal-programm". Ħafna drabi tista 'tisma' li meta tuża metodi formali, aħna nġibu kodiċi ineffiċjenti - fil-prattika, kollox huwa eżattament l-oppost. Barra minn hekk, hemm opinjoni li l-maniġers ma jistgħux ikunu konvinti mill-ħtieġa għal metodi formali, anki jekk il-programmaturi huma konvinti mill-utilità tagħhom. U Newcomb jikteb: "Il-maniġers issa qed jimbuttaw ħafna biex jiktbu speċifikazzjonijiet għal TLA +, u speċifikament jallokaw ħin għal dan". Allura meta l-maniġers jaraw li TLA+ qed jaħdem, huma kuntenti li jaċċettawh. Chris Newcomb kiteb dan madwar sitt xhur ilu (Ottubru 2014), iżda issa, sa fejn naf jien, TLA+ jintuża f'14-il proġett, mhux f'10. Eżempju ieħor huwa fid-disinn tal-XBox 360. Intern ġie għand Charles Thacker u kiteb speċifikazzjoni għas-sistema tal-memorja. Grazzi għal din l-ispeċifikazzjoni, instab bug li kieku ma kienx innutat, u li minħabba fih kull XBox 360 kien jikkraxxja wara erba' sigħat ta' użu. L-inġiniera tal-IBM ikkonfermaw li t-testijiet tagħhom ma kinux isibu dan il-bug.
Tista 'taqra aktar dwar TLA + fuq l-Internet, iżda issa ejja nitkellmu dwar speċifikazzjonijiet informali. Rari għandna niktbu programmi li jikkalkulaw l-inqas diviżur komuni u simili. Ħafna aktar spiss niktbu programmi bħall-għodda pretty-printer li ktibt għal TLA+. Wara l-aktar proċessar sempliċi, il-kodiċi TLA + jidher bħal dan:
Iżda fl-eżempju ta 'hawn fuq, l-utent x'aktarx ried li l-konġunzjoni u s-sinjali ugwali jiġu allinjati. Allura l-ifformattjar korrett ikun jidher aktar bħal dan:
Ejja nikkunsidraw eżempju ieħor:
Hawnhekk, għall-kuntrarju, l-allinjament tas-sinjali ugwali, żieda, u multiplikazzjoni fis-sors kien każwali, għalhekk l-ipproċessar l-aktar sempliċi huwa pjuttost biżżejjed. B'mod ġenerali, m'hemm l-ebda definizzjoni matematika eżatta ta 'ifformattjar korrett, minħabba li "korretta" f'dan il-każ tfisser "dak li jrid l-utent", u dan ma jistax jiġi determinat matematikament.
Jidher li jekk ma jkollniex definizzjoni tal-verità, allura l-ispeċifikazzjoni hija inutli. Imma mhux. Sempliċement għax ma nafux x’għandu jagħmel programm ma jfissirx li m’għandniex bżonn naħsbu dwar kif jaħdem—anzi, irridu nagħmlu aktar sforz fih. L-ispeċifikazzjoni hija speċjalment importanti hawn. Huwa impossibbli li jiġi ddeterminat l-aħjar programm għall-istampar strutturat, iżda dan ma jfissirx li m'għandniex neħduh xejn, u l-kitba tal-kodiċi bħala fluss ta 'kuxjenza mhix ħaġa tajba. Fl-aħħar, ktibt speċifikazzjoni ta 'sitt regoli b'definizzjonijiet fil-forma ta’ kummenti f'fajl java. Hawn eżempju ta 'waħda mir-regoli: a left-comment token is LeftComment aligned with its covering token. Din ir-regola hija miktuba bl-Ingliż matematiku, ngħidu aħna: LeftComment aligned, left-comment и covering token - termini b'definizzjonijiet. Dan huwa kif il-matematiċi jiddeskrivu l-matematika: jiktbu definizzjonijiet ta 'termini u, ibbażati fuqhom, regoli. Il-benefiċċju ta 'speċifikazzjoni bħal din huwa li sitt regoli huma ħafna aktar faċli biex jinftiehmu u jiġu debug minn 850 linja ta' kodiċi. Irrid ngħid li l-kitba ta 'dawn ir-regoli ma kinitx faċli, ħadet ħafna ħin biex jiġu debugjati. Speċjalment għal dan il-għan, ktibt kodiċi li rrapporta liema regola ntużat. Grazzi għall-fatt li ttestjajt dawn is-sitt regoli fuq diversi eżempji, ma kellix għalfejn niddibaggja 850 linja ta 'kodiċi, u l-bugs irriżultaw li kienu pjuttost faċli biex issibhom. Java għandu għodda kbira għal dan. Kieku kont għadni kif ktibt il-kodiċi, kien jieħu ħafna aktar żmien, u l-ifformattjar kien ikun ta 'kwalità fqira.
Għaliex ma setgħetx tintuża speċifikazzjoni formali? Min-naħa waħda, l-eżekuzzjoni korretta mhix wisq importanti hawn. Il-printouts strutturali huma marbuta li ma jogħġbu lil ħadd, għalhekk ma kellix għalfejn inġibha taħdem sew fis-sitwazzjonijiet strambi kollha. Saħansitra aktar importanti huwa l-fatt li ma kellix għodod adegwati. Il-kontrollur tal-mudell TLA + huwa inutli hawn, għalhekk ikolli nikteb l-eżempji manwalment.
L-ispeċifikazzjoni ta 'hawn fuq għandha karatteristiċi komuni għall-ispeċifikazzjonijiet kollha. Huwa livell ogħla mill-kodiċi. Jista 'jiġi implimentat fi kwalunkwe lingwa. Kwalunkwe għodda jew metodu huma inutli biex tiktebha. L-ebda kors tal-ipprogrammar ma jgħinek tikteb din l-ispeċifikazzjoni. U m'hemm l-ebda għodda li tista 'tagħmel din l-ispeċifikazzjoni bla bżonn, sakemm, ovvjament, ma tkunx qed tikteb lingwa speċifikament għall-kitba ta' programmi stampati strutturati f'TLA+. Fl-aħħarnett, din l-ispeċifikazzjoni ma tgħid xejn dwar eżattament kif se niktbu l-kodiċi, tiddikjara biss dak li jagħmel dan il-kodiċi. Aħna niktbu l-ispeċifikazzjoni biex tgħinna naħsbu fil-problema qabel ma nibdew naħsbu dwar il-kodiċi.
Iżda din l-ispeċifikazzjoni għandha wkoll karatteristiċi li jiddistingwuha minn speċifikazzjonijiet oħra. 95% ta 'speċifikazzjonijiet oħra huma sinifikament iqsar u aktar sempliċi:
Barra minn hekk, din l-ispeċifikazzjoni hija sett ta' regoli. Bħala regola, dan huwa sinjal ta 'speċifikazzjoni fqira. Nifhem il-konsegwenzi ta 'sett ta' regoli huwa pjuttost diffiċli, u huwa għalhekk li kelli nqatta 'ħafna ħin niddibaggjahom. Madankollu, f'dan il-każ, ma stajtx insib mod aħjar.
Ta’ min jgħid ftit kliem dwar programmi li jaħdmu kontinwament. Bħala regola, jaħdmu b'mod parallel, pereżempju, sistemi operattivi jew sistemi distribwiti. Ftit nies jistgħu jifhmuhom mentalment jew fuq il-karta, u jien mhux wieħed minnhom, għalkemm darba kont kapaċi nagħmel dan. Għalhekk, neħtieġu għodod li jiċċekkjaw ix-xogħol tagħna - pereżempju, TLA + jew PlusCal.
Għaliex kien meħtieġ li tikteb speċifikazzjoni jekk diġà kont naf x'għandu jagħmel eżattament il-kodiċi? Fil-fatt, ħsibt biss li kont naf. Barra minn hekk, bi speċifikazzjoni, barrani m'għadux jeħtieġ li jidħol fil-kodiċi biex jifhem x'jagħmel eżattament. Għandi regola: m'għandux ikun hemm regoli ġenerali. Hemm eċċezzjoni għal din ir-regola, ovvjament, hija l-unika regola ġenerali li nsegwi: l-ispeċifikazzjoni ta 'dak li jagħmel il-kodiċi għandha tgħid lin-nies dak kollu li għandhom bżonn ikunu jafu meta jużaw il-kodiċi.
Allura x'għandhom bżonn ikunu jafu eżattament il-programmaturi dwar il-ħsieb? Biex nibdew, l-istess bħal kulħadd: jekk ma tiktebx, allura jidhirlek biss li qed taħseb. Ukoll, trid taħseb qabel ma tikkodifika, li jfisser li għandek bżonn tikteb qabel ma tikkodifika. L-ispeċifikazzjoni hija dak li niktbu qabel ma nibdew il-kodifikazzjoni. Hemm bżonn ta' speċifikazzjoni għal kwalunkwe kodiċi li jista' jintuża jew jiġi modifikat minn kulħadd. U dan "xi ħadd" jista 'jkun l-awtur tal-kodiċi innifsu xahar wara li nkiteb. Speċifikazzjoni hija meħtieġa għal programmi u sistemi kbar, għal klassijiet, għal metodi, u xi kultant anke għal sezzjonijiet kumplessi ta 'metodu wieħed. X'għandu jinkiteb eżattament dwar il-kodiċi? Trid tiddeskrivi x'tagħmel, jiġifieri, x'jista' jkun utli għal kull persuna li tuża dan il-kodiċi. Xi drabi jista 'jkun meħtieġ ukoll li jiġi speċifikat kif il-kodiċi jwettaq l-iskop tiegħu. Jekk għaddejna minn dan il-metodu fil-kors ta 'algoritmi, allura nsejħulu algoritmu. Jekk hija xi ħaġa aktar speċjali u ġdida, allura nsejħulha disinn ta 'livell għoli. M'hemm l-ebda differenza formali hawnhekk: it-tnejn huma mudell astratt ta 'programm.
Kif eżattament għandek tikteb speċifikazzjoni tal-kodiċi? Il-ħaġa prinċipali: għandu jkun livell ogħla mill-kodiċi innifsu. Għandu jiddeskrivi l-istati u l-imgieba. Għandu jkun strett daqs kemm jeħtieġ il-kompitu. Jekk qed tikteb speċifikazzjoni dwar kif biċċa xogħol trid tiġi implimentata, tista' tiktebha f'psewdocode jew b'PlusCal. Għandek bżonn titgħallem kif tikteb speċifikazzjonijiet fuq speċifikazzjonijiet formali. Dan jagħtik il-ħiliet meħtieġa li jgħinuk ma’ dawk informali wkoll. Kif titgħallem tikteb speċifikazzjonijiet formali? Meta tgħallimna nipprogrammaw, ktibna programmi u mbagħad niddebuggjawhom. Huwa l-istess hawn: ikteb l-ispeċifikazzjoni, iċċekkjaha mal-kontrollur tal-mudell, u waħħal il-bugs. TLA+ jista' ma jkunx l-aħjar lingwa għal speċifikazzjoni formali, u lingwa oħra x'aktarx li tkun aħjar għall-bżonnijiet speċifiċi tiegħek. Il-vantaġġ ta 'TLA+ huwa li jgħallem il-ħsieb matematiku tajjeb ħafna.
Kif torbot l-ispeċifikazzjoni u l-kodiċi? Bl-għajnuna ta 'kummenti li jorbtu kunċetti matematiċi u l-implimentazzjoni tagħhom. Jekk taħdem ma 'graffs, allura fil-livell tal-programm ser ikollok matriċi ta' nodi u arrays ta 'links. Għalhekk, għandek tikteb eżattament kif il-graff huwa implimentat minn dawn l-istrutturi ta 'programmar.
Għandu jiġi nnutat li l-ebda wieħed minn dawn t'hawn fuq ma japplika għall-proċess attwali tal-kitba tal-kodiċi. Meta tikteb il-kodiċi, jiġifieri, twettaq it-tielet pass, jeħtieġ ukoll li taħseb u taħseb permezz tal-programm. Jekk subkompitu jirriżulta li huwa kumpless jew mhux ovvju, għandek bżonn tikteb speċifikazzjoni għaliha. Imma jien mhux qed nitkellem dwar il-kodiċi innifsu hawn. Tista 'tuża kwalunkwe lingwa ta' programmar, kwalunkwe metodoloġija, mhux dwarhom. Ukoll, l-ebda wieħed minn dawn t'hawn fuq ma jelimina l-ħtieġa li tittestja u tiddibaggja l-kodiċi. Anke jekk il-mudell astratt huwa miktub b'mod korrett, jista 'jkun hemm bugs fl-implimentazzjoni tiegħu.
L-ispeċifikazzjonijiet tal-kitba huwa pass addizzjonali fil-proċess tal-kodifikazzjoni. Grazzi għaliha, ħafna żbalji jistgħu jinqabdu b'inqas sforz - dan nafu mill-esperjenza tal-programmaturi mill-Amazon. Bi speċifikazzjonijiet, il-kwalità tal-programmi ssir ogħla. Allura għala, allura, aħna daqshekk sikwit noqogħdu mingħajrhom? Għax il-kitba hija diffiċli. U l-kitba hija diffiċli, għax għal dan trid taħseb, u taħseb huwa diffiċli wkoll. Dejjem huwa aktar faċli li tippretendi dak li taħseb. Hawnhekk tista 'tiġbed analoġija mal-ġiri - inqas ma tmexxi, iktar ma tmexxi bil-mod. Għandek bżonn tħarreġ il-muskoli tiegħek u tipprattika l-kitba. Ħtieġa prattika.
L-ispeċifikazzjoni tista' tkun żbaljata. Jista' jkun li għamilt żball x'imkien, jew ir-rekwiżiti setgħu nbidlu, jew jista' jkun hemm bżonn li jsir titjib. Kwalunkwe kodiċi li xi ħadd juża jrid jinbidel, għalhekk illum jew għada l-ispeċifikazzjoni ma tibqax taqbel mal-programm. Idealment, f'dan il-każ, għandek bżonn tikteb speċifikazzjoni ġdida u tikteb kompletament mill-ġdid il-kodiċi. Nafu sew li ħadd ma jagħmel hekk. Fil-prattika, aħna nagħtu garża tal-kodiċi u possibbilment naġġornaw l-ispeċifikazzjoni. Jekk dan huwa marbut li jseħħ illum jew għada, allura għaliex tikteb speċifikazzjonijiet? L-ewwelnett, għall-persuna li se teditja l-kodiċi tiegħek, kull kelma żejda fl-ispeċifikazzjoni tkun tiswa l-piż tagħha fid-deheb, u din il-persuna tista 'tkun int stess. Spiss inniżżel lili nnifsi talli ma nsibx biżżejjed speċifikazzjoni meta nkun qed neditja l-kodiċi tiegħi. U nikteb aktar speċifikazzjonijiet minn kodiċi. Għalhekk, meta teditja l-kodiċi, l-ispeċifikazzjoni dejjem teħtieġ li tiġi aġġornata. It-tieni nett, ma 'kull reviżjoni, il-kodiċi tmur għall-agħar, isir aktar u aktar diffiċli biex jinqara u jinżamm. Din hija żieda fl-entropija. Imma jekk ma tibdax bi spec, allura kull linja li tikteb tkun editjar, u l-kodiċi se jkun diffiċli u diffiċli biex jinqara mill-bidu.
Kif intqal , l-ebda battalja ma ntrebħet bi pjan, u l-ebda battalja ma ntrebħet mingħajr pjan. U kien jaf xi ħaġa jew tnejn dwar il-battalji. Hemm opinjoni li l-kitba tal-ispeċifikazzjonijiet hija ħela ta 'ħin. Xi drabi dan huwa minnu, u l-kompitu huwa tant sempliċi li m'hemm xejn x'taħseb. Imma għandek dejjem tiftakar li meta jgħidulek biex ma tiktebx speċifikazzjonijiet, jgħidulek biex ma taħsibx. U għandek taħseb dwarha kull darba. Li taħseb fil-kompitu ma tiggarantixxix li mhux se tagħmel żbalji. Kif nafu, ħadd ma vvinta l-bastun maġiku, u l-ipprogrammar huwa kompitu diffiċli. Imma jekk ma taħsibx fil-problema, int garantit li tagħmel żbalji.
Tista' taqra aktar dwar TLA + u PlusCal fuq websajt speċjali, tista' tmur hemm mill-home page tiegħi . Dak kollu għalija, grazzi tal-attenzjoni tiegħek.
Jekk jogħġbok innota li din hija traduzzjoni. Meta tikteb kummenti, ftakar li l-awtur mhux se jaqrahom. Jekk verament trid tiċċettja mal-awtur, allura jkun fil-konferenza Hydra 2019, li se ssir bejn il-11 u t-12 ta 'Lulju, 2019 f'San Pietruburgu. Biljetti jistgħu jinxtraw .
Sors: www.habr.com