Ky është një artikull përkthim . Por para saj ka një hyrje të shkurtër. Si formohen zombi? Çdo njeri ka përjetuar situatën kur dëshiron të tërheqë një mik ose koleg në nivelin e tij, por nuk ia del. Dhe ndonjëherë «nuk ia del» nuk është aq shumë për ty, sa për të: nga njëra anë është paga normale, detyrat dhe kështu me radhë, ndërsa nga ana tjetër është nevoja për të menduar. Të mendosh është e pakëndshme dhe e dhimbshme. Ai dorëzohet shpejt dhe vazhdon të shkruajë kod, pa aktivizuar fare trurin. A e di sa shumë energji duhet të harxhohet për të kapërcyer barrierën e pafuqisë së mësuar, dhe thjesht nuk e bën. Kështu formohen zombit, të cilët duket se mund të shërohen, por ndoshta askush nuk do të merret me këtë.
Kur e pashë se (po, po, ai vetë nga tekstet shkollore) dhe nuk bën një paraqitje, por një sesion pyetje-përgjigje, unë u shqetësova pak. Për raste emergjente, Leslie është një shkencëtar i njohur ndërkombëtarisht, autor i punimeve themelore në llogaritë e shpërndara, dhe ju mund ta njihni gjithashtu nga shkronjat La në fjalën LaTeX — "Lamport TeX". Faktori i dytë shqetësues është kërkesa e tij: çdo kush që do të vijë duhet (plotësisht falas) të dëgjojë disa nga prezantimet e tij përpara, të formulojë së paku një pyetje për to dhe vetëm atëherë të vijë. Vendosa të shikoj se çfarë thotë Lamport — dhe është e mrekullueshme! Kjo është pikërisht ajo gjë, lidhja magjike-tabletë për të shëruar trurin e dëmtuar. Paralajmëroj: nga teksti do të digjen ndjeshëm ata që preferojnë metodologjitë super fleksibile dhe ata që nuk u pëlqejnë testimet e asaj që është shkruar.
Pas hibridizimit, në fakt, fillon përkthimi i seminarit. Lexim të këndshëm!
Pavarësisht nga detyra që merrni, gjithmonë duhet të kaloni nëpër tre hapa:
- të vendosni se cilin objektiv dëshironi të arrini;
- të vendosni se si do të përpiqeni të arrini objektivin tuaj;
- të arrini objektivin tuaj.
Kjo është e rëndësishme edhe për programimin. Kur shkruajmë kod, na nevojitet:
- të vendosim se çfarë duhet të bëjë programi;
- përcaktoni se si duhet të përmbushë detyrën e saj;
- shkruani kodin përkatës.
Hapi i fundit, natyrisht, është shumë i rëndësishëm, por për të nuk do flas sot. Në vend të kësaj, ne do të diskutojmë dy hapat e parë. Këto i bën çdo programues para se të fillojë të punojë. Nuk uleni të shkruani nëse nuk keni vendosur se çfarë po shkruani: një shfletues apo një bazë të dhënash. Një përfaqësim i saktë i qëllimit duhet të jetë patjetër prezent. Dhe ju patjetër mendoni se çfarë do të bëjë programi, e jo të shkruani pa menduar në shpresë se kodi do të shndërrohet vetë në shfletues.
Si si ndihmoni qe të mendoni paraprakisht për kodin? Sa përpjekje duhet të shpenzojmë për këtë? Të gjithçka varet nga sa e ndërlikuar është problemi që po zgjidhim. Le të supozojmë se dëshirojmë të shkruajmë një sistem të shpërndarë rezistent ndaj dështimeve. Në këtë rast, duhet ta mendojmë çdo gjë përpara se të ndihmojmë sërish në kod. Por nëse na nevojitet vetëm të rrisim një variabël të plotë me 1? Në shikim të parë, kjo duket e thjeshtë dhe s'ka nevojë për mendim, por pastaj kujtojmë se ndoshta do të ndodhë mbingarkesë. Prandaj, për të kuptuar nëse problemi është i thjeshtë apo i ndërlikuar — fillimisht duhet të mendojmë.
Nëse mendoni paraprakisht për zgjidhjet e mundshme të problemit, mund të shmangni gabimet. Por që kjo të ndodhë, mendja juaj duhet të jetë e qartë. Për ta arritur këtë, duhet të shkruani mendimet tuaja. Më pëlqen shumë një citat nga Dick Gindon: «Kur shkruani, natyra ju tregon se sa pa rregull është mendimi juaj». Nëse nuk shkruani, vetëm mendoni se po mendoni. Dhe duhet të shkruani mendimet tuaja në formën e specifikimeve.
Specifikimet kryejn shumë funksione, sidomos në projekte të mëdha. Por unë do të flas vetëm për një nga to: ato na ndihmojnë të mendojmë qartë. Të mendosh qartë është shumë e rëndësishme dhe mjaft e vështirë, prandaj këtu na nevojitet çdo ndihmë. Në cilin gjuhë duhet të shkruajmë specifikimet? Ky gjithmonë është pyetja e parë për programuesit: në cilën gjuhë do ta shkruajmë. S’ka një përgjigje të saktë për të: problemet që zgjidhim janë shumë të ndryshme. Për disa, TLA+ është i dobishëm — ky është një gjuhë specifikimesh që unë e kam zhvilluar. Për të tjerë, është më e lehtë të përdorin mandarinin. E gjithë kjo varet nga situata.
Një pyetje më e rëndësishme është: si të arrijmë një mendim më të qartë? Përgjigjja: ne duhet të mendojmë si shkencëtarë. Ky është një stil mendimi që ka dhënë rezultate të shkëlqyera gjatë 500 viteve të fundit. Në shkencë, ne krijojmë modele matematikore të realitetit. Astronomija ishte ndoshta shkenca e parë në kuptimin e vërtetë të fjalës. Në modelin matematikor të përdorur në astronomi, trupat qiellorë shfaqen si pika me masë, pozicion dhe impuls, megjithatë në realitet ata janë objekte shumë komplekse me male dhe oqeane, me rrjedha dhe tërheqje. Ky model, si çdo model tjetër, është krijuar për të zgjidhur probleme të caktuara. Ai është gjithashtu shumë i përshtatshëm për të përcaktuar se ku duhet të drejtohet teleskopi nëse duhet të gjendet një planet. Por nëse dëshiron të parashikosh motin në këtë planet, ky model nuk do të funksionojë.
Matematika na lejon të përcaktojë karakteristikat e një modeli. Shkenca tregon se si këto karakteristika lidhen me realitetin. Le të flasim për shkencën tonë, informatikën. Realiteti me të cilin punojmë përfshin sisteme kompjuterike të ndryshme: procesorë, konsola lojërash, kompjuterë që ekzekutojnë programe dhe më shumë. Do flas për ekzekutimin e një programi në kompjuter, por, në thelb, të gjitha këto përfundime janë të aplikueshme në çdo sistem kompjuterik. Në shkencën tonë përdorim shumë modele të ndryshme: makina e Turing-ut, grupe të pjesshme të renditur të ngjarjeve dhe shumë të tjera.
Çfarë është një program? Është çdo kod që mund të shqyrtohet në mënyrë të pavarur. Le të supozojmë se na nevojitet të shkruajmë një shfletues. Ne përmbushim tri detyra: dizajnojmë paraqitjen e programit për përdoruesin, pastaj shkruajmë një skemë të lartë të programit, dhe përfundimisht shkruajmë kodin. Gjatë shkruarjes së kodit, kuptojmë se na nevojitet të krijojmë një mjet për formatimin e tekstit. Këtu na nevojitet përsëri të zgjidhim tri detyra: të përcaktojmë se cili tekst do të kthejë kjo mjet; të zgjedhim një algoritëm për formatimin; të shkruajmë kodin. Kjo detyrë ka një nën detyrë: të fusë saktë defisin në fjalë. Këtë nën detyrë e zgjidhim gjithashtu në tre hapa — siç e shohim, ato përsëriten në shumë nivele.
Le të shohim më hollësisht hapat e parë: çfarë problemi zgjidh programi. Këtu ne shpesh e modelojmë programin si një funksion, i cili merr disa të dhëna hyrëse dhe jep disa të dhëna dalëse. Në matematikë, funksioni përshkruhet zakonisht si një grup i renditur çiftërash. Për shembull, funksioni i ngritjes në katror për numrat natyrorë përshkruhet si grupi {, , , , ...}. Zona e definimit të këtij funksioni është grupi i elementeve të parë të çdo çifti, domethënë numrat natyrorë. Për të përcaktuar funksionin, na nevojitet të caktojmë zonën e tij të definimit dhe formulën.
Por funksionet në matematikë nuk janë të njëjta si funksionet në gjuhët e programimit. Matematika është shumë më e thjeshtë. Duke qenë se nuk kam kohë për shembuj të ndërlikuar, le të marrim një të thjeshtë: një funksion në gjuhën C ose një metodë statike në Java që kthen gjendjen më të madhe të përbashkët (GCD) të dy numrave të plotë. Në specifikimin e kësaj metode do të shkruajmë: llogarit GCD(M,N) për argumentet M dhe N, ku GCD(M,N) — një funksion, zona e definimit të cilit është grupi i çiftëve të numrave të plotë, dhe vlera e kthyer është numri më i madh i plotë me të cilin ndahen. M dhe N. Si lidhët kjo model me realitetin? Modeli punon me numra të plotë, ndërsa në C ose Java kemi 32-bitësh. int. Ky model na lejon të zgjidhim nëse algoritmi është i saktë. GCD, por nuk do të parandalojë gabimet e mbingarkesës. Për këtë do të ishte e nevojshme një model më i komplikuar, për të cilin nuk ka kohë.
Le të flasim për kufizimet e funksionit si model. Disa programe (p.sh., sistemet operative) nuk përfundojnë me kthimin e një vlerë të caktuar për argumente të caktuara, ato mund të ekzekutohen vazhdimisht. Për më tepër, funksioni si model nuk është i përshtatshëm për hapin e dytë: planifikimi i mënyrës për të zgjidhur problemin. Shtimi i shpejtë dhe shtimi i balonave llogarisin të njëjtin funksion, por janë algoritma krejtësisht të ndryshëm. Prandaj, për të përshkruar mënyrën e arrijes së qëllimit të programit, unë përdor një model tjetër, ta quajmë modelin standard të sjelljes. Programi në të përfaqësohet si një grup i gjithë sjelljeve të lejuara, secila prej të cilave është një sekuencë gjendjesh, dhe gjendja është një caktim vlerash për variablat.
Le të shohim se si do të duket hapi i dytë për algorimin e Euklidit. Na nevojitet të llogarisim GCD(M, N). Ne e inicojmë M si x, dhe N si y, dhe pastaj vazhdojmë të heqim variablën më të vogël nga ajo më e madhe deri sa ato të bëhen të barabarta. Për shembull, nëse M = 12, dhe N = 18, mund të përshkruajmë këtë sjellje:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Por nëse M = 0 dhe N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Këtu duhet të bëjmë një shkëputje të vogël për produktivitetin. Ai shpesh matet në numrin e rreshtave të kodit të shkruar në ditë. Por puna juaj është shumë më e dobishme nëse keni hequr një sasi të caktuar rreshtash, sepse keni më pak hapësirë për defekte. Dhe heqja e kodit është më e lehtë pikërisht në hapin e parë. Mund të jetë se thjesht nuk keni nevojë për të gjitha ato funksionalitete që po përpiqeni të realizoni. Mënyra më e shpejtë për të thjeshtuar programin dhe për të kursyer kohë është të mos bëni gjëra që nuk ia vlen të bëni. Hapi i dytë është në vendin e dytë për potencialin e kursimit të kohës. Nëse e matni produktivitetin në numrin e rreshtave të shkruar, mendimi për mënyrën e kryerjes së detyrës do t'ju bëjë më pak produktivë, pasi do të jeni në gjendje të zgjidhni të njëjtën detyrë me një kod më të vogël. Statistika e saktë nuk mund t’i jap këtu, pasi nuk kam një mënyrë për të numëruar atë sasi rreshtash që nuk i kam shkruar falë kohës që kalova për specifikimin, domethënë për hapat e parë dhe të dytë. Dhe në këtë eksperiment nuk mund të procedohet as, sepse në eksperiment nuk kemi të drejtë të kryejmë hapin e parë, detyra është e përcaktuar paraprakisht.
Në specifikimet informale është lehtë të mos merret parasysh shumë vështirësi. Nuk ka asgjë të komplikuar në shkruarjen e specifikimeve strikte për funksionet, nuk do ta diskutoj këtë. Në vend të kësaj, do të flasim për shkruarjen e specifikimeve strikte për modelet standarde të sjelljes. Ekziston një teoremë që thotë se çdo shumëllojshmëri sjelljesh mund të përshkruhet përmes pronës së sigurisë (safety) dhe pronës së qëndrueshmërisë (liveness). Siguria do të thotë që nuk do të ndodhin gjëra të këqija, programa nuk do të japë përgjigje të gabuara. Qëndrueshmëria do të thotë që njëherë e mirë do të ndodhin gjëra të mira, domethënë programa njëherë e mirë do të japë përgjigje të sakta. Në përgjithësi, siguria është një tregues më i rëndësishëm, gabimet ndodhin më shpesh këtu. Prandaj, për të kursyer kohë, nuk do të flas për qëndrueshmërinë, edhe pse ajo, natyrisht, është gjithashtu e rëndësishme.
Ne arrijmë sigurinë duke specifikuar, së pari, një numër të madh gjendjesh fillestare. Dhe, së dyti, marrëdhëniet me të gjitha gjendjet e mundshme pasuese për secilën gjendje. Do të veprojmë si shkencëtarë dhe do të përcaktojmë gjendjet matematikisht. Grupi i gjendjeve fillestare përshkruhet me një formulë, për shembull, në rastin e algoritmit të Euclidit: (x = M) ∧ (y = N). Për vlera të caktuara M dhe N ekziston vetëm një gjendje fillestare. Marrëdhënia me gjendjen e ardhshme përshkruhet me formulën ku variablat e gjendjes së ardhshme shkruhen me një tërheqje, ndërsa të gjendjes aktuale - pa. Në rastin e algoritmit të Euclidit, do të merremi me disjunkcionin e dy formulave, ku njëra prej tyre x është vlera më e madhe, ndërsa në të dytën — y:
Në rastin e parë, vlera e re y është e barabartë me vlerën e mëparshme y, ndërsa vlera e re x e marrim duke i hequr vlerës më të vogël atë më të madhe. Në rastin e dytë, ne bëjmë të kundërtën.
Të kthehemi te algoritmi i Euclidit. Supozojmë sërish se M = 12, N = 18. Kjo përcakton një gjendje fillestare të vetme, (x = 12) ∧ (y = 18). Më pas, ne zëvendësojmë këto vlera në formulën e mësipërme dhe marrim:
Këtu, zgjidhja e vetme e mundshme është: x' = 18 - 12 ∧ y' = 12, dhe merrni sjelljen: [x = 12, y = 18]. Po ashtu, ne mund të përshkruajmë të gjitha gjendjet në sjelljen tonë: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Në gjendjen e fundit [x = 6, y = 6] të dyja pjesët e shprehjes do të jenë false, prandaj, nuk ka gjendje të ardhshme për të. Pra, ne kemi një spesifikim të plotë të hapit të dytë — siç shihni, kjo është krejtësisht matematikë e zakonshme, si për inxhinierët dhe shkencëtarët, dhe jo e çuditshme, si në shkencën kompjuterike.
Këto dy formula mund të bashkohen në një formulë të logjikës temporale. Ajo është elegante dhe nuk është e vështirë ta shpjegosh, por nuk ka kohë për të tani. Logjika temporale mund të na nevojitet vetëm për pronësinë e jetëgjatësisë, nuk është e nevojshme për sigurinë. Logjika temporale si e tillë nuk pëlqehet, nuk është matematikë krejtësisht e zakonshme, por në rastin e jetëgjatësisë ajo është një të keqe të nevojshme.
Në algoritmin e Euclidit për çdo vlerë x dhe y ka vlera unike x' dhe y', të cilat e bëjnë marrëdhënien me gjendjen e ardhshme të vërtetë. Në fjalë të tjera, algoritmi i Euclidit është deterministik. Për të modeluar një algoritëm të pandeterminueshëm, duhet që gjendja aktuale të ketë disa gjendje të mundshme të ardhshme, dhe që çdo vlerë e variablës pa linjë të ketë disa vlera të variablës me linjë, për të cilat marrëdhënia me gjendjen e ardhshme është e vërtetë. Nuk është e vështirë të bëhet, por tani nuk do të jap shembuj.
Për të bërë një mjet funksional, na nevojitet matematikë formale. Si ta bëjmë specifikimin formal? Për këtë do të na duhet një gjuhë formale, për shembull, . Specifikimi i algoritmit të Euklidit do të duket kështu në këtë gjuhë:
Simboli i shenjës së barazisë me trekëndësh do të thotë se vlera në anën e majtë të shenjës është e përcaktuar si e barabartë me vlerën në anën e djathtë të shenjës. Në thelb, specifikimi është një definim, në rastin tonë dy definime. Në TLA+ duhet të shtojmë shpallje dhe disa sintaksë, siç është në slajdin më sipër. Në ASCII do të duket kështu:
Siç e shohim, nuk ka asgjë të komplikuar. Specifikimi në TLA+ mund të testohet, dmth. të kalojmë të gjitha sjelljet e mundshme në një model të vogël. Në rastin tonë, ky model do të jetë vlerat e caktuara. M dhe N. Ky është një mënyrë shumë efikase dhe e thjeshtë e verifikimit, e cila kryhet plotësisht në mënyrë automatike. Përveç kësaj, është e mundur të shkruhen prova formale të vërtetësisë dhe të verifikohen ato mekanikisht, por kjo kërkon shumë kohë, kështu që askush nuk e bën atë.
Disavantazhi kryesor i TLA+ është se kjo është matematikë, dhe programuesit e shkencëtarët e kompjuterëve e kanë frikë matematikën. Në shikim të parë, kjo tingëllon si një shaka, por, fatkeqësisht, po e them këtë me seriozitet të plotë. Kolegu im sapo më tregoi se si përpiqej të shpjegonte TLA+ disa zhvilluesve. Sa herë që para ekranit shfaqeshin formulat, ata menjëherë merrnin një shikim qelqi. Pra, nëse TLA+ është frikësuese, mund të përdoren , është një lloj gjuhe programimi për lodra. Një shprehje në PlusCal mund të jetë çdo shprehje TLA+, që do të thotë, në thelb, çdo shprehje matematikore. Për më tepër, PlusCal ka sintaksë për algoritmet ndeterministike. Duke qenë se në PlusCal është e mundur të shkruhet çdo shprehje TLA+, ai është dukshëm më i shprehshëm se çdo gjuhë programimi reale. Më tej, PlusCal kompilohet në një specifikim të lehtë për t'u lexuar TLA+. Kjo nuk do të thotë, natyrisht, që një specifikim i ndërlikuar PlusCal do të shndërrohet në një të thjeshtë në TLA+ — vetëm përputhja midis tyre është e qartë, pa u shtuar kompleksitet i ri. Në fund, ky specifikim mund të kontrollohet me mjete TLA+. Në përgjithësi, PlusCal mund të ndihmojë në kapërcimin e fobisë së matematikës, është e lehtë për t'u kuptuar edhe për programuesit dhe shkencëtarët kompjuterikë. E kaluara ime, për një kohë (rreth 10 vjet), kam publikuar algoritme në të.
Ndoshta dikush do të kundërshtojë se TLA+ dhe PlusCal janë matematikë, dhe matematikë funksionon vetëm me shembuj të shpikur. Por në praktikë, nevojitet një gjuhë reale me tipe, procedura, objekte dhe kështu me radhë. Nuk është kështu. Ja çfarë thotë Kris Newcomb, që ka punuar në Amazon: «Kemi përdorur TLA+ në dhjetë projekte të mëdha, dhe në secilin rast përdorimi i tij ka kontribuar ndjeshëm në zhvillim, sepse arritëm të kapnim defekte të rrezikshme para se të dilnin në prodhim dhe sepse na dha kuptimin dhe sigurinë e nevojshme për optimizime agresive të performancës, pa ndikuar në saktësinë e programit». Shpesh dëgjohet se përdorimi i metodave formale sjell kod të paaftë — por në praktikë, e kundërta është e vërtetë. Për më tepër, ekziston mendimi se menaxherët është e pamundur t'i bindësh për nevojën e metodave formale, edhe nëse programuesit janë të bindur në përdorimin e tyre. Por Newcomb shkruan: «Menaxherët tani po e shtyjnë atë që të shkruhen specifikime në TLA+, dhe me më shumë kohë të posaçme dhënë për këtë». Pra kësaj, kur menaxherët shohin se TLA+ funksionon, ata e pranojnë me gëzim. Chris Newcomb e shkroi këtë diku rreth gjashtë muaj më parë (në tetor 2014), dhe tani, sa di, TLA+ përdoret në 14 projekte, jo 10. Një shembull tjetër i lidhur me projektimin e XBox 360. Një praktikant i doli para Charles Tecker dhe shkroi një specifikim për sistemin e memorjes. Falë këtij specifikimi u zbulua një gabim, i cili ndryshe do të ishte anashkaluar, dhe për shkakun e të cilit çdo XBox 360 do të çonte në dështim pas katër orësh përdorimi. Inxhinierët e IBM konfirmuan se testet e tyre nuk do ta kishin zbuluar këtë gabim.
Më shumë rreth TLA+ mund të lexoni në internet, por tani le të flasim për specifikimet joformale. Ne rrallë herë shkojmë të shkruajmë programe që llogaritën më të përbashkëtin dhe gjëra të ngjashme. Shumë më shpesh ne shkruajmë programe si një mjet për printimin strukturor (pretty-printer), që unë e shkrova për TLA+. Pas përpunimit më të thjeshtë, kodi në TLA+ do të dukej si më poshtë:
Por shembullin e para, përdoruesi ka prirjen të dëshirojë që shenjat e konjuksionit dhe barazimit të jenë të rregulluara. Pra, formatimi i duhur do të duket më shumë kështu:
Le të shqyrtojmë një shembull tjetër:
Në këtë rast, përkundrazi, rregullimi i shenjave të barazimit, shumëzimit dhe mbledhjes në burim ishte rastësor, prandaj përpunimi më i thjeshtë është mjaftueshëm. Në përgjithësi, nuk ka një përkufizim matematikor të saktë për formatimin e duhur, sepse "i saktë" në këtë rast do të thotë "ashtu siç dëshiron përdoruesi", dhe kjo nuk mund të përcaktohet matematikisht.
Duket se, nëse nuk kemi një përkufizim të vërtetësisë, atëherë specifikimi është i padobishëm. Por kjo nuk është e vërtetë. Nëse nuk e dimë se çfarë duhet të bëjë programi, kjo nuk do të thotë që nuk duhet të mendojmë për punën e tij — përkundrazi, duhet të investojmë më shumë përpjekje. Specifikimi në këtë rast është veçanërisht i rëndësishëm. Të përcaktojmë programin optimal për printimin strukturor është e pamundur, por kjo nuk do të thotë se nuk duhet të merremi me të, dhe të shkruajmë kodin si një rrjedhë mendimi — kjo nuk është e drejtë. Në fund, unë shkrova një specifikim me gjashtë rregulla me përkufizime. në formë komentesh në skedarin Java. Ja një shembull i njërit prej rregullave: një token komenti të majtë është LeftComment i rreshtuar me tokenin mbështetës. Ky rregull është shkruar në, për ta thënë ashtu, anglishten matematikore: LeftComment i rreshtuar, komenti i majtë dhe token mbështetës — terma me përkufizime. Kjo është mënyra se si matematicienët përshkruajnë matematikën: shkruajnë përkufizime të terma dhe mbi bazën e tyre — rregulla. Përdorimi i një specifikimi të tillë është se është shumë më e lehtë të kuptohet dhe të debatohet mbi gjashtë rregullat sesa mbi 850 rreshta kod. Duhet thënë se shkruarja e këtyre rregullave ishte e vështirë, u desh shumë kohë për t'i debug-uar. Përdorës dhe për këtë qëllim shkrova kodin që raportonte se cili ishte saktësisht rregulli që përdorej. Falë faktit se e kam testuar këto gjashtë rregulla me disa shembuj, nuk pata nevojë të debatoj 850 rreshta kodi, dhe gabimet u gjetën përsa shpejt. Në Java ka mjete të shkëlqyera për këtë. Po të kisha thjesht shkruar kodin, do të më kishte marrë ndjeshëm më shumë kohë, dhe formati do të kishte rezultuar me cilësi më të dobët.
Pse nuk mund të përdoret specifikimi formal? Nga njëra anë, saktësia e ekzekutimit këtu nuk është aq e rëndësishme. Një printim strukturor mund të mos i pëlqejë askujt, kështu që nuk ishte nevoja të arrihesha që të punonte saktë në të gjitha situatat e jashtëzakonshme. Po aq e rëndësishme është fakti që nuk kisha mjete adekuate. Mjeti për të verifikuar modelet TLA+ këtu është i pa dobishëm, kështu që do të më duhej të shkruaja manualisht shembuj.
Specifikacioni i dhënë ka karakteristika të zakonshme për të gjitha specifikimet. Ajo është në një nivel më të lartë se kodi. Mund të realizohet në çdo gjuhë. Çdo mjet ose metodë për të shkruar atë është e panevojshme. Asnjë kurs programimi nuk do t'ju ndihmojë të shkruani këtë specifikim. Nuk ka mjete që mund ta bëjnë këtë specifikim të panevojshëm, përveç nëse po shkruani një gjuhë të krijuar posaçërisht për të shkruar programe strukturore në TLA+. Në fund, ky specifikim nuk tregon asgjë mbi mënyrën se si ne do të shkruajmë kodin, vetëm tregon se çfarë bën ky kod. Ne shkruajmë specifikimin për të na ndihmuar të mendojmë rreth problemit, para se të fillojmë të mendojmë për kodin.
Por ky specifikim ka gjithashtu veçori që e dallojnë atë nga specifikimet e tjera. 95% e specifikimeve të tjera janë ndjeshëm më të shkurtra dhe më të thjeshta:
Për më tepër, ky specifikim është një grup rregullash. Si rregull, ky është një shenjë e një specifikimi të dobët. Të kuptosh pasojat e një grupi rregullash është mjaft e vështirë, dhe saktësisht për këtë arsye më është dashur të kaloj shumë kohë duke i debug-uar ato. Megjithatë, në këtë rast, nuk kam gjetur një mënyrë më të mirë.
Është e domosdoshme të thuhet disa fjalë rreth programeve që punojnë në mënyrë të vazhdueshme. Në përgjithësi, ato operojnë paralelisht, për shembull, sistemet operative ose sistemet e shpërndara. Të kuptuarit e tyre në mendje ose në letër është një sfidë për shumë pak, dhe unë nuk i përkas asaj kategorie, megjithëse ndonjëherë më ka qenë e mundur. Prandaj, janë të nevojshme mjete që do të kontrollojnë punën tonë — për shembull, TLA+ ose PlusCal.
Përse duhej të shkruaja specifikimin, nëse unë e dija se çfarë duhej të bënte kodi? Në të vërtetë, më dukej se e dija. Për më tepër, me një specifikim, një person i jashtëm nuk ka nevojë për të hyrë në kod për të kuptuar se çfarë bën ai. Kam një rregull: nuk duhet të ketë asnjë rregull të përgjithshëm. Ky rregull ka, natyrisht, përjashtimin e tij, është rregulli i vetëm i zakonshëm që ndjek: specifikimi i asaj që bën kodi duhet të informojë njerëzit për gjithçka që duhet të dinë gjatë përdorimit të këtij kodi.
Pra në fillim, çfarë duhet të dinë programuesit rreth mendimit? E para, ajo që duhet të dinë edhe të gjithë të tjerët: nëse nuk shkruani, keni vetëm iluzionin se po mendoni. Për më tepër, duhet të mendoni para se të kodoni, dhe kjo do të thotë se duhet të shkruani para se të kodoni. Specifikimi është ajo që shkruajmë para se të fillojmë kodimin. Specifikimi është i nevojshëm për çdo kod që mund të përdoret ose të modifikohet nga dikush tjetër. Dhe ky "dikush tjetër" mund të jetë vetë autori i kodit një muaj pas shkruajturit të tij. Specifikimi është i nevojshëm për programe dhe sisteme të mëdha, për klasa, për metoda dhe ndonjëherë madje edhe për pjesë komplekse të një metode të veçantë. Çfarë duhet të shkruajmë për kodin? Duhet të përshkruajmë se çfarë bën, domethënë çfarë mund të jetë e dobishme për çdo person që e përdor këtë kod. Ndonjëherë, mund të jetë e nevojshme të tregojmë se si e arrin kodimi qëllimin e tij. Nëse kjo metodë është trajtuar në kursin për algoritme, ne e quajmë atë algoritëm. Nëse është diçka më specifike dhe të re, atëherë e quajmë projektim në nivel të lartë. Së pari, nuk ka ndonjë dallim formal: të dyja janë modele abstrakte të programit.
Si duhet të shkruani një spécifikim të kodit? E rëndësishme: ai duhet të jetë mbi nivelin e vetë kodit. Ai duhet të përshkruajë shtetet dhe sjelljet. Duhet të jetë i dhënë aq sa e kërkon detyra. Nëse po shkruani një specifikim të mënyrës së zgjidhjes së detyrës, atëherë mund ta shkruani në pseudokod ose duke përdorur PlusCal. Të frisni rreth shkrimit të specifikimeve duhet të mësoni nëpërmjet specifikimeve formale. Kjo do t'ju japë aftësi të nevojshme, të cilat do t'ju ndihmojnë edhe me ato informale. Dhe si të mësoni të shkruani specifikime formale? Kur ne mësonim programimin, ne shkruanim programe dhe pastaj i rregullonim ato. E njëjta gjë vlen këtu: duhet të shkruani një specifikim, ta verifikoni atë përmes një mjeti të kontrollit të modeleve dhe të korrigjoni gabimet. TLA+ ndoshta nuk është gjuha më e mirë për specifikim formal, dhe për nevojat tuaja specifike probabilisht do të ishte më mirë një gjuhë tjetër. Avantazhi i TLA+ është se ai mëson mendimin matematikor mjaft mirë.
Si shpjegoni lidhjen midis specifikimeve dhe kodit? Me anë të komenteve, të cilat lidhin konceptet matematikore me zbatimin e tyre. Nëse punoni me grafika, atëherë në nivelin e programit do të keni array të nyjave dhe array të lidhjeve. Prandaj, ju nevojitet të shkruani se si saktësisht grafiku implementohet me këto struktura programimi.
Duhet të theksohet se asgjë nga e sipërthënë nuk i referohet procesit të shkrimit të kodit. Kur shkruani kod, domethënë realizoni hapin e tretë, gjithashtu duhet të mendoni dhe planifikoni programin. Nëse nëndetyra del të jetë e komplikuar ose e paqartë, duhet të shkruani një specifikim për të. Por për kodin vetë nuk po flas këtu. Mund të përdorni çdo gjuhë programimi, çdo metodologji, nuk është fjala për to. Përveç kësaj, asgjë nga e sipërthënë nuk ju çliron nga nevoja për të testuar dhe debug kodin. Edhe nëse modeli abstrakt është shkruar saktë, në zbatimin e tij mund të ketë bugs.
Shkrimi i specifikimeve është një hap shtesë në procesin e kodimit. Falë tij, shumë gabime mund të zbulohen me më pak përpjekje — e dimë këtë nga eksperienca e programuesve në Amazon. Me specifikimet, cilësia e programeve rritet. Pse ndodhin atëherë kaq shpesh që ne i kalojmë pa to? Sepse të shkruarit është e vështirë. Dhe është e vështirë të shkruash, sepse për këtë duhet të mendosh, dhe të mendosh gjithashtu është e vështirë. Gjithmonë është më e lehtë të bësh si të mendosh. Këtu mund të bëhet një krahasim me vrapimin — sa më pak të vraponi, aq më ngadalë vraponi. Duhet të stërvisni muskujt tuaj dhe të ushtroni shkrimin. Praktika është e nevojshme.
Specifikimi mund të jetë i gabuar. Mund të keni bërë ndonjë gabim diku, ose kërkesat mund të kenë ndryshuar, ose është bërë e nevojshme të bëhen përmirësime. Çdo kod që përdoret nga dikush duhet të ndryshohet, prandaj vonë a herët specifikimi do të ndalojë së përputhuri me programin. Në mënyrë ideale, në këtë rast duhen shkruar një specifikim i ri dhe të rishkruhet plotësisht kodi. Ne e dimë mirë se askush nuk e bën kështu. Në praktikë, ne bëjmë patch në kod dhe ndoshta azhurnojmë specifikimin. Nëse kjo ndodh patjetër në një moment, atëherë përse të shkruajmë fare specifikime? Së pari, për atë që do të rregullojë kodin tuaj, çdo fjalë e panevojshme në specifikim do të jetë shumë e çmuar, dhe ky person mund të jeni vetë. Unë shpesh e qortoj veten për specifikimin e papërshtatshëm kur rregulloj kodin tim. Dhe unë shkruaj më shumë specifikime se sa kod. Prandaj, kur të rregulloni kodin, duhet ta përditësoni gjithmonë specifikimin. Së dyti, me çdo rregullim, kodi bëhet më i keq, bëhet gjithnjë e më e vështirë për t'u lexuar dhe mbajtur. Ky është një rritje e entropisë. Por nëse nuk filloni nga specifikimi, atëherë çdo varg i shkruar do të jetë një rregullim dhe kodi që nga fillimi do të jetë i rëndë dhe i vështirë për tu lexuar.
Siç tha , asnjë betejë nuk është fituar sipas planit, dhe asnjë betejë nuk është fituar pa plan. Ai dinte diçka për betejat. Ekziston mendimi se shkruajtja e specifikimeve është një humbje kohe. Ndonjëherë, kjo është e vërtetë, dhe detyra është aq e thjeshtë sa nuk ka asgjë për të menduar. Por gjithmonë duhet të mbani mend se kur ju këshillojnë të mos shkruani specifikacione, kjo do të thotë se ju rekomandojnë të mos mendoni. Dhe për këtë duhet të mendoni çdo herë. Mendimi i detyrës nuk garanton se nuk do të bëni gabime. Siç e dimë, askush nuk ka shpikur një magji, dhe programimi është një profesion kompleks. Por nëse nuk e mendoni detyrën, ju garantoni se do të bëni gabime.
Mund të lexoni më shumë mbi TLA+ dhe PlusCal në një site të veçantë, ku mund të hyni nga faqja ime e shtëpisë . Këtu kam gjithçka, faleminderit për vëmendjen.
Dua t'ju kujtoj se ky është një përkthim. Kur të shkruani komente — mbani mend se autori nuk do t'i lexojë ato. Nëse vërtet dëshironi të flisni me autorin, ai do të jetë në konferencën Hydra 2019, e cila do të zhvillohet më 11-12 korrik 2019 në Shën Petersburg. Biletet mund të blihen .
Burimi: habr.com
