Å is ir tulkoÅ”anas raksts . Bet pirms tam ir Ä«ss ievads. KÄ veidojas zombiji? Ikviens ir nonÄcis situÄcijÄ, kad vÄlas pacelt draugu vai kolÄÄ£i lÄ«dz savam lÄ«menim, bet tas neizdodas. TurklÄt āneizdodasā ne tik daudz jums, bet viÅam: vienÄ skalas pusÄ ir normÄla alga, uzdevumi un tÄ tÄlÄk, bet otrÄ ir nepiecieÅ”amÄ«ba domÄt. DomÄÅ”ana ir nepatÄ«kama un sÄpÄ«ga. ViÅÅ” Ätri padodas un turpina rakstÄ«t kodu, neizmantojot savas smadzenes. JÅ«s saprotat, cik daudz pūļu ir nepiecieÅ”ams, lai pÄrvarÄtu iemÄcÄ«tÄs bezpalÄ«dzÄ«bas barjeru, un jÅ«s to vienkÄrÅ”i nedarÄt. TÄ veidojas zombiji, kurus it kÄ ir iespÄjams izÄrstÄt, bet Ŕķiet, ka neviens to nedarÄ«s.
Kad es to redzÄju (jÄ, tas pats draugs no mÄcÄ«bu grÄmatÄm) un nesniedz ziÅojumu, bet gan jautÄjumu un atbilžu sesiju, es biju nedaudz piesardzÄ«gs. Katram gadÄ«jumam, Leslijs ir pasaulÄ pazÄ«stams zinÄtnieks, izkliedÄtÄs skaitļoÅ”anas pamatdarbu autors, un jÅ«s, iespÄjams, viÅu pazÄ«stat arÄ« pÄc LaTeX burtiem La - āLamport TeXā. Otrs satraucoÅ”ais faktors ir viÅa prasÄ«ba: katram atnÄkuÅ”ajam ir (pilnÄ«gi bez maksas) iepriekÅ” jÄnoklausÄs pÄris viÅa referÄtu, jÄizdomÄ vismaz viens jautÄjums par tiem un tikai tad jÄnÄk. Es nolÄmu redzÄt, ko Lamports tur pÄrraida, un tas ir lieliski! Tas ir tieÅ”i tas, burvju saiÅ”u tablete zombiju ÄrstÄÅ”anai. BrÄ«dinu: teksts var nopietni sadedzinÄt tos, kam patÄ«k Ä«paÅ”i veiklÄs metodikas un kuriem nepatÄ«k pÄrbaudÄ«t rakstÄ«to.
PÄc habrokata faktiski sÄkas seminÄra tulkoÅ”ana. Izbaudi lasÄ«Å”anu!
NeatkarÄ«gi no tÄ, kÄdu uzdevumu jÅ«s uzÅematies, jums vienmÄr ir jÄveic trÄ«s darbÄ«bas:
- izlemiet, kÄdu mÄrÄ·i vÄlaties sasniegt;
- izlemiet, kÄ tieÅ”i jÅ«s sasniegsiet savu mÄrÄ·i;
- sasniegt savu mÄrÄ·i.
Tas attiecas arÄ« uz programmÄÅ”anu. Kad mÄs rakstÄm kodu, mums ir nepiecieÅ”ams:
- izlemt, kas tieÅ”i programmai jÄdara;
- precÄ«zi noteikt, kÄ tai bÅ«tu jÄpilda savs uzdevums;
- uzrakstiet atbilstoŔo kodu.
PÄdÄjais solis, protams, ir ļoti svarÄ«gs, bet es par to Å”odien nerunÄÅ”u. TÄ vietÄ mÄs apspriedÄ«sim pirmos divus. Katrs programmÄtÄjs tos veic pirms darba sÄkÅ”anas. JÅ«s nesÄdat, lai rakstÄ«tu, ja vien neesat izlÄmis, ko rakstÄt: pÄrlÅ«kprogrammu vai datu bÄzi. JÄbÅ«t noteiktam priekÅ”statam par mÄrÄ·i. Un jÅ«s noteikti domÄjat par to, ko tieÅ”i programma darÄ«s, un nerakstiet to nejauÅ”i, cerot, ka pats kods kaut kÄ pÄrvÄrtÄ«sies par pÄrlÅ«kprogrammu.
KÄ tieÅ”i notiek Ŕī koda iepriekÅ”Äja domÄÅ”ana? Cik daudz pūļu mums vajadzÄtu pielikt Å”ajÄ jautÄjumÄ? Tas viss ir atkarÄ«gs no tÄ, cik sarežģītu problÄmu mÄs risinÄm. PieÅemsim, ka mÄs vÄlamies uzrakstÄ«t defektiem izturÄ«gu sadalÄ«tu sistÄmu. Å ajÄ gadÄ«jumÄ mums vajadzÄtu rÅ«pÄ«gi pÄrdomÄt lietas, pirms apsÄsties pie kodÄÅ”anas. Ko darÄ«t, ja mums vienkÄrÅ”i jÄpalielina vesels mainÄ«gais par 1? No pirmÄ acu uzmetiena Å”eit viss ir triviÄls un nav jÄdomÄ, bet tad atceramies, ka var rasties pÄrplÅ«de. TÄpÄc, pat lai saprastu, vai problÄma ir vienkÄrÅ”a vai sarežģīta, vispirms ir jÄdomÄ.
Ja iepriekÅ” pÄrdomÄjat iespÄjamos problÄmas risinÄjumus, varat izvairÄ«ties no kļūdÄm. Bet tas prasa, lai jÅ«su domÄÅ”ana bÅ«tu skaidra. Lai to panÄktu, jums ir jÄpieraksta savas domas. Man patÄ«k Dika Gindona citÄts: āKad tu raksti, daba parÄda, cik pavirÅ”a ir tava domÄÅ”ana.ā Ja jÅ«s nerakstÄt, jÅ«s tikai domÄjat, ka domÄjat. Un jums ir jÄpieraksta savas domas specifikÄciju veidÄ.
SpecifikÄcijas kalpo daudzÄm funkcijÄm, Ä«paÅ”i lielos projektos. Bet es runÄÅ”u tikai par vienu no tiem: tie palÄ«dz mums skaidri domÄt. Skaidra domÄÅ”ana ir ļoti svarÄ«ga un diezgan sarežģīta, tÄpÄc mums ir vajadzÄ«ga palÄ«dzÄ«ba. KÄdÄ valodÄ jÄraksta specifikÄcijas? KopumÄ programmÄtÄjiem tas vienmÄr ir pirmais jautÄjums: kÄdÄ valodÄ mÄs rakstÄ«sim? Nav vienas pareizas atbildes: mÅ«su risinÄmÄs problÄmas ir pÄrÄk dažÄdas. Dažiem cilvÄkiem TLA+ ir manis izstrÄdÄta specifikÄcijas valoda. Citiem ÄrtÄk izmantot Ä·Ä«nieÅ”u valodu. Tas viss ir atkarÄ«gs no situÄcijas.
SvarÄ«gÄks jautÄjums ir: kÄ mÄs varam panÄkt skaidrÄku domÄÅ”anu? Atbilde: Mums jÄdomÄ kÄ zinÄtniekiem. Å is ir domÄÅ”anas veids, kas ir labi strÄdÄjis pÄdÄjos 500 gadus. ZinÄtnÄ mÄs veidojam matemÄtiskos realitÄtes modeļus. Astronomija, iespÄjams, bija pirmÄ zinÄtne Ŕī vÄrda tieÅ”Ä nozÄ«mÄ. AstronomijÄ izmantotajÄ matemÄtiskajÄ modelÄ« debess Ä·ermeÅi parÄdÄs kÄ punkti ar masu, stÄvokli un impulsu, lai gan patiesÄ«bÄ tie ir ÄrkÄrtÄ«gi sarežģīti objekti ar kalniem un okeÄniem, bÄgumiem un bÄgumiem. Å is modelis, tÄpat kÄ jebkurÅ” cits, tika izveidots noteiktu problÄmu risinÄÅ”anai. Tas ir lieliski piemÄrots, lai noteiktu, kur vÄrst teleskopu, ja vÄlaties atrast planÄtu. Bet, ja vÄlaties paredzÄt laikapstÄkļus uz Ŕīs planÄtas, Å”is modelis nedarbosies.
MatemÄtika ļauj noteikt modeļa Ä«paŔības. Un zinÄtne parÄda, kÄ Å”Ä«s Ä«paŔības ir saistÄ«tas ar realitÄti. ParunÄsim par mÅ«su zinÄtni, datorzinÄtnÄm. RealitÄte, ar kuru mÄs strÄdÄjam, ir dažÄda veida skaitļoÅ”anas sistÄmas: procesori, spÄļu konsoles, datori, kuros darbojas programmas, un tÄ tÄlÄk. Es runÄÅ”u par programmas izpildi datorÄ, bet kopumÄ visi Å”ie secinÄjumi attiecas uz jebkuru skaitļoÅ”anas sistÄmu. MÅ«su zinÄtnÄ mÄs izmantojam daudz dažÄdu modeļu: TjÅ«ringa maŔīnu, daļÄji sakÄrtotus notikumu kopumus un daudzus citus.
Kas ir programma? Å is ir jebkurÅ” kods, ko var apsvÄrt atseviŔķi. PieÅemsim, ka mums ir jÄraksta pÄrlÅ«kprogramma. MÄs veicam trÄ«s uzdevumus: noformÄjam lietotÄja prezentÄciju par programmu, pÄc tam uzrakstÄm programmas augsta lÄ«meÅa diagrammu un visbeidzot uzrakstÄm kodu. Rakstot kodu, mÄs saprotam, ka mums ir jÄraksta teksta formatÄtÄjs. Å eit atkal jÄatrisina trÄ«s problÄmas: jÄnosaka, kÄdu tekstu Å”is rÄ«ks atgriezÄ«s; izvÄlieties formatÄÅ”anas algoritmu; rakstÄ«t kodu. Å im uzdevumam ir savs apakÅ”uzdevums: pareizi ievietot defises vÄrdos. ArÄ« Å”o apakÅ”uzdevumu risinÄm trÄ«s soļos ā kÄ redzam, tie atkÄrtojas daudzos lÄ«meÅos.
SÄ«kÄk apskatÄ«sim pirmo soli: kÄdu problÄmu programma atrisina. Å eit mÄs visbiežÄk modelÄjam programmu kÄ funkciju, kas Åem zinÄmu ievadi un dod kÄdu izvadi. MatemÄtikÄ funkciju parasti raksturo kÄ sakÄrtotu pÄru kopu. PiemÄram, naturÄlu skaitļu kvadrÄtoÅ”anas funkcija ir aprakstÄ«ta kÄ kopa {<0,0>, <1,1>, <2,4>, <3,9>, ā¦}. Å Ädas funkcijas definÄ«cijas domÄns ir katra pÄra pirmo elementu kopa, tas ir, naturÄlie skaitļi. Lai definÄtu funkciju, mums jÄnorÄda tÄs domÄns un formula.
Bet funkcijas matemÄtikÄ nav tÄdas paÅ”as kÄ funkcijas programmÄÅ”anas valodÄs. MatemÄtika ir daudz vienkÄrÅ”Äka. TÄ kÄ man nav laika sarežģītiem piemÄriem, aplÅ«kosim vienkÄrÅ”u: funkciju C vai statisku metodi Java, kas atgriež lielÄko kopÄjo divu veselu skaitļu dalÄ«tÄju. Å Ä«s metodes specifikÄcijÄ rakstÄ«sim: aprÄÄ·ina GCD(M,N) par argumentiem M Šø NKur GCD(M,N) - funkcija, kuras domÄns ir veselu skaitļu pÄru kopa, un atgriežamÄ vÄrtÄ«ba ir lielÄkais veselais skaitlis, kas dalÄ«ts ar M Šø N. KÄ realitÄte atŔķiras ar Å”o modeli? Modelis darbojas ar veseliem skaitļiem, un C vai Java mums ir 32 biti int. Å is modelis ļauj mums izlemt, vai algoritms ir pareizs GCD, taÄu tas nenovÄrsÄ«s pÄrpildes kļūdas. Tam bÅ«tu nepiecieÅ”ams sarežģītÄks modelis, kuram nav laika.
ParunÄsim par funkcijas kÄ modeļa ierobežojumiem. Dažas programmas (piemÄram, operÄtÄjsistÄmas) ne tikai atgriež noteiktu vÄrtÄ«bu noteiktiem argumentiem; tÄs var darboties nepÄrtraukti. TurklÄt funkcija kÄ modelis ir slikti piemÄrota otrajam solim: problÄmas risinÄÅ”anas plÄnoÅ”anai. ÄtrÄ kÄrtoÅ”ana un burbuļu kÄrtoÅ”ana aprÄÄ·ina vienu un to paÅ”u funkciju, taÄu tie ir pilnÄ«gi atŔķirÄ«gi algoritmi. TÄpÄc, lai aprakstÄ«tu veidu, kÄ sasniegt programmas mÄrÄ·i, es izmantoju citu modeli, sauksim to par standarta uzvedÄ«bas modeli. Programma tajÄ tiek attÄlota kÄ visu derÄ«go uzvedÄ«bu kopums, no kuriem katrs, savukÄrt, ir stÄvokļu secÄ«ba, un stÄvoklis ir vÄrtÄ«bu pieŔķirÅ”ana mainÄ«gajiem.
ApskatÄ«sim, kÄ izskatÄ«sies EiklÄ«da algoritma otrais solis. Mums ir jÄaprÄÄ·ina GCD(M, N). MÄs inicializÄjam M kÄ xUn N kÄ y, pÄc tam atkÄrtoti atÅemiet mazÄko no Å”iem mainÄ«gajiem lielumiem, lÄ«dz tie ir vienÄdi. PiemÄram, ja M = 12Un N = 18, mÄs varam aprakstÄ«t Å”Ädu uzvedÄ«bu:
[x = 12, y = 18] ā [x = 12, y = 6] ā [x = 6, y = 6]
Un ja M = 0 Šø N = 0? Nulle dalÄs ar visiem skaitļiem, tÄpÄc Å”ajÄ gadÄ«jumÄ nav lielÄkÄ dalÄ«tÄja. Å ajÄ situÄcijÄ mums ir jÄatgriežas pie pirmÄ soļa un jÄjautÄ: vai mums tieÅ”Äm ir jÄaprÄÄ·ina GCD nepozitÄ«viem skaitļiem? Ja tas nav nepiecieÅ”ams, jums vienkÄrÅ”i jÄmaina specifikÄcija.
Å eit ir vietÄ Ä«sa atkÄpe par produktivitÄti. To bieži mÄra dienÄ uzrakstÄ«to koda rindiÅu skaitÄ. Bet jÅ«su darbs ir daudz noderÄ«gÄks, ja atbrÄ«vojaties no noteikta rindu skaita, jo jums ir mazÄk vietas kļūdÄm. Un vienkÄrÅ”Äkais veids, kÄ atbrÄ«voties no koda, ir pirmais solis. IespÄjams, ka jums vienkÄrÅ”i nav vajadzÄ«gi visi zvani un svilpes, ko mÄÄ£inÄt Ä«stenot. ÄtrÄkais veids, kÄ vienkÄrÅ”ot programmu un ietaupÄ«t laiku, ir nedarÄ«t lietas, kuras nevajadzÄtu darÄ«t. Otrajam solim ir otrs lielÄkais laika taupÄ«Å”anas potenciÄls. Ja mÄra produktivitÄti uzrakstÄ«to rindiÅu izteiksmÄ, tad domas par to, kÄ izpildÄ«t uzdevumu, liks jums mazÄk produktÄ«vs, jo jÅ«s varat atrisinÄt to paÅ”u problÄmu ar mazÄku kodu. Å eit nevaru sniegt precÄ«zu statistiku, jo man nav iespÄjas saskaitÄ«t rindiÅu skaitu, kuras neuzrakstÄ«ju specifikÄcijas, tas ir, pirmajam un otrajam solim, pavadÄ«tÄ laika dÄļ. Un arÄ« Å”eit nevar veikt eksperimentu, jo eksperimentÄ mums nav tiesÄ«bu veikt pirmo soli, uzdevums tiek noteikts iepriekÅ”.
NeformÄlajÄs specifikÄcijÄs ir viegli nepamanÄ«t daudzas grÅ«tÄ«bas. Stingru funkciju specifikÄciju rakstÄ«Å”anÄ nav nekÄ sarežģīta; es to neapspriedÄ«Å”u. TÄ vietÄ mÄs runÄsim par stingru standarta uzvedÄ«bas specifikÄciju rakstÄ«Å”anu. PastÄv teorÄma, kas nosaka, ka jebkuru darbÄ«bu kopumu var aprakstÄ«t, izmantojot droŔības rekvizÄ«tu (droŔība) un izdzÄ«voÅ”anas Ä«paŔības (dzÄ«vÄ«gums). DroŔība nozÄ«mÄ, ka nekas slikts nenotiks, programma nesniegs nepareizu atbildi. IzdzÄ«voÅ”ana nozÄ«mÄ, ka agrÄk vai vÄlÄk notiks kaut kas labs, t.i., programma agrÄk vai vÄlÄk sniegs pareizo atbildi. Parasti svarÄ«gÄks rÄdÄ«tÄjs ir droŔība, Å”eit visbiežÄk rodas kļūdas. TÄpÄc, lai ietaupÄ«tu laiku, es nerunÄÅ”u par izdzÄ«voÅ”anu, lai gan tas, protams, arÄ« ir svarÄ«gs.
MÄs panÄkam droŔību, vispirms norÄdot iespÄjamo sÄkotnÄjo stÄvokļu kopu. Un, otrkÄrt, attiecÄ«bas ar visiem iespÄjamiem nÄkamajiem stÄvokļiem katram Å”tatam. UzvedÄ«simies kÄ zinÄtnieki un definÄsim stÄvokļus matemÄtiski. SÄkotnÄjo stÄvokļu kopu apraksta ar formulu, piemÄram, EiklÄ«da algoritma gadÄ«jumÄ: (x = M) ā§ (y = N). Par noteiktÄm vÄrtÄ«bÄm M Šø N ir tikai viens sÄkuma stÄvoklis. AttiecÄ«bas ar nÄkamo stÄvokli apraksta ar formulu, kurÄ nÄkamÄ stÄvokļa mainÄ«gie tiek ierakstÄ«ti ar pirmskaitli, bet paÅ”reizÄjÄ stÄvokļa mainÄ«gie bez pirmskaitļa. EiklÄ«da algoritma gadÄ«jumÄ mÄs nodarbosimies ar divu formulu disjunkciju, no kurÄm vienÄ x ir lielÄkÄ vÄrtÄ«ba, bet otrajÄ - y:
PirmajÄ gadÄ«jumÄ jaunÄ y vÄrtÄ«ba ir vienÄda ar iepriekÅ”Äjo y vÄrtÄ«bu, un mÄs iegÅ«stam jauno x vÄrtÄ«bu, atÅemot mazÄko mainÄ«go no lielÄkÄ. OtrajÄ gadÄ«jumÄ mÄs rÄ«kojamies pretÄji.
AtgriezÄ«simies pie EiklÄ«da algoritma. PieÅemsim vÄlreiz, ka M = 12, N = 18. Tas definÄ vienu sÄkotnÄjo stÄvokli, (x = 12) ā§ (y = 18). PÄc tam mÄs pievienojam Ŕīs vÄrtÄ«bas iepriekÅ” minÄtajÄ formulÄ un iegÅ«stam:
Å eit ir vienÄ«gais iespÄjamais risinÄjums: x' = 18 - 12 ā§ y' = 12, un mÄs iegÅ«stam uzvedÄ«bu: [x = 12, y = 18]. TÄdÄ paÅ”Ä veidÄ mÄs varam aprakstÄ«t visus mÅ«su uzvedÄ«bas stÄvokļus: [x = 12, y = 18] ā [x = 12, y = 6] ā [x = 6, y = 6].
PÄdÄjÄ stÄvoklÄ« [x = 6, y = 6] abas izteiksmes daļas bÅ«s nepatiesas, tÄpÄc tai nav nÄkamÄ stÄvokļa. TÄtad, mums ir pilnÄ«ga otrÄ posma specifikÄcija - kÄ mÄs redzam, tÄ ir diezgan parasta matemÄtika, piemÄram, inženieru un zinÄtnieku, un nav dÄ«vaina, piemÄram, datorzinÄtnÄs.
Å Ä«s divas formulas var apvienot vienÄ temporÄlÄs loÄ£ikas formulÄ. Tas ir eleganti un viegli izskaidrojams, bet tagad tam nav laika. LaicÄ«gÄ loÄ£ika mums var bÅ«t nepiecieÅ”ama tikai dzÄ«vÄ«guma Ä«paŔībai, droŔībai tÄ nav vajadzÄ«ga. Man nepatÄ«k temporÄlÄ loÄ£ika kÄ tÄda, tÄ nav gluži parasta matemÄtika, bet dzÄ«vÄ«guma gadÄ«jumÄ tas ir nepiecieÅ”ams ļaunums.
EiklÄ«da algoritmÄ katrai vÄrtÄ«bai x Šø y ir unikÄlas vÄrtÄ«bas x' Šø y', kas padara saistÄ«bu ar nÄkamo stÄvokli patiesu. Citiem vÄrdiem sakot, EiklÄ«da algoritms ir deterministisks. Lai modelÄtu nedeterministisku algoritmu, paÅ”reizÄjam stÄvoklim ir jÄbÅ«t vairÄkiem iespÄjamiem nÄkotnes stÄvokļiem, un katrai neapstrÄdÄtÄ mainÄ«gÄ vÄrtÄ«bai ir jÄbÅ«t vairÄkÄm primÄrÄ mainÄ«gÄ vÄrtÄ«bÄm, lai attiecÄ«bas ar nÄkamo stÄvokli bÅ«tu patiesas. Tas nav grÅ«ti izdarÄms, bet es tagad nesniegÅ”u piemÄrus.
Lai izveidotu darba rÄ«ku, nepiecieÅ”ama formÄlÄ matemÄtika. KÄ specifikÄciju padarÄ«t formÄlu? Lai to izdarÄ«tu, mums bÅ«s nepiecieÅ”ama formÄla valoda, piem. . EiklÄ«da algoritma specifikÄcija Å”ajÄ valodÄ izskatÄ«sies Å”Ädi:
VienÄdÄ«bas zÄ«mes simbols ar trÄ«sstÅ«ri nozÄ«mÄ, ka vÄrtÄ«ba pa kreisi no zÄ«mes tiek noteikta kÄ vienÄda ar vÄrtÄ«bu pa labi no zÄ«mes. BÅ«tÄ«bÄ specifikÄcija ir definÄ«cija, mÅ«su gadÄ«jumÄ divas definÄ«cijas. TLA+ specifikÄcijai ir jÄpievieno deklarÄcijas un zinÄma sintakse, kÄ parÄdÄ«ts augstÄk esoÅ”ajÄ slaidÄ. ASCII formÄtÄ tas izskatÄ«tos Å”Ädi:
KÄ redzat, nekas sarežģīts. TLA+ specifikÄciju var pÄrbaudÄ«t, t.i., mazÄ modelÄ« ir iespÄjams apiet visas iespÄjamÄs darbÄ«bas. MÅ«su gadÄ«jumÄ Å”is modelis bÅ«s noteiktas vÄrtÄ«bas M Šø N. Å Ä« ir ļoti efektÄ«va un vienkÄrÅ”a verifikÄcijas metode, kas ir pilnÄ«bÄ automÄtiska. TurklÄt ir iespÄjams uzrakstÄ«t formÄlus patiesÄ«bas pierÄdÄ«jumus un pÄrbaudÄ«t tos mehÄniski, taÄu tas aizÅem daudz laika, tÄpÄc gandrÄ«z neviens to nedara.
TLA+ galvenais trÅ«kums ir tas, ka tÄ ir matemÄtika, un programmÄtÄji un datorzinÄtnieki baidÄs no matemÄtikas. No pirmÄ acu uzmetiena tas izklausÄs kÄ joks, bet diemžÄl es to saku ļoti nopietni. Mans kolÄÄ£is tikko stÄstÄ«ja, kÄ viÅÅ” mÄÄ£inÄja izskaidrot TLA+ vairÄkiem izstrÄdÄtÄjiem. TiklÄ«dz formulas parÄdÄ«jÄs ekrÄnÄ, viÅu acis uzreiz kļuva stiklveida. TÄtad, ja TLA+ ir biedÄjoÅ”s, varat to izmantot , ir sava veida rotaļlietu programmÄÅ”anas valoda. Izteiksme programmÄ PlusCal var bÅ«t jebkura TLA+ izteiksme, tas ir, bÅ«tÄ«bÄ jebkura matemÄtiska izteiksme. TurklÄt PlusCal ir sintakse nedeterministiskiem algoritmiem. TÄ kÄ PlusCal var rakstÄ«t jebkuru TLA+ izteiksmi, tÄ ir ievÄrojami izteiksmÄ«gÄka nekÄ jebkura reÄla programmÄÅ”anas valoda. PÄc tam PlusCal ir apkopots viegli lasÄmÄ TLA+ specifikÄcijÄ. Tas, protams, nenozÄ«mÄ, ka sarežģītÄ PlusCal specifikÄcija TLA+ pÄrtaps par vienkÄrÅ”u ā tikai tÄpÄc, ka atbilstÄ«ba starp tÄm ir acÄ«mredzama, nekÄda papildu sarežģītÄ«ba neparÄdÄ«sies. Visbeidzot, Å”o specifikÄciju var pÄrbaudÄ«t, izmantojot TLA+ rÄ«kus. KopumÄ PlusCal var palÄ«dzÄt pÄrvarÄt matemÄtikas fobiju; to ir viegli saprast pat programmÄtÄjiem un datorzinÄtniekiem. Es kÄdu laiku (apmÄram 10 gadus) publicÄju tajÄ algoritmus.
VarbÅ«t kÄds iebildÄ«s, ka TLA+ un PlusCal ir matemÄtika un matemÄtika darbojas tikai ar izdomÄtiem piemÄriem. PraksÄ jums ir nepiecieÅ”ama Ä«sta valoda ar veidiem, procedÅ«rÄm, objektiem utt. Tas ir nepareizi. LÅ«k, ko raksta Kriss Å Å«kombs, kurÅ” strÄdÄja Amazon: āMÄs esam izmantojuÅ”i TLA+ desmit lielos projektos, un katrÄ gadÄ«jumÄ tÄ izmantoÅ”ana bÅ«tiski ietekmÄja attÄ«stÄ«bu, jo mÄs varÄjÄm noÄ·ert bÄ«stamas kļūdas, pirms tÄs nonÄca ražoÅ”anÄ, un tÄpÄc, ka tas sniedza mums ieskatu un pÄrliecÄ«bu, kas bija nepiecieÅ”ama, lai kļūtu agresÄ«vs. veiktspÄjas optimizÄcija, neietekmÄjot programmas patiesumu". Bieži var dzirdÄt, ka, izmantojot formÄlas metodes, mÄs iegÅ«stam neefektÄ«vu kodu ā praksÄ viss ir tieÅ”i otrÄdi. TurklÄt pastÄv uzskats, ka vadÄ«tÄjus nevar pÄrliecinÄt par formÄlu metožu nepiecieÅ”amÄ«bu, pat ja programmÄtÄji ir pÄrliecinÄti par to lietderÄ«bu. Un Å Å«kombs raksta: āVadÄ«tÄji tagad visos iespÄjamos veidos cenÅ”as rakstÄ«t specifikÄcijas TLA+ un Ä«paÅ”i atvÄl tam laiku.ā. TÄtad, kad vadÄ«tÄji redz, ka TLA+ darbojas, viÅi to pieÅem. Kriss Å Å«kombs to rakstÄ«ja apmÄram pirms seÅ”iem mÄneÅ”iem (2014. gada oktobrÄ«), bet tagad, cik man zinÄms, TLA+ tiek izmantots 14 projektos, nevis 10. VÄl viens piemÄrs attiecas uz XBox 360 dizainu. Pie ÄÄrlza Tekera ieradÄs praktikants un uzrakstÄ«ja specifikÄciju atmiÅas sistÄmai. Pateicoties Å”ai specifikÄcijai, tika atrasta kļūda, kas citÄdi netiktu atklÄta un izraisÄ«tu katra XBox 360 avÄriju pÄc Äetru stundu lietoÅ”anas. IBM inženieri apstiprinÄja, ka viÅu testi nebÅ«tu atklÄjuÅ”i Å”o kļūdu.
VairÄk par TLA+ var lasÄ«t internetÄ, bet tagad parunÄsim par neformÄlajÄm specifikÄcijÄm. Mums reti ir jÄraksta programmas, kas aprÄÄ·ina vismazÄko dalÄ«tÄju un tamlÄ«dzÄ«gi. Daudz biežÄk mÄs rakstÄm tÄdas programmas kÄ diezgan printera rÄ«ks, ko rakstÄ«ju TLA+. PÄc vienkÄrÅ”ÄkÄs apstrÄdes TLA+ kods izskatÄ«tos Å”Ädi:
TaÄu iepriekÅ” minÄtajÄ piemÄrÄ lietotÄjs, visticamÄk, vÄlÄjÄs, lai savienojums un vienÄdÄ«bas zÄ«mes tiktu lÄ«dzinÄti. TÄtad pareizais formatÄjums izskatÄ«tos vairÄk Å”Ädi:
Apsveriet citu piemÄru:
Å eit, gluži pretÄji, vienÄdÄ«bas zÄ«mju sakÄrtoÅ”ana, saskaitÄ«Å”ana un reizinÄÅ”ana avotÄ bija nejauÅ”a, tÄpÄc pietiek ar vienkÄrÅ”Äko apstrÄdi. KopumÄ pareizam formatÄjumam nav precÄ«zas matemÄtiskas definÄ«cijas, jo āpareiziā Å”ajÄ gadÄ«jumÄ nozÄ«mÄ āko vÄlas lietotÄjsā, un to nevar noteikt matemÄtiski.
Å Ä·iet, ja mums nav patiesÄ«bas definÄ«cijas, tad specifikÄcija ir bezjÄdzÄ«ga. Bet tÄ nav taisnÄ«ba. Tas, ka mÄs nezinÄm, kas programmai ir jÄdara, nenozÄ«mÄ, ka mums nav jÄdomÄ par to, kÄ tai bÅ«tu jÄdarbojas ā gluži pretÄji, mums tai ir jÄvelta vÄl vairÄk pūļu. ÄŖpaÅ”i svarÄ«ga Å”eit ir specifikÄcija. Nav iespÄjams noteikt optimÄlo programmu strukturÄtai drukÄÅ”anai, taÄu tas nenozÄ«mÄ, ka mums tas vispÄr nebÅ«tu jÄuzÅemas, un koda rakstÄ«Å”ana kÄ apziÅas plÅ«sma tÄ nav. Es beidzot uzrakstÄ«ju seÅ”u noteikumu specifikÄciju ar definÄ«cijÄm komentÄru veidÄ Java failÄ. Å eit ir piemÄrs vienam no noteikumiem: a left-comment token is LeftComment aligned with its covering token. Å is noteikums ir uzrakstÄ«ts, teiksim, matemÄtiskÄ angļu valodÄ: LeftComment aligned, left-comment Šø covering token ā termini ar definÄ«cijÄm. MatemÄtiÄ·i apraksta matemÄtiku Å”Ädi: viÅi raksta terminu definÄ«cijas un, pamatojoties uz tiem, veido noteikumus. Å Ä«s specifikÄcijas priekÅ”rocÄ«ba ir tÄda, ka seÅ”us noteikumus ir daudz vieglÄk saprast un atkļūdot nekÄ 850 koda rindiÅas. Man jÄsaka, ka Å”o noteikumu rakstÄ«Å”ana nebija vienkÄrÅ”a, to atkļūdoÅ”ana prasÄ«ja diezgan daudz laika. Es uzrakstÄ«ju kodu tieÅ”i Å”im nolÅ«kam, kas man norÄdÄ«ja, kurÅ” noteikums tika izmantots. TÄ kÄ es pÄrbaudÄ«ju Å”os seÅ”us noteikumus ar dažiem piemÄriem, man nebija jÄatkļūdo 850 koda rindiÅas, un kļūdas bija diezgan viegli atrast. Java tam ir lieliski rÄ«ki. Ja es bÅ«tu tikko uzrakstÄ«jis kodu, tas bÅ«tu prasÄ«jis daudz ilgÄku laiku un formatÄjums bÅ«tu sliktÄks.
KÄpÄc nevarÄja izmantot formÄlu specifikÄciju? No vienas puses, pareiza izpilde Å”eit nav pÄrÄk svarÄ«ga. StrukturÄta izdruka noteikti dažiem neapmierinÄs, tÄpÄc man nebija jÄpanÄk, lai tÄ darbotos pareizi visÄs neparastajÄs situÄcijÄs. VÄl svarÄ«gÄk ir tas, ka man nebija atbilstoÅ”u instrumentu. TLA+ modeļu pÄrbaudÄ«tÄjs Å”eit ir bezjÄdzÄ«gs, tÄpÄc man bÅ«tu jÄraksta piemÄri ar roku.
Dotajai specifikÄcijai ir iezÄ«mes, kas ir kopÄ«gas visÄm specifikÄcijÄm. Tas ir augstÄks lÄ«menis nekÄ kods. To var ieviest jebkurÄ valodÄ. Nav rÄ«ku vai metožu tÄ rakstÄ«Å”anai. Neviens programmÄÅ”anas kurss nepalÄ«dzÄs uzrakstÄ«t Å”o specifikÄciju. Un nav rÄ«ku, kas varÄtu padarÄ«t Å”o specifikÄciju nevajadzÄ«gu, ja vien jÅ«s, protams, nerakstÄt valodu, kas ir Ä«paÅ”i paredzÄta strukturÄtu izdruku programmu rakstÄ«Å”anai TLA+. Visbeidzot, Å”ajÄ specifikÄcijÄ nekas nav teikts par to, kÄ tieÅ”i mÄs rakstÄ«sim kodu, tajÄ ir tikai norÄdÄ«ts, ko kods dara. MÄs rakstÄm specifikÄciju, lai palÄ«dzÄtu mums pÄrdomÄt problÄmu, pirms sÄkam domÄt par kodu.
Bet Å”ai specifikÄcijai ir arÄ« pazÄ«mes, kas to atŔķir no citÄm specifikÄcijÄm. 95% citu specifikÄciju ir daudz Ä«sÄkas un vienkÄrÅ”Äkas:
TurklÄt Ŕī specifikÄcija ir noteikumu kopums. Tas parasti liecina par sliktu specifikÄciju. Izprast noteikumu kopuma sekas ir diezgan grÅ«ti, tÄpÄc man bija jÄpavada daudz laika, lai tos atkļūdotu. TomÄr Å”ajÄ gadÄ«jumÄ es nevarÄju atrast labÄku veidu.
Ir vÄrts pateikt dažus vÄrdus par programmÄm, kas darbojas nepÄrtraukti. Parasti tÄs darbojas paralÄli, piemÄram, operÄtÄjsistÄmas vai sadalÄ«tas sistÄmas. Ä»oti maz cilvÄku var tos saprast savÄ prÄtÄ vai uz papÄ«ra, un es neesmu viens no tiem, lai gan kÄdreiz es to varÄju. TÄpÄc mums ir nepiecieÅ”ami rÄ«ki, kas pÄrbaudÄ«s mÅ«su darbu - piemÄram, TLA+ vai PlusCal.
KÄpÄc man bija jÄraksta specifikÄcija, ja es jau zinÄju, kas kodam jÄdara? PatiesÄ«bÄ es tikai domÄju, ka es to zinu. TurklÄt, ja ir ieviesta specifikÄcija, ÄrÄjam vairs nav jÄiedziļinÄs kodÄ, lai saprastu, ko tieÅ”i tas dara. Man ir noteikums: vispÄrÄjiem noteikumiem nevajadzÄtu bÅ«t. Protams, Å”im noteikumam ir izÅÄmums, tas ir vienÄ«gais vispÄrÄ«gais noteikums, ko es ievÄroju: koda darbÄ«bas specifikÄcijai ir jÄpasaka cilvÄkiem viss, kas viÅiem jÄzina, lietojot Å”o kodu.
Kas tad Ä«sti programmÄtÄjiem jÄzina par domÄÅ”anu? SÄkumÄ tas pats, kas visiem: ja tu neraksti, tad tev tikai Ŕķiet, ka tu domÄ. TurklÄt jums ir jÄdomÄ pirms kodÄÅ”anas, kas nozÄ«mÄ, ka pirms kodÄÅ”anas jums ir jÄraksta. SpecifikÄcijas ir tas, ko mÄs rakstÄm pirms kodÄÅ”anas. SpecifikÄcija ir nepiecieÅ”ama jebkuram kodam, ko var izmantot vai mainÄ«t ikviens. Un Å”is ākÄdsā var izrÄdÄ«ties koda autors mÄnesi pÄc tÄ uzrakstÄ«Å”anas. SpecifikÄcija ir nepiecieÅ”ama lielÄm programmÄm un sistÄmÄm, klasÄm, metodÄm un dažreiz pat vienas metodes sarežģītÄm sadaļÄm. Kas tieÅ”i bÅ«tu jÄraksta par kodu? Jums jÄapraksta, ko tas dara, tas ir, kaut kas var bÅ«t noderÄ«gs ikvienam, kas izmanto Å”o kodu. Dažreiz var bÅ«t nepiecieÅ”ams arÄ« norÄdÄ«t, kÄ tieÅ”i kods sasniedz savu mÄrÄ·i. Ja mÄs Å”o metodi izgÄjÄm algoritmu kursÄ, tad to saucam par algoritmu. Ja tas ir kaut kas specializÄtÄks un jauns, tad mÄs to saucam par augsta lÄ«meÅa dizainu. Å eit nav formÄlas atŔķirÄ«bas: abi ir abstrakti programmas modeļi.
KÄ tieÅ”i jums vajadzÄtu rakstÄ«t koda specifikÄciju? Galvenais: tam jÄbÅ«t vienu lÄ«meni augstÄkam par paÅ”u kodu. Tam jÄapraksta stÄvokļi un uzvedÄ«ba. Tam jÄbÅ«t tik stingrai, cik to prasa uzdevums. Ja rakstÄt specifikÄciju, kÄ Ä«stenot uzdevumu, tad to var rakstÄ«t pseidokodÄ vai izmantojot PlusCal. Jums jÄiemÄcÄs rakstÄ«t specifikÄcijas, izmantojot formÄlas specifikÄcijas. Tas iegÅ«s nepiecieÅ”amÄs prasmes, kas palÄ«dzÄs arÄ« neformÄlajÄs. KÄ iemÄcÄ«ties rakstÄ«t oficiÄlas specifikÄcijas? Kad iemÄcÄ«jÄmies programmÄt, rakstÄ«jÄm programmas un pÄc tam tÄs atkļūdojÄm. Tas pats Å”eit: jums ir jÄuzraksta specifikÄcija, jÄpÄrbauda tÄ ar modeļa pÄrbaudÄ«tÄju un jÄizlabo kļūdas. TLA+ var nebÅ«t labÄkÄ valoda formÄlai specifikÄcijai, un cita valoda, iespÄjams, bÅ«tu labÄk piemÄrota jÅ«su Ä«paÅ”ajÄm vajadzÄ«bÄm. LieliskÄ TLA+ lieta ir tÄ, ka tÄ lieliski mÄca matemÄtisko domÄÅ”anu.
KÄ saistÄ«t specifikÄciju un kodu? Izmantojot komentÄrus, kas saista matemÄtiskos jÄdzienus un to realizÄciju. Ja strÄdÄjat ar grafikiem, tad programmas lÄ«menÄ« jums bÅ«s mezglu masÄ«vi un saiÅ”u masÄ«vi. TÄtad jums ir jÄuzraksta, kÄ tieÅ”i grafu realizÄ Å”Ä«s programmÄÅ”anas struktÅ«ras.
JÄatzÄ«mÄ, ka nekas no iepriekÅ” minÄtÄ neattiecas uz paÅ”u koda rakstÄ«Å”anas procesu. Rakstot kodu, tas ir, veicot treÅ”o darbÄ«bu, jums ir arÄ« jÄdomÄ un jÄpÄrdomÄ programma. Ja apakÅ”uzdevums izrÄdÄs sarežģīts vai nav acÄ«mredzams, jums ir jÄraksta tÄ specifikÄcija. Bet es Å”eit nerunÄju par paÅ”u kodu. JÅ«s varat izmantot jebkuru programmÄÅ”anas valodu, jebkuru metodiku, tas nav par tiem. TurklÄt nekas no iepriekÅ”minÄtÄ neatbrÄ«vo no nepiecieÅ”amÄ«bas pÄrbaudÄ«t un atkļūdot kodu. Pat ja abstraktais modelis ir uzrakstÄ«ts pareizi, tÄ ievieÅ”anÄ var bÅ«t kļūdas.
SpecifikÄciju rakstÄ«Å”ana ir papildu solis kodÄÅ”anas procesÄ. Pateicoties tam, daudzas kļūdas var pieÄ·ert ar mazÄku piepÅ«li - mÄs to zinÄm no Amazon programmÄtÄju pieredzes. Ar specifikÄcijÄm programmu kvalitÄte kļūst augstÄka. KÄpÄc tad mÄs tik bieži iztiekam bez tiem? Jo rakstÄ«t ir grÅ«ti. Bet rakstÄ«t ir grÅ«ti, jo tam ir jÄdomÄ, un arÄ« domÄt ir grÅ«ti. VienmÄr ir vieglÄk izlikties, ka domÄjat. Å eit var vilkt analoÄ£iju ar skrieÅ”anu ā jo mazÄk skrien, jo lÄnÄk skrien. Jums ir jÄtrenÄ savi muskuļi un jÄvingrinÄs rakstÄ«t. Tas prasa praksi.
SpecifikÄcija var bÅ«t nepareiza. IespÄjams, kaut kur esat pieļÄvis kļūdu, prasÄ«bas ir mainÄ«juÅ”Äs, vai arÄ« ir jÄveic uzlabojumi. JebkurÅ” kods, ko kÄds izmanto, ir jÄmaina, tÄpÄc agri vai vÄlu specifikÄcija vairs nesakritÄ«s ar programmu. IdeÄlÄ gadÄ«jumÄ Å”ajÄ gadÄ«jumÄ jums ir jÄraksta jauna specifikÄcija un pilnÄ«bÄ jÄpÄrraksta kods. MÄs ļoti labi zinÄm, ka neviens to nedara. PraksÄ mÄs labojam kodu un, iespÄjams, atjauninÄm specifikÄciju. Ja agrÄk vai vÄlÄk tas noteikti notiks, tad kÄpÄc vispÄr rakstÄ«t specifikÄcijas? PirmkÄrt, personai, kas rediÄ£Äs jÅ«su kodu, katrs papildu vÄrds specifikÄcijÄ bÅ«s zelta vÄrts, un Ŕī persona, iespÄjams, esat jÅ«s. Es bieži spÄrdos sevi par to, ka rediÄ£Äjot kodu, neesmu pietiekami precÄ«zs. Un es rakstu vairÄk specifikÄcijas nekÄ kodu. TÄpÄc, rediÄ£Äjot kodu, specifikÄcija vienmÄr ir jÄatjaunina. OtrkÄrt, ar katru labojumu kods kļūst sliktÄks, to kļūst grÅ«tÄk lasÄ«t un uzturÄt. Tas ir entropijas pieaugums. Bet, ja nesÄkat ar specifikÄciju, katra jÅ«su rakstÄ«tÄ rindiÅa bÅ«s labojums, un kods bÅ«s apjomÄ«gs un grÅ«ti nolasÄms no paÅ”a sÄkuma.
KÄ teikts , neviena kauja netika uzvarÄta pÄc plÄna, un neviena kauja netika uzvarÄta bez plÄna. Un viÅÅ” kaut ko zinÄja par kaujÄm. PastÄv viedoklis, ka specifikÄciju rakstÄ«Å”ana ir laika izŔķieÅ”ana. Dažreiz tÄ ir taisnÄ«ba, un uzdevums ir tik vienkÄrÅ”s, ka nav jÄgas to pÄrdomÄt. Bet jums vienmÄr jÄatceras, ka tad, kad jums tiek ieteikts nerakstÄ«t specifikÄcijas, tas nozÄ«mÄ, ka jums ir ieteicams nedomÄt. Un jums par to vajadzÄtu padomÄt katru reizi. Uzdevuma pÄrdomÄÅ”ana negarantÄ, ka nepieļausit kļūdas. KÄ zinÄms, neviens nav izgudrojis burvju nÅ«jiÅu, un programmÄÅ”ana ir grÅ«ts uzdevums. Bet, ja jÅ«s nepÄrdomÄjat uzdevumu, jÅ«s noteikti pieļausit kļūdas.
VairÄk par TLA+ un PlusCal varat lasÄ«t speciÄlÄ mÄjaslapÄ, turp var doties no manas mÄjas lapas . Tas man ir viss, paldies par uzmanÄ«bu.
LÅ«dzu, atcerieties, ka Å”is ir tulkojums. Rakstot komentÄrus, atcerieties, ka autors tos nelasÄ«s. Ja ļoti vÄlies patÄrzÄt ar autoru, viÅÅ” bÅ«s Hydra 2019 konferencÄ, kas notiks 11. gada 12.-2019.jÅ«lijÄ SanktpÄterburgÄ. Biļetes var iegÄdÄties .
Avots: www.habr.com