Å is ir tulkojuma raksts . Bet pirms tam neliels 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. Un āneizdodasā ne tik daudz tev, cik viÅam: uz vienas kausa svara ir normÄla alga, uzdevumi un tÄ tÄlÄk, bet uz otras ā nepiecieÅ”amÄ«ba domÄt. DomÄt ir nepatÄ«kami un sÄpÄ«gi. ViÅÅ” Ätri padodas un turpina rakstÄ«t kodu, pilnÄ«gi neieslÄdzot prÄtu. Tu vari iedomÄties, cik daudz spÄku ir jÄtÄrÄ, lai pÄrvarÄtu iemÄcÄ«tÄs bezpalÄ«dzÄ«bas barjeru, un tu vienkÄrÅ”i nedari to. TÄ veidojas zombiji, kurus it kÄ var izÄrstÄt, bet it kÄ neviens ar to nenodarbojas.
Kad es redzÄju, ka (jÄ-jÄ, tas pats cilvÄks no mÄcÄ«bu grÄmatÄm) un taisa nevis ziÅojumu, bet jautÄjumu-atbilžu sesiju, es nedaudz norakstÄ«ju. KatrÄ ziÅÄ, Leslijs ā vispasaules pazÄ«stams zinÄtnieks, pamatu darbu autors izkliedÄtajÄ skaitļoÅ”anÄ, kÄ arÄ« jÅ«s varat viÅu pazÄ«t pÄc burtiem La vÄrdÄ LaTeX ā āLamport TeXā. Otra satraucoÅ”Ä lieta ir viÅa prasÄ«ba: ikvienam, kas ieradÄ«sies, jÄbÅ«t (absolÅ«ti par brÄ«vu) iepriekÅ” noklausÄ«jies pÄris viÅa ziÅojumu, izdomÄjis vismaz vienu jautÄjumu un tikai tad ieradies. NolÄmu paskatÄ«ties, ko Lamports vÄsta ā un tas ir lieliski! Tas ir tieÅ”i tÄ, maÄ£iskÄ saite-tablete zombju ÄrstÄÅ”anai. BrÄ«dinÄÅ”u: tekstÄ varÄtu bÅ«t nopietni saskarsmÄ ar tiem, kas ir par superelastÄ«gÄm metodÄm un pret testÄÅ”anu, ko viÅi ir rakstÄ«juÅ”i.
PÄc habrokata, principÄ, sÄkas seminÄra tulkojums. PatÄ«kamu lasÄ«Å”anu!
Par kuru uzdevumu jÅ«s nolemjat, jums vienmÄr jÄnokÄrto trÄ«s soļi:
- nolÄmt, kÄdu mÄrÄ·i jÅ«s vÄlaties sasniegt;
- izdomÄt, kÄ tieÅ”i jÅ«s sasniegsiet savu mÄrÄ·i;
- nonÄkt pie sava mÄrÄ·a.
Tas attiecas arÄ« uz programmÄÅ”anu. Kad mÄs rakstÄm kodu, mums ir nepiecieÅ”ams:
- nolÄmt, ko tieÅ”i programmai vajadzÄtu darÄ«t;
- noteikt, kÄ tieÅ”i tai vajadzÄtu veikt savu uzdevumu;
- uzrakstīt atbilstoŔo kodu.
PÄdÄjais solis, protams, ir ļoti svarÄ«gs, taÄu Å”odien par to nerunÄÅ”u. TÄ vietÄ apspriedÄ«sim pirmos divus. Tos veic katrs programmÄtÄjs pirms sÄkt darbu. JÅ«s nesÄkat rakstÄ«t, ja neesat izdomÄjis, ko tieÅ”i rakstÄt: pÄrlÅ«kprogrammu vai datu bÄzi. Noteiktai izpratnei par mÄrÄ·i ir jÄbÅ«t obligÄti. Un jums obligÄti jÄizdomÄ, ko tieÅ”i programma darÄ«s, nevis jÄraksta kaut kÄdÄ veidÄ, cerot, ka kods pats par sevi pÄrvÄrtÄ«sies par pÄrlÅ«kprogrammu.
KÄ tieÅ”i notiek Ŕī priekÅ”izpÄte koda izstrÄdei? Cik daudz pūļu mums tam vajadzÄtu tÄrÄt? Viss ir atkarÄ«gs no tÄ, cik sarežģītu problÄmu mÄs risinÄm. PieÅemsim, ka mÄs vÄlamies uzrakstÄ«t izturÄ«gu izkliedÄtu sistÄmu. Å ajÄ gadÄ«jumÄ mums jÄizdomÄ viss kÄrtÄ«gi, pirms sÄžamies pie koda. Bet, ja mums vienkÄrÅ”i jÄpalielina vesela skaitļa mainÄ«gÄ vÄrtÄ«ba par 1? PirmajÄ mirklÄ« Å”eit viss Ŕķiet cita lieta, un nav nepiecieÅ”ams domÄt, taÄu pÄc tam mÄs atceramies, ka var notikt pÄrsniegums. TÄdÄļ pat, lai saprastu, vai problÄma ir vienkÄrÅ”a vai sarežģīta ā vispirms jÄpadomÄ.
Ja iepriekÅ” padomÄjat par iespÄjamiem problÄmas risinÄjumiem, varat izvairÄ«ties no kļūdÄm. Bet tam ir nepiecieÅ”ams, lai jÅ«su domÄÅ”ana bÅ«tu skaidra. Lai to sasniegtu, ir jÄvÄro savas domas. Man ļoti patÄ«k Dika Gindona citÄts: Ā«Kad jÅ«s rakstÄt, daba jums parÄda, cik nekÄrtÄ«ga ir jÅ«su domÄÅ”anaĀ». Ja jÅ«s nerakstÄt, jums tikai liekas, ka domÄjat. Un domas jÄreÄ£istrÄ specifikÄciju formÄ.
SpecifikÄcijas veic daudzas funkcijas, jo Ä«paÅ”i lielos projektos. Bet es runÄÅ”u tikai par vienu no tÄm: tÄs palÄ«dz mums skaidri domÄt. Skaidra domÄÅ”ana ir ļoti svarÄ«ga un diezgan grÅ«ta, tÄpÄc Å”eit mums ir nepiecieÅ”ams jebkÄds atbalsts. KÄdÄ valodÄ mums vajadzÄtu rakstÄ«t specifikÄcijas? Tas vienmÄr ir pirmais jautÄjums programmÄtÄjiem: kÄdÄ valodÄ mÄs rakstÄ«sim. Uz to nav vienas pareizas atbildes: problÄmas, kuras mÄs risinÄm, ir pÄrÄk daudzveidÄ«gas. Dažiem noder TLA+ ā tas ir specifikÄciju valoda, ko es izstrÄdÄju. Citiem ÄrtÄk izmantot Ä·Ä«nieÅ”u valodu. Viss ir atkarÄ«gs no situÄcijas.
Ir svarÄ«gÄks jautÄjums: kÄ panÄkt skaidrÄku domÄÅ”anu? Atbilde: mums jÄdomÄ kÄ zinÄtniekiem. Å Ä« domÄÅ”ana ir izcili sevi pierÄdÄ«jusi pÄdÄjo 500 gadu laikÄ. ZinÄtnÄ mÄs veidojam matemÄtiskÄs realitÄtes modeļus. Astronomija, iespÄjams, bija pirmÄ zinÄtne, kurai Å”is vÄrds patieÅ”Äm atbilst. MatemÄtiskajÄ modelÄ«, ko izmanto astronomijÄ, debess Ä·ermeÅi tiek attÄloti kÄ punkti ar masu, atraÅ”anÄs vietu un impulsu, lai gan realitÄtÄ tie ir ÄrkÄrtÄ«gi sarežģīti objekti ar kalniem un okeÄniem, plÅ«diem un paisumiem. Å is modelis, tÄpat kÄ jebkurÅ” cits, ir izveidots, lai risinÄtu konkrÄtas problÄmas. Tas lieliski piemÄrots, lai noskaidrotu, kur jÄpavÄrÅ” teleskops, ja jÄatrod planÄta. Bet, ja vÄlaties prognozÄt laiku Å”ajÄ planÄtÄ, Å”is modelis nebÅ«s piemÄrots.
MatemÄtika ļauj mums noteikt modeļa Ä«paŔības. Bet zinÄtne parÄda, kÄ Å”Ä«s Ä«paŔības attiecÄs uz realitÄti. ParunÄsim par mÅ«su zinÄtni, datorzinÄtni. RealitÄte, ar kuru mÄs strÄdÄjam, ir dažÄdu veidu aprÄÄ·inu sistÄmas: procesori, spÄļu konsoles, datori, kas izpilda programmas, un tÄ tÄlÄk. Es runÄÅ”u par programmas izpildi datorÄ, bet lielÄkÄ mÄrÄ visi Å”ie secinÄjumi attiecas uz jebkuru aprÄÄ·inu sistÄmu. MÅ«su zinÄtnÄ mÄs izmantojam daudz dažÄdu modeļu: Tjuringa maŔīnu, daļÄji sakÄrtotas notikumu kopas un daudzus citus.
Kas ir programma? TÄ ir jebkÄds kods, ko var apsvÄrt patstÄvÄ«gi. PieÅemam, ka mums jÄuzraksta pÄrlÅ«ks. MÄs veicam trÄ«s uzdevumus: projektÄjam programmas iesniegÅ”anu lietotÄjam, tad rakstÄm augstÄkas pakÄpes programmas shÄmu un, visbeidzot, rakstÄm kodu. Rakstot kodu, mÄs saprotam, ka mums jÄraksta rÄ«ks teksta formatÄÅ”anai. Å eit mums atkal jÄrisina trÄ«s uzdevumi: noteikt, kÄds teksts tiks atgriezts Å”im rÄ«kam; izvÄlÄties algoritmu formatÄÅ”anai; uzrakstÄ«t kodu. Å im uzdevumam ir sava apakÅ”uzdevums: pareizi ievietot defises vÄrdos. Å o apakÅ”uzdevumu arÄ« risinÄm trÄ«s posmos ā kÄ redzam, tie atkÄrtojas daudzos lÄ«meÅos.
ApskatÄ«sim tuvÄk pirmo soli: kÄdu uzdevumu risina programma. Å eit mÄs bieži vien modelÄjam programmu kÄ funkciju, kas saÅem noteiktus ievades datus un dod noteiktus iznÄkuma datus. MatematikÄ funkcija parasti tiek aprakstÄ«ta kÄ sakÄrtots pÄru kopums. PiemÄram, kvadrÄta funkcija dabiskajiem skaitļiem tiek aprakstÄ«ta kÄ kopums {, , , , ...}. Å Ädas funkcijas definÄ«cijas joma ir pirmo elementu kopums katrÄ pÄrÄ«, proti, dabiskie skaitļi. Lai definÄtu funkciju, mums jÄnorÄda tÄs definÄ«cijas joma un formula.
Bet matemÄtikas funkcijas nav tas pats, kas 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: funkcija valodÄ C vai statisks statiskÄ metode Java, kas atgriež divu veselu skaitļu lielÄko kopÄ«go dalÄ«tÄju. Å Ä« metode specifikÄcijÄ mÄs rakstÄ«sim: aprÄÄ·ina GCD(M,N) argumentiem M un N, kur GCD(M,N) ā funkcija, kuras definÄ«cijas joma ir veselu skaitļu pÄru kopums, bet atgrieztÄ vÄrtÄ«ba ir lielÄkais vesels skaitlis, kas dala M un N. KÄ Å”is modelis attiecÄs uz realitÄti? Modelis strÄdÄ ar veseliem skaitļiem, taÄu C vai Java mÄs strÄdÄjam ar 32 bitu int. Å is modelis ļauj mums noskaidrot, vai algoritms ir pareizs GCD, bet tas nepieļaus pÄrsnieguma kļūdas. Tam vajadzÄtu bÅ«t sarežģītÄkam modelim, uz kuru nav laika.
ParunÄsim par funkcijas ierobežojumiem kÄ modeli. Dažas programmu (piemÄram, operÄtÄjsistÄmu) darbÄ«bas nevar samazinÄt lÄ«dz noteiktas vÄrtÄ«bas atgrieÅ”anai konkrÄtiem argumentiem, tÄs var darboties nepÄrtraukti. TurklÄt funkcija kÄ modelis slikti der otrajam solim: uzdevuma risinÄÅ”anas veida plÄnoÅ”anai. ÄtrÄ Å”Ä·iroÅ”ana un burbuļu ŔķiroÅ”ana aprÄÄ·ina to paÅ”u funkciju, bet tie ir pilnÄ«gi atŔķirÄ«gi algoritmi. TÄdÄļ programmas mÄrÄ·a sasniegÅ”anas veida aprakstÄ«Å”anai es izmantoju citu modeli, kuru nosauksim par standarta uzvedÄ«bas modeli. ProgrammÄ tas tiek attÄlots kÄ visu atļauto uzvedÄ«bu kopa, no kurÄm katra, 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 otrais solis Euklida algoritmam. Mums ir jÄsaskaita GCD(M, N). MÄs inicializÄjam M kÄ x, bet N kÄ y, pÄc tam atkÄrtoti atÅemam mazÄko no Ŕīm mainÄ«gajÄm no lielÄkÄ, lÄ«dz tÄs kļūst vienÄdas. PiemÄram, ja M = 12, bet N = 18, mÄs varam aprakstÄ«t sekojoÅ”o uzvedÄ«bu:
[x = 12, y = 18] ā [x = 12, y = 6] ā [x = 6, y = 6]
Bet, ja M = 0 un N = 0? ŠŠ¾Š»Ń Š“ŠµŠ»ŠøŃŃŃ Š½Š° Š²ŃŠµ ŃŠøŃŠ»Š°, ŠæŠ¾ŃŃŠ¾Š¼Ń Š½Š°ŠøŠ±Š¾Š»ŃŃŠµŠ³Š¾ Š“ŠµŠ»ŠøŃŠµŠ»Ń Š² ŃŃŠ¾Š¼ ŃŠ»ŃŃŠ°Šµ Š½ŠµŃ. Š ŃŃŠ¾Š¹ ŃŠøŃŃŠ°ŃŠøŠø Š½Š°Š¼ Š½ŃŠ¶Š½Š¾ Š²ŠµŃŠ½ŃŃŃŃŃ Šŗ ŠæŠµŃŠ²Š¾Š¼Ń ŃŠ°Š³Ń Šø ŃŠæŃŠ¾ŃŠøŃŃ: Š“ŠµŠ¹ŃŃŠ²ŠøŃŠµŠ»ŃŠ½Š¾ Š»Šø Š½Š°Š¼ Š½ŃŠ¶Š½Š¾ Š²ŃŃŠøŃŠ»ŃŃŃ ŠŠŠ Š“Š»Ń Š½ŠµŠæŠ¾Š»Š¾Š¶ŠøŃŠµŠ»ŃŠ½ŃŃ
ŃŠøŃŠµŠ»? ŠŃŠ»Šø Š² ŃŃŠ¾Š¼ Š½ŠµŃ Š½ŠµŠ¾Š±Ń
Š¾Š“ŠøŠ¼Š¾ŃŃŠø, ŃŠ¾ Š½ŃŠ¶Š½Š¾ ŠæŃŠ¾ŃŃŠ¾ ŠøŠ·Š¼ŠµŠ½ŠøŃŃ ŃŠæŠµŃŠøŃŠøŠŗŠ°ŃŠøŃ.
Å eit ir vÄrts nedaudz atkÄpties par produktivitÄti. To bieži mÄra ar dienÄ uzrakstÄ«to rindu skaitu. TomÄr jÅ«su darbs ir ievÄrojami izdevÄ«gÄks, ja esat samazinÄjuÅ”i noteiktu rindu skaitu, jo jums ir mazÄk vietas kļūdÄm. Un no koda ir visvieglÄk atbrÄ«voties tieÅ”i pirmajÄ solÄ«. Ir iespÄjams, ka jums vispÄr nav nepiecieÅ”ami visi tie sarežģījumi, kurus mÄÄ£inÄt Ä«stenot. ÄtrÄkais veids, kÄ vienkÄrÅ”ot programmu un ietaupÄ«t laiku, ir nedarÄ«t lietas, kuras nevajag darÄ«t. Otrais solis ir otrajÄ vietÄ pÄc potenciÄla laika ietaupÄ«Å”anai. Ja jÅ«s mÄrat produktivitÄti ar uzrakstÄ«tajÄm rindÄm, tad uzdevuma izpildes veida pÄrdomÄÅ”ana padara jÅ«s mazÄk produktÄ«vus, jo jÅ«s varat atrisinÄt to paÅ”u uzdevumu ar mazÄku koda apjomu. PrecÄ«zu statistiku Å”eit nevaru sniegt, jo man nav veida saskaitÄ«t to rindu skaitu, kuras neesmu uzrakstÄ«jis, pateicoties tam, ka pavadÄ«ju laiku specifikÄcijai, proti, pirmajiem un otrajiem soļiem. Un Å”eit arÄ« nav iespÄjams veikt eksperimentu, jo eksperimentÄ mums nav atļauts veikt pirmo soli, uzdevums ir noteikts iepriekÅ”.
NeformÄlajÄs specifikÄcijÄs ir viegli neievÄrot daudzas grÅ«tÄ«bas. Nekas sarežģīts nav rakstÄ«t stingras specifikÄcijas funkcijÄm, par to es nerunÄÅ”u. TÄ vietÄ mÄs runÄsim par stingru specifikÄciju rakstÄ«Å”anu standartizÄtÄm uzvedÄ«bas modeļiem. Ir teoria, kas apgalvo, ka jebkura uzvedÄ«bu kopa var tikt aprakstÄ«ta, izmantojot droŔības Ä«paŔību (safety) un dzÄ«votspÄjas Ä«paŔību (liveness). DroŔība nozÄ«mÄ, ka nekas slikts nenotiks, programma nesniegs nepareizu atbildi. Ilgmūžība nozÄ«mÄ, ka agri vai vÄlu notiks kaut kas labs, proti, programma agri vai vÄlu sniegs pareizu atbildi. Parasti droŔība ir svarÄ«gÄks rÄdÄ«tÄjs, kļūdas visbiežÄk rodas tieÅ”i Å”eit. TÄdÄļ laika taupÄ«Å”anas nolÅ«kos es nerunÄÅ”u par ilgmūžību, lai gan tÄ arÄ« ir svarÄ«ga.
MÄs panÄkam droŔību, vispirms nosakot daudz iespÄjamo sÄkotnÄjo stÄvokļu. Un, otrs, attiecÄ«bas ar visiem iespÄjamajiem nÄkamajiem stÄvokļiem katram stÄvoklim. UzvedÄ«simies kÄ zinÄtnieki un matemÄtiski definÄsim stÄvokļus. SÄkotnÄjo stÄvokļu kopums tiek aprakstÄ«ts ar formulu, piemÄram, Eiropas algoritma gadÄ«jumÄ: (x = M) ā§ (y = N). Noteiktiem vÄrtÄ«bÄm M un N pastÄv tikai viens sÄkotnÄjais stÄvoklis. AttiecÄ«bas ar nÄkamo stÄvokli tiek aprakstÄ«tas ar formulu, kurÄ nÄkamÄ stÄvokļa mainÄ«gie tiek rakstÄ«ti ar svÄ«tru, bet paÅ”reizÄjÄ stÄvokļa ā bez svÄ«tras. Eiropas algoritma gadÄ«jumÄ mums bÅ«s jÄtiek galÄ ar divu formulu disjunkciju, kurÄ vienÄ no tÄm x ir augstÄkais vÄrtÄ«ba, bet otrajÄ ā y:
PirmajÄ gadÄ«jumÄ jaunÄ vÄrtÄ«ba y ir vienÄda ar iepriekÅ”Äjo y vÄrtÄ«bu, bet jauno x vÄrtÄ«bu mÄs iegÅ«stam, atÅemot no lielÄkÄs mainÄ«gÄs mazÄko. OtrajÄ gadÄ«jumÄ mÄs rÄ«kojamies pretÄji.
AtgriezÄ«simies pie Eiropas algoritma. PieÅemam, ka M = 12, N = 18. Tas nosaka vienÄ«go sÄkotnÄjo stÄvokli, (x = 12) ā§ (y = 18). Tad mÄs aizvietojam Ŕīs vÄrtÄ«bas iepriekÅ” minÄtajÄ formulÄ un iegÅ«stam:
Å eit ir vienÄ«gÄ iespÄjamÄ atrisinÄjuma: x' = 18 - 12 ā§ y' = 12, un mÄs iegÅ«stam uzvedÄ«bu: [x = 12, y = 18]. TieÅ”i tÄpat mÄs varam aprakstÄ«t visus stÄvokļus mÅ«su uzvedÄ«bÄ: [x = 12, y = 18] ā [x = 12, y = 6] ā [x = 6, y = 6].
PÄdÄjÄ stÄvoklÄ« [x = 6, y = 6] abi izteikuma daļu bÅ«s nepatiesi, lÄ«dz ar to tam nav nÄkamÄ stÄvokļa. TÄtad, mÄs iegÅ«stam pilnu otrÄ soļa specifikÄciju ā kÄ redzam, tÄ ir diezgan parasta matemÄtika, kÄ pie inženieriem un zinÄtniekiem, nevis dÄ«vaina, kÄ datorzinÄtnÄs.
Å os divus formulas var apvienot vienÄ laika loÄ£ikas formulÄ. TÄ ir eleganta, un ir viegli to izskaidrot, taÄu Å”obrÄ«d tam nav laika. Laika loÄ£ika mums var bÅ«t nepiecieÅ”ama tikai dzÄ«votspÄjas Ä«paŔībai, droŔībai tÄ nav vajadzÄ«ga. Laika loÄ£ika kÄ tÄda nepatÄ«k, tÄ nav gluži parasta matemÄtika, bet dzÄ«votspÄjas gadÄ«jumÄ tÄ ir nepiecieÅ”amais ļaunums.
Eiklida algoritmÄ katrai vÄrtÄ«bai x un y ir unikÄlas vÄrtÄ«bas x' un y', kas padara attiecÄ«bu ar nÄkamo stÄvokli patiesu. Citiem vÄrdiem sakot, Eiklida algoritms ir deterministiskais. Lai modelÄtu nedeterministisku algoritmu, ir jÄnodroÅ”ina, ka paÅ”reizÄjam stÄvoklim ir vairÄki iespÄjamie nÄkotnes stÄvokļi, un ka katrai mainÄ«gÄs vÄrtÄ«bai bez svÄ«tras ir vairÄki mainÄ«gÄs vÄrtÄ«bas ar svÄ«tru, kuru attiecÄ«ba ar nÄkamo stÄvokli ir patiesa. To nav grÅ«ti izdarÄ«t, taÄu paÅ”laik piemÄrus sniegt neplÄnoju.
Lai izveidotu strÄdÄjoÅ”u rÄ«ku, nepiecieÅ”ama formÄlÄ matemÄtika. KÄ padarÄ«t specifikÄciju formÄlu? Tam mums bÅ«s nepiecieÅ”ams formÄls valodas, piemÄram, . Eiklida algoritma specifikÄcija Å”ajÄ valodÄ izskatÄ«sies Å”Ädi:
VienÄdÄ«bas zÄ«me ar trÄ«sstÅ«ri nozÄ«mÄ, ka vÄrtÄ«ba pa kreisi no zÄ«mes ir definÄta kÄ vienÄda ar vÄrtÄ«bu pa labi no zÄ«mes. PamatspecifikÄcija ir definÄ«cija, mÅ«su gadÄ«jumÄ divas definÄ«cijas. TLA+ specifikÄcijai nepiecieÅ”ams pievienot deklarÄcijas un kÄdu sintaksi, kÄ norÄdÄ«ts augstÄkajÄ slaidÄ. ASCII tas izskatÄ«sies Å”Ädi:
KÄ redzam, nekÄ sarežģīta. TLA+ specifikÄciju var pÄrbaudÄ«t, t.i., iziet cauri visiem iespÄjamajiem uzvedÄ«bas modeļiem nelielÄ modelÄ«. MÅ«su gadÄ«jumÄ Å”is modelis bÅ«s konkrÄtas vÄrtÄ«bas M un N. Tas ir ļoti efektÄ«vs un vienkÄrÅ”s pÄrbaudes veids, kas pilnÄ«bÄ tiek izpildÄ«ts automÄtiski. TurklÄt var uzrakstÄ«t formÄlus pierÄdÄ«jumus par patiesumu un pÄrbaudÄ«t tos mehÄniski, taÄu tam ir nepiecieÅ”ams daudz laika, tÄpÄc tÄ gandrÄ«z neviens to nedara.
Galvenais TLA+ trÅ«kums ir tas, ka tÄ ir matemÄtika, un programmÄtÄji un datorspeciÄlisti baidÄs no matemÄtikas. PirmajÄ brÄ«dÄ« tas izklausÄs kÄ joks, bet, diemžÄl, es runÄju pavisam nopietni. Mans kolÄÄ£is tikko stÄstÄ«ja, kÄ viÅÅ” mÄÄ£inÄjis izskaidrot TLA+ vairÄkiem izstrÄdÄtÄjiem. TiklÄ«dz uz ekrÄna parÄdÄ«jÄs formulas, viÅiem uzreiz izdarÄ«jÄs stikla acis. TÄpÄc, ja TLA+ biedÄ, var izmantot , tas ir tÄds kÄ rotaļu programmÄÅ”anas valoda. Izteiksme PlusCal var bÅ«t jebkura izteiksme TLA+, tÄtad, bÅ«tÄ«bÄ, jebkura matemÄtiskÄ izteiksme. TurklÄt PlusCal ir sintakse nedeterministiskajiem algoritmiem. Pateicoties tam, ka PlusCal var rakstÄ«t jebkuru TLA+ izteiksmi, tas ir ievÄrojami izteiksmÄ«gÄks par jebkuru reÄlo programmÄÅ”anas valodu. TurklÄt PlusCal tiek kompilÄts saprotamÄ TLA+ specifikÄcijÄ. Tas nenozÄ«mÄ, ka sarežģīta PlusCal specifikÄcija pÄrvÄrtÄ«sies vienkÄrÅ”Ä TLA+ ā vienkÄrÅ”i atbilstÄ«ba starp tÄm ir acÄ«mredzama, papildu sarežģītÄ«ba neradÄ«sies. Visbeidzot, Å”o specifikÄciju varÄs pÄrbaudÄ«t ar TLA+ rÄ«kiem. KopumÄ PlusCal var palÄ«dzÄt pÄrvarÄt matemÄtikas fobiju, to viegli sapratÄ«s pat programmÄtÄji un datorspeciÄlisti. PagÄtnÄ es kÄdu laiku (apmÄram 10 gadus) publicÄju algoritmus uz tÄ.
IespÄjams, kÄds iebildÄ«s, ka TLA+ un PlusCal ir matemÄtika, un matemÄtika darbojas tikai ar izdomÄtiem piemÄriem. PraksÄ tomÄr ir nepiecieÅ”ama reÄla valoda ar tipiem, procedÅ«rÄm, objektiem un tÄ tÄlÄk. Tas nav taisnÄ«ba. Å Ädu komentÄru sniedz Kris NÅ«kombs, kurÅ” strÄdÄjis Amazon: Ā«MÄs izmantojÄm TLA+ desmit lielos projektos, un katrÄ gadÄ«jumÄ tÄ izmantoÅ”ana bÅ«tiski veicinÄja izstrÄdi, jo mÄs spÄjÄm atklÄt bÄ«stamas kļūdas pirms tÄm nonÄkÅ”anu produkcijÄ, un tÄ sniedza mums izpratni un pÄrliecÄ«bu, kas nepiecieÅ”ama agresÄ«vÄm veiktspÄjas optimizÄcijÄm, neietekmÄjot programmas patiesumuĀ». Bieži var dzirdÄt, ka, izmantojot formÄlos metodus, mÄs iegÅ«stam neefektÄ«vu kodu ā tomÄr praksÄ viss ir tieÅ”i otrÄdi. TurklÄt pastÄv uzskats, ka menedžerus nevar pÄrliecinÄt par formÄlo metožu nepiecieÅ”amÄ«bu, pat ja programmÄtÄji tic to lietderÄ«bai. Un NÅ«kombs raksta: Ā«Menedžeri tagad visÄdi mudina rakstÄ«t specifikÄcijas TLA+, un speciÄli tam paredz laikuĀ». TÄdÄļ, kad menedžeri redz, ka TLA+ darbojas, viÅi to entuziastiski pieÅem. Kriss NjÅ«kombs to uzrakstÄ«ja apmÄram pirms seÅ”iem mÄneÅ”iem (2014. gada oktobrÄ«), un, cik man zinÄms, tagad TLA+ tiek izmantots 14 projektos, nevis 10. VÄl viens piemÄrs attiecas uz XBox 360 projektÄÅ”anu. Pie ÄÄrlza Tekeru pienÄca prakÅ”u students un uzrakstÄ«ja specifikÄciju atmiÅu sistÄmai. Pateicoties Å”ai specifikÄcijai, tika atrasts bugs, kuru citÄdi nebÅ«tu pamanÄ«ts, un kura dÄļ katrs XBox 360 uzkristu pÄc Äetru stundu lietoÅ”anas. IBM inženieri apstiprinÄja, ka viÅu testi Å”o bug neatrastu.
VairÄk par TLA+ jÅ«s varat izlasÄ«t internetÄ, bet tagad parunÄsim par neformÄlÄm specifikÄcijÄm. Mums reti nÄkas rakstÄ«t programmas, kas aprÄÄ·ina mazÄko kopÄjo dalÄ«tÄju un tamlÄ«dzÄ«gi. BiežÄk mÄs rakstÄm programmas, piemÄram, strukturÄlÄ izdrukas instrumentu (pretty-printer), kuru es uzrakstÄ«ju TLA+. PÄc vienkÄrÅ”ÄkÄs apstrÄdes kods uz TLA+ izskatÄ«tos Å”Ädi:
Bet dotajÄ piemÄrÄ lietotÄjs, visticamÄk, vÄlÄjÄs, lai konjunkcijas un vienÄdÄ«bas simboli bÅ«tu izkÄrtoti. TÄdÄļ pareizÄ formatÄÅ”ana izskatÄ«tos aptuveni Å”Ädi:
ApskatÄ«sim citu piemÄru:
Å eit, tieÅ”i pretÄji, vienÄdÄ«bas, summÄÅ”anas un reizinÄÅ”anas simbolu izkÄrtojums avotÄ bija nejauÅ”s, tÄdÄļ vienkÄrÅ”ÄkÄs apstrÄdes pilnÄ«gi pietiek. Parasti precÄ«zs matemÄtisks definÄjums pareizai formatÄÅ”anai nepastÄv, jo āpareizsā Å”ajÄ gadÄ«jumÄ nozÄ«mÄ ātÄds, kÄdu vÄlas lietotÄjsā, un to matemÄtiski noteikt nav iespÄjams.
IzskatÄs, ka, ja mums nav patiesÄ«bas definÄ«cijas, tad specifikÄcija ir bezjÄdzÄ«ga. Bet tÄ nav. Ja mÄs nezinÄm, ko tieÅ”i programmai jÄveic, tas nenozÄ«mÄ, ka mums nevajadzÄtu izdomÄt tÄs darbÄ«bu ā tieÅ”i pretÄji, mums uz to jÄvelta vÄl lielÄkas pÅ«les. SpecifikÄcija Å”eit ir Ä«paÅ”i svarÄ«ga. Noteikt optimÄlu programmu strukturÄlajai izdrukai nav iespÄjams, bet tas nenozÄ«mÄ, ka mums nevajadzÄtu to mÄÄ£inÄt realizÄt, un rakstÄ«t kodu kÄ apziÅas plÅ«smu ā tas nav pareizi. Galu galÄ es uzrakstÄ«ju seÅ”u noteikumu specifikÄciju ar definÄ«cijÄm komentÄru formÄ Java failÄ. LÅ«k, viens no noteikumiem piemÄrs: left-comment tokens ir LeftComment, kas saskaÅota ar tÄs pÄrklÄjoÅ”o token.. Å is noteikums ir rakstÄ«ts, teiksim, matemÄtiskÄ angļu valodÄ: LeftComment saskaÅota, left-comment un pÄrklÄjoÅ”ais token ā termini ar definÄ«cijÄm. TÄ ir matemÄtiÄ·u metode matemÄtikas aprakstÄ«Å”anai: viÅi definÄ terminus un balstoties uz tiem ā noteikumus. Å Ädas specifikÄcijas priekÅ”rocÄ«ba ir tÄ, ka saprast un atkļūdot seÅ”us noteikumus ir ievÄrojami vieglÄk, nekÄ 850 koda rindiÅas. JÄteic, rakstÄ«t Å”os noteikumus nebija viegli, samÄrÄ daudz laika tika patÄrÄts to atkļūdoÅ”anai. TieÅ”i Å”im nolÅ«kam es uzrakstÄ«ju kodu, kas ziÅo, kÄds noteikums tiek izmantots. Pateicoties tam, ka es pÄrbaudÄ«ju Å”os seÅ”us noteikumus uz vairÄkiem piemÄriem, man nebija jÄkļūdo 850 koda rindiÅas, un kļūdas izrÄdÄ«jÄs salÄ«dzinoÅ”i viegli atrodamas. Java Å”im nolÅ«kam piedÄvÄ lieliskus rÄ«kus. Ja es vienkÄrÅ”i bÅ«tu uzrakstÄ«jis kodu, tas man prasÄ«tu ievÄrojami vairÄk laika un formatÄjums bÅ«tu daudz sliktÄks.
KÄpÄc nevarÄja izmantot formÄlo specifikÄciju? No vienas puses, pareizÄ«ba Å”eit nav tik bÅ«tiska. StrukturÄlo izdrukÄÅ”anu noteikti kÄds neapmierinÄs, tÄpÄc man nebija jÄdara viss iespÄjams, lai tÄ darbotos visÄs neordinÄrajÄs situÄcijas. VÄl svarÄ«gÄk ir tas, ka man nebija adekvÄtu rÄ«ku. TLA+ modeļu pÄrbaudes rÄ«ks Å”eit ir bezjÄdzÄ«gs, tÄpÄc man bÅ«tu jÄraksta piemÄri manuÄli.
NorÄdÄ«tajai specifikÄcijai ir iezÄ«mes, kas ir kopÄ«gas visÄm specifikÄcijÄm. TÄ ir augstÄka lÄ«meÅa, nekÄ kods. To var Ä«stenot jebkurÄ valodÄ. TÄs izveidei nav noderÄ«gi nekÄdi rÄ«ki vai metodes. Neviens programmÄÅ”anas kurss nepalÄ«dzÄs jums uzrakstÄ«t Å”o specifikÄciju. Un nav neviena rÄ«ka, kas varÄtu padarÄ«t Å”o specifikÄciju nevajadzÄ«gu, ja, protams, jÅ«s nesarakstÄt valodu tieÅ”i struktÅ«ras izdrukas programmu rakstÄ«Å”anai uz TLA+. Visbeidzot, Ŕī specifikÄcija neko nesaka par to, kÄ mÄs rakstÄ«sim kodu, tajÄ tikai norÄdÄ«ts, ko Å”is kods dara. MÄs rakstÄm specifikÄciju, lai palÄ«dzÄtu bÅ«t skaidriem par problÄmu, pirms sÄkam domÄt par kodu.
TomÄr Å”ai specifikÄcijai ir arÄ« Ä«patnÄ«bas, kas to atŔķir no citÄm specifikÄcijÄm. 95% citu specifikÄciju ir ievÄrojami Ä«sÄkas un vienkÄrÅ”Äkas:
TÄlÄk, Å”specifikÄcija ir noteikumu kopums. Parasti tas ir slikta specifikÄcija. Saprast sekas no noteikumu kopuma ir diezgan grÅ«ti, un tieÅ”i tÄpÄc man bija jÄtÄrÄ daudz laika to atkļūdoÅ”anai. TomÄr Å”ajÄ gadÄ«jumÄ man neizdevÄs atrast labÄku veidu.
Ir vÄrts teikt dažus vÄrdus par programmÄm, kas strÄdÄ nepÄrtraukti. Parasti tÄs strÄdÄ vienlaikus, piemÄram, operÄtÄjsistÄmas vai izkliedÄtÄs sistÄmas. Saprast tÄs prÄtÄ vai uz papÄ«ra var ļoti maz cilvÄku, un es nepiederu to skaitam, lai gan kÄdreiz tas man izdevÄs. TÄpÄc ir nepiecieÅ”ami rÄ«ki, kas pÄrbaudÄ«s mÅ«su darbu ā piemÄram, TLA+ vai PlusCal.
KÄpÄc bija jÄraksta specifikÄcija, ja es jau zinÄju, ko tieÅ”i kodam jÄdar? PatiesÄ«bÄ man tikai likÄs, ka es to zinu. TurklÄt, ja ir specifikÄcija, sveÅ”ajam cilvÄkam vairs nav jÄielec kodÄ, lai saprastu, ko tieÅ”i tas dara. Man ir noteikums: nedrÄ«kst bÅ«t nekÄdu kopÄ«gu noteikumu. Å im noteikumam, protams, ir izÅÄmums, tas ir vienÄ«gais kopÄ«gais noteikums, ko es ievÄroju: specifikÄcijai par to, ko dara kods, jÄsniedz cilvÄkiem visa informÄcija, kas viÅiem nepiecieÅ”ama, lietojot Å”o kodu.
TÄtad, ko tieÅ”i programmÄtÄjiem jÄzina par domÄÅ”anu? Vispirms to paÅ”u, ko arÄ« citiem: ja tu neraksti, tad tev tikai Ŕķiet, ka tu domÄ. TurklÄt, ir jÄdomÄ pirms kodÄÅ”anas, un tas nozÄ«mÄ, ka ir jÄraksta pirms kodÄÅ”anas. SpecifikÄcija ir tas, ko mÄs rakstÄm pirms sÄkam kodÄt. SpecifikÄcija ir nepiecieÅ”ama jebkuram kodam, ko kÄds var izmantot vai mainÄ«t. Un Å”is "kÄds" var izrÄdÄ«ties pats 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 sarežģītÄm kÄda atseviŔķa metodei. Ko tieÅ”i vajag rakstÄ«t par kodu? JÄapraksta, ko tas dara, t.i., tas, 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 Å”o paÅÄmienu mÄs esam apguvuÅ”i algoritmu kursÄ, tad mÄs to saucam par algoritmu. Ja tas ir kaut kas Ä«paÅ”Äks un jauns, tad mÄs to saucam par augsta lÄ«meÅa projektÄÅ”anu. FormÄli atŔķirÄ«bu Å”eit nav: gan tas, gan tas ir programmas abstrakta modeļa veids.
KÄ tieÅ”i jÄraksta koda specifikÄcija? Galvenais: tai jÄbÅ«t par vienu lÄ«meni augstÄk par paÅ”u kodu. Tai jÄapraksta stÄvokļi un uzvedÄ«ba. Tai jÄbÅ«t tikpat stingrai, cik prasa uzdevums. Ja tu raksti specifikÄciju uzdevuma Ä«stenoÅ”anas veidam, tad to var uzrakstÄ«t pseido kodÄ vai ar PlusCal palÄ«dzÄ«bu. MÄcÄ«ties rakstÄ«t specifikÄcijas ir jÄizdara, izmantojot formÄlas specifikÄcijas. Tas sniegs tev nepiecieÅ”amÄs prasmes, kas noderÄs arÄ« neformÄlÄm specifikÄcijÄm. Bet kÄ iemÄcÄ«ties rakstÄ«t formÄlas specifikÄcijas? Kad mÄs mÄcÄ«jÄmies programmÄÅ”anu, mÄs rakstÄ«jÄm programmas un tad tÄs atkļūdojÄm. Tas pats attiecas arÄ« uz Å”eit: ir jÄuzraksta specifikÄcija, jÄpÄrbauda tÄ ar modeļu pÄrbaudes lÄ«dzekli un jÄpÄc tam labojumi jÄveic. TLA+, iespÄjams, nav labÄkais valoda formÄlai specifikÄcijai, un jÅ«su konkrÄtajÄm vajadzÄ«bÄm, visticamÄk, labÄk derÄs cita valoda. TLA+ priekÅ”rocÄ«ba ir tÄ, ka tÄ lieliski mÄca matemÄtisko domÄÅ”anu.
KÄ sasaistÄ«t specifikÄciju un kodu? Ar komentÄriem, kas sasaista matemÄtiskos jÄdzienus un to realizÄciju. Ja jÅ«s strÄdÄjat ar grafiem, tad programmas lÄ«menÄ« jums bÅ«s mezglu masÄ«vi un saikÅu masÄ«vi. TÄpÄc jums jÄraksta, kÄ tieÅ”i grafiks tiek realizÄts ar Ŕīm programmÄÅ”anas struktÅ«rÄm.
JÄatzÄ«mÄ, ka nekas no iepriekÅ” minÄtÄ neattiecas uz paÅ”u koda rakstÄ«Å”anas procesu. Kad jÅ«s rakstÄt kodu, kas ir treÅ”ais solis, jums arÄ« ir jÄdomÄ un jÄizplÄno programma. Ja apakÅ”uzdevums ir sarežģīts vai neskaidrs, jums jÄuzraksta tam specifikÄcija. Bet par paÅ”u kodu es Å”eit nerunÄju. JÅ«s varat izmantot jebkuru programmÄÅ”anas valodu, jebkuru metodoloÄ£iju, runa nav par tÄm. TurklÄt nekas no iepriekÅ” teiktÄ neatbrÄ«vo no nepiecieÅ”amÄ«bas testÄt un labot kodu. Pat ja abstraktÄ modeļa rakstÄ«Å”ana ir pareiza, tÄs realizÄcijÄ var bÅ«t kļūdas.
SpecifikÄciju rakstÄ«Å”ana ir papildu posms koda rakstÄ«Å”anas procesÄ. Pateicoties tam, daudzas kļūdas var atklÄt ar mazÄkÄm pÅ«lÄm ā mÄs to zinÄm no Amazon programmÄtÄju pieredzes. Ar specifikÄcijÄm programmu kvalitÄte palielinÄs. TÄtad, kÄpÄc mÄs tik bieži spÄjam iztikt bez tÄm? TÄpÄc, ka rakstÄ«t ir grÅ«ti. Un rakstÄ«t ir grÅ«ti, jo tam nepiecieÅ”ams domÄt, un domÄt arÄ« ir grÅ«ti. VienmÄr ir vieglÄk izlikties, ka domÄjat. Å eit var izdarÄ«t analoÄ£iju ar skrieÅ”anu ā jo mazÄk jÅ«s skrienat, jo lÄnÄk jÅ«s skrienat. Jums jÄtrenÄ savi muskuļi un jÄpraktizÄ rakstÄ«Å”ana. NepiecieÅ”ama prakse.
SpecifikÄcija var bÅ«t nepareiza. IespÄjams, ka jÅ«s kaut kur izdarÄ«jÄt kļūdu, vai arÄ« prasÄ«bas ir mainÄ«juÅ”Äs, vai ir bijusi nepiecieÅ”amÄ«ba veikt uzlabojumus. Ikviens kods, ko kÄds izmanto, ir jÄmaina, tÄpÄc agrÄk vai vÄlÄk specifikÄcija pÄrstÄs atbilst programmÄ. IdeÄlÄ gadÄ«jumÄ Å”ajÄ gadÄ«jumÄ vajadzÄtu uzrakstÄ«t jaunu specifikÄciju un pilnÄ«bÄ pÄrveidot kodu. MÄs lieliski zinÄm, ka neviens tÄ nedara. PraksÄ mÄs labojam kodu un, iespÄjams, atjauninÄm specifikÄciju. Ja tas ir obligÄti, agrÄk vai vÄlÄk notiek, tad kÄpÄc vispÄr rakstÄ«t specifikÄcijas? PirmkÄrt, cilvÄkam, kurÅ” labos jÅ«su kodu, katrs liekais vÄrds specifikÄcijÄ bÅ«s zelta vÄrtÄ«bÄ, un Å”is cilvÄks varat bÅ«t arÄ« jÅ«s paÅ”i. Es bieži sev pÄrmÄju par nepietiekamo specifikÄciju, kad laboju savu kodu. Un es uzrakstu vairÄk specifikÄciju nekÄ kodu. TÄpÄc, kad jÅ«s labojat kodu, specifikÄcija vienmÄr ir jÄatjaunina. OtrkÄrt, ar katru labojumu kods kļūst sliktÄks, to kļūst arvien grÅ«tÄk lasÄ«t un uzturÄt. TÄ ir entropijas pieaugÅ”ana. Bet, ja jÅ«s nesÄkat ar specifikÄciju, tad katra uzrakstÄ«tÄ rinda bÅ«s labojums, un kods no paÅ”a sÄkuma bÅ«s apgrÅ«tinoÅ”s un grÅ«ti lasÄms.
KÄ teica , neviens kauja netika uzvarÄta pÄc plÄna, un neviens kauja netika uzvarÄta bez plÄna. Un viÅÅ” zinÄja kaut ko par kaujÄm. Ir uzskats, ka specifikÄciju rakstÄ«Å”ana ir tukÅ”a laika tÄrÄÅ”ana. Dažreiz tÄ tieÅ”Äm tÄ ir, un uzdevums ir tik vienkÄrÅ”s, ka pÄrdomÄt to nav vÄrts. Bet vienmÄr jÄatceras, ka, kad jums ieteicams nerakstÄ«t specifikÄcijas, tas nozÄ«mÄ, ka jums ieteicams nedomÄt. Un par to katru reizi jÄpadomÄ. Uzdevuma pÄrdomÄÅ”ana negarantÄ, ka jÅ«s nepieļausiet kļūdas. KÄ mÄs zinÄm, neviens burvju nÅ«jiÅas nav izgudrots, un programmÄÅ”ana ir sarežģīts process. Bet, ja jÅ«s nepÄrdomÄjat uzdevumu, jÅ«s garantÄti pieļausiet kļūdas.
Papildu informÄciju par TLA+ un PlusCal var atrast specializÄtajÄ mÄjaslapÄ, pie tÄs var piekļūt no manas mÄjaslapas . Tas arÄ« viss, paldies par uzmanÄ«bu.
AtgÄdinu, ka Å”is ir tulkojums. Kad jÅ«s rakstÄ«siet komentÄrus ā atcerieties, ka autors tos neizlasÄ«s. Ja jums patieÅ”Äm gribas sazinÄties ar autoru, viÅÅ” bÅ«s konferencÄ Hydra 2019, kas notiks 2019. gada 11.-12. jÅ«lijÄ SanktpÄterburgÄ. Biļetes var iegÄdÄties .
Avots: habr.com
Russian
Italian
German
Polish
Estonian
Albanian
Bulgarian
Croatian
Czech
Danish
Dutch
English
French
Hungarian
Latvian
Portuguese
Romanian
Slovak
Slovenian
Spanish
Swedish