Ky është një artikull përkthimi . Por para se të fillojmë, një hyrje e vogël. Si formohen zombit? Çdo njeri ka pasur raste kur dëshiron të inkurajojë një mik ose koleg për të arritur nivelin e tij, por nuk ia del. Dhe “nuk ia del” jo aq shumë prej nesh sa prej tij: në një anë të peshoreve është një pagë normale, detyrat dhe kështu me radhë, e në anën tjetër nevoja për të menduar. Të mendosh është e pakëndshme dhe e dhimbshme. Ai dorëzohet shpejt dhe vazhdon të shkruaj kod pa përfshirë mendjen e tij. E ke parasysh sa energji duhen për të kapërcyer barrierën e mësuarit të pafuqishëm, dhe thjesht nuk e bën. Kështu formohen zombit, të cilët, siç duket, mund të shërohen, por duket se askush nuk do të merret me këtë.
Kur pashë se (po, po, ai shoku i famshëm nga tekstet shkollore) dhe po bën jo një prezantim, por një seancë pyetje-përgjigje, u shqetësova pak. Për çdo rast, Leslie është një shkencëtar i njohur ndërkombëtarisht, autor i punimeve themelore në llogaritë e shpërndara, dhe ndoshta e njohim nga letra La në fjalën LaTeX — "Lamport TeX". Faktori i dytë që më shqetësoi ishte kërkesa e tij: çdo kush që do të vijë duhet (krejtësisht falas) të dëgjojë disa nga prezantimet e tij paraprakisht, të shpikë së paku një pyetje mbi to dhe vetëm atëherë të vijë. Vendosa të shikoj se çfarë thotë Lamport — dhe kjo është mahnitëse! Ky është pikërisht ajo gjë, lidhja magjike-tabletë për shërimin e zombit. Paralajmëroj: teksti mund të irritojë shumë ata që janë të apasionuar pas metodologjive të tepër fleksibël dhe ata që nuk i pëlqejnë testimin e asaj që janë shkruar.
Pas hapjes së seminarit, fillon përkthimi i seminarit. Lexim të këndshëm!
Kështu që sa herë që merrni përsipër një detyrë, gjithmonë duhet të kaloni tre hapa:
- të përcaktoni se çfarë qëllimi dëshironi të arrini;
- të vendosni se si do ta arrini këtë qëllim;
- të arrini qëllimin tuaj.
Kjo ndikon edhe në programim. Kur shkruajmë kod, na nevojitet:
- të vendosim se çfarë duhet të bëjë programa;
- të përcaktojmë se si përkatësi duhet ta përmbushë detyrën e saj;
- të shkruajmë kodin përkatës.
Hapi i fundit, padyshim, është shumë i rëndësishëm, por sot nuk do të flas për të. Në vend të kësaj, do të diskutojmë dy të parat. Ato bëhen nga çdo programues para se të fillojë të punojë. Nuk uleni të shkruani nëse nuk keni vendosur se çfarë saktësisht po shkruani: një shfletues ose një bazë të dhënash. Një koncept i qartë mbi qëllimin duhet patjetër të ekzistojë. Dhe ju patjetër imagjinoni se çfarë do të bëjë programi, dhe nuk shkruani ndonjëherë pa një plan, me shpresën se kodi do të shndërrohet vetë në shfletues.
Si ndodh kjo planifikim paraprak i kodit? Sa përpjekje duhet të investojmë në këtë? Çdo gjë varet nga sa kompleks është problemi që po zgjidhim. Supozoni se duam të shkruajmë një sistem të shpërndarë të qëndrueshëm. Në këtë rast, na nevojitet të mendojmë thellë për gjithçka para se të ulem në kod. E nëse thjesht na duhen të rrisim një variabël të plotë me 1? Në shikim të parë, dukej se është gjë triviale dhe nuk kërkon shumë reflektim, por pastaj e kujtojmë se ndodhi mund të ketë mbingarkesë. Prandaj, për të kuptuar nëse problemi është i thjeshtë apo i komplikuar, në fillim duhen menduar mirë.
Nëse planifikoni paraprakisht zgjidhjet e mundshme të problemit, mund të shmangni gabimet. Por për këtë është e nevojshme që mendja juaj të jetë e qartë. Për ta arritur këtë, duhet të shkruani mendimet tuaja. Më pëlqen shumë citati i Dick Gindon: "Kur shkruani, natyra ju tregon se sa kaq e pavendosur është mendja juaj". Nëse nuk shkruani, ju duket vetëm se po mendoni. Dhe mendimet tuaja duhet të regjistrohen në formën e specifikimeve.
Specifikimet kryejnë shumë funksione, sidomos në projektet e mëdha. Por do të flas vetëm për një prej tyre: ato na ndihmojnë të mendojmë qartë. Të menduarit 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 është gjithmonë pyetja e parë për programuesit: në cilin gjuhë do të shkruajmë. Nuk ka një përgjigje të saktë për këtë: problemet që zgjidhim janë shumë të larmishme. Për disa është i dobishëm TLA+ — një gjuhë specifikimesh që e kam zhvilluar unë. Për të tjerët është më e lehtë të përdorin mandarin. Çdo gjë varet nga situata.
Një pyetje më e rëndësishme është: Si mund të arrijmë një mendim më të qartë? Përgjigja: Ne duhet të mendojmë si shkencëtarë. Ky është një mënyrë mendimi që ka treguar rezultate të shkëlqyera gjatë 500 viteve të fundit. Në shkencë, ne ndërtuam modele matematike të realitetit. Astronomia ka qenë ndoshta shkenca e parë në sensin e vërtetë të këtij termi. Në modelin matematik të përdorur në astronomi, trupat qiellor paraqiten si pika me masë, pozicion dhe impuls, megjithëse në realitet ata janë objekte jashtëzakonisht komplekse me male dhe oqeane, ngritje dhe rënie të ujërave. Ky model, si çdo model tjetër, është krijuar për të zgjidhur probleme të caktuara. Ai është jashtëzakonisht i përshtatshëm për të përcaktuar se ku duhet drejtuar teleskopi nëse duhet të gjejmë një planet. Por nëse dëshironi të parashikoni motin në këtë planet, ky model nuk do të ishte i përshtatshëm.
Matematika na lejon të përcaktojmë pronat e modelit. Dhe shkenca tregon se si këto prona janë të lidhura me realitetin. Le të flasim për shkencën tonë, shkencën kompjuterike. Realiteti me të cilin punojmë janë sistemet llogaritëse të të gjitha llojeve: procesorët, konsolat e lojërave, kompjuterët që ekzekutojnë programe e kështu me radhë. Do të flas për ekzekutimin e një programi në kompjuter, por, në përgjithësi, të gjitha këto përfundime janë të aplikueshme për çdo sistem llogaritës. Në shkencën tonë ne përdorim shumë modele të ndryshme: makina Turing, grupe të pjesërisht të renditura të ngjarjeve dhe shumë të tjera.
Çfarë është një program? Kjo është çfarëdo kod që mund të merret si një tërësi e pavarur. Le të supozojmë se na nevojitet të shkruajmë një shfletues. Ne kryejmë tri detyra: projektimi i paraqitjes së programit për përdoruesin, pastaj shkruajmë një skemë të lartë të programit dhe, në fund, shkruajmë kodin. Në procesin e shkruarjes së kodit, ne kuptojmë se na duhet të shkruajmë një mjet për formatimin e tekstit. Këtu na duhen përsëri tri detyra: të përcaktojmë se çfarë teksti do të kthejë ky mjet; të zgjedhim një algoritëm për formatimin; të shkruajmë kodin. Kjo detyrë ka një nën detyrë: të vendosim saktësisht ndarësit në fjalë. Këtë nën detyrë ne gjithashtu e zgjidhim në tri hapa - siç e shohim, ato përsëriten në shumë nivele.
Të shqyrtojmë në detaje hapin e parë: çfarë problemi zgjidh programi. Këtu ne zakonisht modelojmë programin si një funksion, i cili merr disa të dhëna hyrëse dhe jep disa të dhëna në dalje. Në matematikë, funksioni zakonisht përshkruhet si një grup i renditur çiftesh. Për shembull, funksioni i ngritjes në katror për numrat natyrorë përshkruhet si grupi {, , , , …}. Dija e përcaktuar e këtij funksioni është grupi i elementeve të parë të çdo çifti, pra numrat natyrorë. Për të përcaktuar funksionin, na nevojitet të caktuar fushën e tij të përcaktuar dhe formulën.
Por funksionet në matematikë nuk janë të njëjta me funksionet në gjuhët e programimit. Matematika është shumë më e thjeshtë. Tani, për shkak se nuk kam kohë për shembuj të komplikuar, do të shqyrtojmë një të thjeshtë: një funksion në gjuhën C ose një metodë statike në Java që kthen gcd e dy numrave të plotë. Në specifikimin e kësaj metode do të shkruajmë: llogarit GCD(M,N) për argumentet M dhe Nindex GCD(M,N) — një funksion, ku fusha e tij e përcaktuar është grupi i çifteve të numrave të plotë, dhe vlera që kthen është numri më i madh të cilin e ndan M dhe N. Si lidhet kjo model me realitetin? Modeli operon me numra të plotë, ndërsa në C ose Java kemi një int32-bit. Ky model na lejon të përcaktojmë nëse algoritmi është i saktë përGCD
, por ai nuk do të parandajë gabimet e tejkalimit. Për këtë do të kishte nevojë për një model më kompleks, për të cilin nuk ka kohë. Të flasim për kufizimet e funksionit si model. Disa programe (për shembull, sistemet operative) nuk reduktohen vetëm në kthimin e një vlere 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ë: planifikimin e mënyrës se si të zgjidhet problemi. Radhitja e shpejtë dhe radhitja me flluska llogarisin të njëjtin funksion, por këto janë algorithma krejtësisht të ndryshëm. Prandaj, për të përshkruar mënyrën e arritjes së qëllimit të programit, unë përdor një model të ndryshëm, ta quajmë modelin standard të sjelljes. Programi në të është i paraqitur si një grup të gjitha sjelljeve të lejuara, secila e të cilave, nga ana e saj, është një sekuencë gjendjesh, dhe gjendja është caktimi i vlerave për variablat.
Le të shohim se si do të duket hapi i dytë për algoritmin e Euklidit. Na nevojitet të llogarisim GCD(M, N). Ne e inicializojmë M si x, ndërsa N si y, pastaj vazhdojmë të heqim vlerë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, ndërsa N = 18, mund të përshkruajmë këtë sjellje:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
E nëse M = 0 dhe N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Këtu duhet të bëjmë një shpjegim të vogël rreth produktivitetit. Ai shpesh matet në numrin e rreshtave të kodit të shkruar gjatë një dite. Por puna juaj është ndjeshëm më e dobishme nëse hiqni një numër të caktuar të rreshtave, sepse keni më pak hapësirë për të metat. Dhe heqja e kodit është më e lehtë pikërisht në hapat e parë. Është plotësisht e mundur që ndoshta nuk keni nevojë për të gjitha ato ndërlikime 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 duhen bërë. Hapi i dytë - në vendin e dytë për potencialin për kursim kohor. Nëse e matin produktivitetin në numrin e rreshtave të shkruara, atëherë mendimi për mënyrën e realizimit të detyrës do t'ju bëjë më pak produktivë, pasi do të mund të zgjidhni të njëjtën detyrë me një vëllim më të vogël kod. Nuk mund të jap një statistikë të saktë këtu, pasi nuk kam një mënyrë për të numëruar numrin e rreshtave që nuk shkrova për shkak se kalova kohë në specifikim, pra në hapat e parë dhe të dytë. Dhe këtu nuk mund të realizoj një eksperiment, sepse në eksperiment nuk kemi të drejtë të kryejmë hapin e parë, pasi detyrimi është përcaktuar më përpara.
Në specifikimet joformale është lehtë të injoroni shumë vështirësi. Nuk ka asgjë të komplikuar në shkrimin e specifikimeve strikte për funksionet, këtë nuk do ta diskutoj. Në vend të kësaj, do të flasim për shkrimin e specifikimeve strikte për modelet standarde të sjelljes. Ekziston një teoremë që thotë se çdo grup sjelljesh mund të përshkruhet me pronën e sigurisë (safety) dhe pronën e jetësisë (liveness). Siguria do të thotë se nuk do të ndodhi asgjë e keqe, programi nuk do të japë një përgjigje të gabuar. Qëndrueshmëria do të thotë se herët a vonë do të ndodhi diçka e mirë, pra, programi do të japë në fund një përgjigje të saktë. Në përgjithësi, siguria është një tregues më i rëndësishëm, gabimet ndodhin më shpesh pikërisht këtu. Prandaj, për të kursyer kohë, nuk do të flas për qëndrueshmërinë, edhe pse natyrisht ajo është gjithashtu e rëndësishme.
Ne arrijmë sigurinë duke shkruar, së pari, shumë mundësi të gjendjeve fillestare. Dhe, së dyti, lidhjet me të gjitha gjendjet pasuese të mundshme për çdo gjendje. Do të sillemi si shkencëtarë dhe do të përcaktojmë gjendjet matematikisht. Grupi i gjendjeve fillestare përshkruhet nga formula, 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. Lidhja me gjendjen pasuese përshkruhet nga formula, në të cilën variablat e gjendjes pasuese shkruhen me një të theksuar, dhe gjendja aktuale pa të theksuar. Në rastin e algoritmit të Euclidit do të kemi të bëjmë me një disjunkcion të dy formulave, në njërën prej të cilave x është vlera maksimale, dhe në tjetrën — y:
Në rastin e parë, vlera e re y është e barabartë me vlerën e mëparshme y, dhe vlera e re x e marrim duke i zbritur variablën më të vogël nga variabli më i madh. Në rastin e dytë, ne veprojmë në të kundërt.
Le të kthehemi te algoritmi i Euclidit. Supozoni përsëri se M = 12, N = 18. Kjo përcakton një gjendje të vetme fillestare, (x = 12) ∧ (y = 18). Pastaj, ne zëvendësojmë këto vlera në formulën e mësipërme dhe marrim:
Këtu është zgjidhja e vetme e mundshme: x' = 18 - 12 ∧ y' = 12, dhe ne marrim 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ë dy pjesët e shprehjes do të jenë të gabuara, prandaj, nuk ka gjendje pasuese për të. Pra, ne kemi një specifikim të plotë të hapi të dytë — siç e shohim, kjo është plotësisht matematikë e zakonshme, siç e bëjnë inxhinierët dhe shkencëtarët, dhe jo diçka e çuditshme, si në informatikë.
Këto dy formula mund të bashkohen në një formulë të logjikës temporale. Ajo është elegante dhe e lehtë për t'u shpjeguar, por nuk ka kohë për të tani. Logjika temporale mund të na nevojitet vetëm për pronësinë e gjallërisë, për sigurinë nuk është e nevojshme. Logjika temporale si një hapësirë vetë nuk është tërheqëse, nuk është matematikë krejt e zakonshme, por në rastin e gjallërisë ajo është një e keqe e 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ë i determinist. Për të modeluar një algoritëm të paedukatë, është e nevojshme që të gjendja aktuale të ketë disa gjendje të mundshme të ardhshme, dhe që çdo vlerë variabël pa vija të ketë disa vlera variabël me vija, për të cilat marrëdhënia me gjendjen e ardhshme është e vërtetë. Kjo nuk është e vështirë për t'u bërë, por tani nuk do të jap shembuj.
Për të krijuar një mjet funksional, është e nevojshme një matematikë formale. Si ta bëjmë specifikimin formal? Për këtë na nevojitet një gjuhë formale, për shembull, . Specifikimi i algoritmit të Euclidit do të duket kështu në këtë gjuhë:
Simboli i shenjës së barazisë me trekëndëshin tregon se vlera në anën e majtë të shenjës përcaktohet si e barabartë me vlerën në anën e djathtë. Në thelb, specifikimi është një definim, në rastin tonë dy definime. Për specifikimin në TLA+ duhen shtuar shpallje dhe disa sintaksë, si në slajdin lart. Në ASCII, kjo do të dukej kështu:
Siç shohim, nuk ka asgjë të komplikuar. Specifikimi në TLA+ mund të verifikohet, dmth të kalojë përmes të gjitha sjelljeve të mundshme në një model të vogël. Në rastin tonë, ky model do të jetë vlerat e caktuara M dhe N. Kjo është një mënyrë shumë efikase dhe e thjeshtë për verifikim, e cila realizohet krejtësisht automatikisht. Për më tepër, është e mundur të shkruhen prova formale të vërtetësisë dhe t'i verifikohet ato në mënyrë mekanike, por për këtë nevojitet shumë kohë, prandaj askush nuk e bën këtë pothuajse.
Dobësia kryesore e TLA+ është se është matematikë, dhe programuesit dhe shkencëtarët kompjuterik frikosen nga matematika. Në shikim të parë kjo tingëllon si një shaka, por, fatkeqësisht, e them këtë me çdo seriozitet. Kolegu im sapo më tregoi se si përpiqej të shpjegonte TLA+ disa zhvilluesve. Sa herë që formula shfaqej në ekran, ata menjëherë merrnin një shprehje të ngurtë. Prandaj, nëse TLA+ është frikësues, mund të përdorim , një lloj gjuhe programimi loje. Një shprehje në PlusCal mund të jetë çdo shprehje TLA+, pra, në thelb, çdo shprehje matematike. Për më tepër, PlusCal ka sintaksë për algoritma ndërlikuese. Falë faktit se në PlusCal mund të shkruhet çdo shprehje TLA+, ai është në mënyrë të konsiderueshme më ekspresiv se çdo gjuhë reale programimi. Më tej, PlusCal kompilohet në një specifikim të lehtë për t'u lexuar të TLA+. Kjo nuk do të thotë, sigurisht, se një specifikim i ndërlikuar i PlusCal do të shndërrohet në një të thjeshtë në TLA+ — thjesht lidhja ndërmjet tyre është e qartë, nuk do të ketë kompleksitet shtesë. Së fundi, ky specifikim mund të verifikohet nga veglat e TLA+. Në përgjithësi, PlusCal mund të ndihmojë në kalimin përmes frikës nga matematika, është e lehtë për tu kuptuar madje edhe për programuesit dhe shkencëtarët kompjuterikë. Në të kaluarën, unë kam publikuar për rreth 10 vjet algoritme në të.
Ndoshta dikush do të argumentonte se TLA+ dhe PlusCal janë matematikë, dhe matematika funksionon vetëm në shembuj të shpikur. Në praktikë, nevojitet një gjuhë reale me lloje, procedura, objekte dhe kështu me radhë. Kjo nuk është e vërtetë. Ky është mendimi i Kris Newcomb, i cili ka punuar në Amazon: «Ne e përdorëm TLA+ në dhjetë projekte të mëdha, dhe në çdo rast përdorimi i saj kontribuoi në zhvillim, sepse arritëm të identifikonim defekte të rrezikshme para se të shkonin në prodhim, dhe sepse na dha kuptim dhe besim të nevojshëm për optimizime agresive të performancës, pa ndikuar në vërtetësinë e programit». Shpesh mund të dëgjojmë se duke përdorur metoda formale, ne marrim kod joefikas — në praktikë, ndodhet e kundërta. Për më tepër, ekziston një mendim se menaxherët është e pamundur t'i bindësh për nevojën e metodave formale, edhe nëse programuesit besojnë në dobishmërinë e tyre. Dhe Newcomb shkruan: «Menaxherët tani e inkurajojnë gjithmonë të shkruhen specifikimet për TLA+, dhe veçanërisht caktuan kohë për këtë». Pra, kur menaxherët shohin që TLA+ funksionon, ata e pranojnë me kënaqësi. Kris Newcomb e shkroi këtë rreth gjashtë muaj më parë (në tetor 2014), tani, sa di unë, TLA+ përdoret në 14 projekte, jo 10. Një shembull tjetër ka të bëjë me projektimin e XBox 360. Një praktikant iu afrua Charles Taker dhe shkroi një specifikim për sistemin e memories. Falë këtij specifikimi u gjet një gabim, i cili ndryshe do të kalonte pa u vënë re, dhe për shkak të të cilit çdo XBox 360 do të binte pas katër orësh përdorimi. Inxhinierët e IBM e konfirmuan se testet e tyre nuk do ta kishin zbuluar këtë gabim.
Më shumë për TLA+ mund të lexoni në internet, por tani le të flasim për specifikimet informale. Rrallë na duhet të shkruajmë programe që llogarisin gjinë më të madhe të zakonshme dhe gjëra të ngjashme. Shumë më shpesh ne shkruajmë programe si instrumentin e printimit strukturor (pretty-printer), që e shkrova për TLA+. Pas përpunimit më të thjeshtë, kodi në TLA+ do të dukej kështu:
Por në shembullin e dhënë, përdoruesi me siguri do të donte që shenjat e konjuksionit dhe të barazimit të ishin të rregulluara. Kështu që formatimi i duhur do të dukej kështu:
Le të shqyrtojmë një shembull tjetër:
Këtu, përkundrazi, rregullimi i shenjave të barazimit, shtesës dhe shumëzimit në burim ishte rastësor, prandaj përpunimi më i thjeshtë është mjaft i përshtatshëm. Në thelb, nuk ka një përkufizim matematikor të saktë për formatimin e saktë, 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, nëse nuk kemi një përcaktim të vërtetësisë, specifikimi është i pafryt. Por nuk është kështu. Nëse nuk e dimë se çfarë duhet të bëjë programi, kjo nuk do të thotë se nuk duhet të mendojmë mbi funksionin e tij — përkundrazi, ne duhet të shpenzojmë më shumë përpjekje për këtë. Specifikimi është veçanërisht i rëndësishëm këtu. Të përcaktosh programin optimal për printimin struktural është e pamundur, por kjo nuk do të thotë se nuk duhet ta provojmë fare; të shkruash kod si një rrjedhë mendimi — kjo nuk është e pranueshme. Në fund, shkrova një specifikim me gjashtë rregulla me përkufizime në formën e komenteve në skedarin Java. Këtu është një shembull i njërit nga rregullat: një token komenti të majtë është LeftComment i rreshtuar me tokenin e tij mbulues. Ky rregull është shkruar në, le të themi, anglishten matematikore: LeftComment i rreshtuar, koment i majtë dhe token mbulues — terma me përdefinitione. Kjo është mënyra se si matematicienët përshkruajnë matematikën: shkruajnë përcaktime të terma dhe mbi ato — rregullat. Përdorimi i tillë i specifikimit është që të kuptohet dhe të rregullohen gjashtë rregulla është ndjeshëm më e lehtë se 850 rreshta kodi. Duhet thënë se shk writing këto rregulla nuk ishte e lehtë; kaloi shumë kohë për t'i testuar ato. Veçanërisht për këtë qëllim shkrova një kod që raportonte se cili rregull po përdorej. Falë faktit që testova këto gjashtë rregulla në disa shembuj, nuk kisha nevojë të rregulloja 850 rreshta kodi dhe gabimet u gjetën mjaft lehtë. Në Java ka mjete të shkëlqyera për këtë. Nëse do të kisha shkruar thjesht kod, do të ishte nevojitur shumë më tepër kohë, dhe formati do të kishte qenë i dobët.
Pse nuk mund të përdorej një specifikim formal? Nga njëra anë, saktësia e zbatimit nuk është shumë e rëndësishme këtu. Printimi strukturore do të ketë ndonjëherë dikë që nuk do të kënaqet, kështu që nuk kisha nevojë të arrija saktësinë në të gjitha situatat jostandarde. Është edhe më e rëndësishme që nuk kisha mjete adekuate. Një mjet për verifikimin e modeleve TLA+ është i padobishëm këtu, kështu që do të kisha shkruar manualisht shembuj.
Specifikimi i dhënë ka karakteristika që janë të përbashkëta për të gjitha specifikimet. Ai është në një nivel më të lartë se kodi. Mund të zbatohet në çdo gjuhë. Përdorimi i ndonjë mjeti ose metode është i padobishëm për ta shkruar atë. Asnjë kurs programimi nuk do t'ju ndihmojë të shkruani këtë specifikim. Dhe nuk ka mjete që mund ta bënin këtë specifikim të panevojshëm, përveç gjithsesi, nëse nuk po shkruani një gjuhë specifike përshkrimi për shkruajtjen e programeve të strukturuara me TLA+. Në fund, ky specifikim nuk thotë asgjë se si do ta shkruajmë kodin, ai thjesht tregon se çfarë bën ky kod. Ne shkruajmë specifikimin për të ndihmuar mendimin tonë për problemin, përpara se të fillojmë të mendojmë për kodin.
Por ky specifikim ka 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:
Më tej, kjo specifikim është një grup rregullash. Si rregull, kjo është një shenjë e specifikimit të dobët. Të kuptosh pasojat e një grupi rregullash është mjaft e vështirë, dhe 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 ndonjë mënyrë më të mirë.
Vlen të thuhet disa fjalë për programet që funksionojnë vazhdimisht. Si rregull, ato punojnë paralelisht, për shembull, sistemet operative ose sistemet e shpërndara. Vetëm shumë pak njerëz mund të kuptojnë ato në mendje ose në letër, dhe unë nuk i përkas atyre, ndonëse dikur më ishte e mundur. Prandaj janë të nevojshme mjete që do të kontrollojnë punën tonë — për shembull, TLA+ ose PlusCal.
Pse duhej të shkruaja një specifikim, nëse unë tashmë e dija se çfarë duhej të bënte kodi? Në të vërtetë, më dukej se tregohesha se e di. Për më tepër, me praninë e specifikimit, një person i jashtëm nuk ka nevojë të hyjë në kod për të kuptuar se çfarë bën ai. Kam një rregull: nuk duhet të ketë rregulla të përgjithshme. Ky rregull, sigurisht, ka përjashtimin e tij, ky është rregulli i vetëm i përgjithshëm që ndjek: specifikimi i asaj që bën kodi duhet t’u tregojë njerëzve gjithçka që ata duhet të dinë kur përdorin këtë kod.
Pra ndaj, çfarë duhet të dijë një programues rreth mënyrës së të menduarit? Së pari, e njëjta gjë si të gjithë të tjerët: nëse nuk shkruan, thjesht të duket se po mendon. Përveç kësaj, duhet të mendosh para se të kodosh, dhe kjo do të thotë se duhet të shkruash para se të kodosh. Specifikimi është ajo që ne shkruajmë para se të fillojmë të kodojmë. 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
Si të lidhni specifikimin me kodin? Me anë të komenteve, të cilat lidhin konceptet matematikore me realizimin e tyre. Nëse punoni me grafe, atëherë në nivelin e programit do të keni masa të nyjeve dhe masa të lidhjeve. Prandaj, duhet të shkruani se si saktësisht grafiku realizohet me këto struktura programimi.
Duhet të theksohet se asgjë nga kjo e thënë nuk i përket procesit të shkruarjes së kodit. Kur shkruani kod, që do të thotë se po kryeni hapin e tretë, duhet gjithashtu të mendoni dhe të planifikoni programin. Nëse një nënpërgjegjësi rezulton të jetë e vështirë ose e pacaktuar, duhet të shkruani një specifikim për të. Por për kodin e vet nuk po flas këtu. Mund të përdorni çdo gjuhë programimi, çdo metodologji, nuk është fjala për to. Për më tepër, asgjë nga kjo e thënë nuk e shtyn nevojën për të testuar dhe debuguar kodin. Edhe nëse modeli abstrakt është shkruar saktësisht, mund të ketë bug-e në realizimin e tij.
Shkrimi i specifikimeve është një hap shtesë në procesin e shkruarjes së kodit. Falë kësaj, shumë gabime mund të kapen me përpjekje më të vogla — e dimë këtë nga përvoja e programuesve në Amazon. Me specifikime, cilësia e skedave bëhet më e lartë. Pra, pse atëherë shpesh i kalojmë ato? Sepse është e vështirë të shkruajmë. Dhe është e vështirë të shkruash, sepse për këtë duhet të mendosh, dhe mendimi gjithashtu është i vështirë. Gjithmonë është më e lehtë të bësh si sikur mendon. Këtu mund të bëhet një analogji me vrapimin — sa më pak të vraponi, aq më ngadalë vraponi. Duhet të stërvitni muskujt tuaj dhe të ushtroni shkrimin. Kërkohet praktikë.
Specifikimi mund të jetë i gabuar. Ju mund të keni bërë një gabim diku, ose kërkesat mund të jenë ndryshuar, ose mund të jetë e nevojshme të bëni përmirësime. Çdo kod që përdor dikush duhet të modifikohet, kështu që më në fund specifikimi do të ndahet nga programi. Në mënyrë ideale, në këtë rast duhet të shkruani një specifikim të ri dhe të rishkruani plotësisht kodin. Ne e dimë mirë se askush nuk e bën këtë. Në praktikë, ne e patch-ojmë kodin dhe ndoshta përditësojmë specifikimin. Nëse kjo ndodh patjetër në një moment, atëherë përse duhet të shkruajmë specifikime? Së pari, për personin që do të modifikojë kodin tuaj, çdo fjalë e tepërt në specifikim do të jetë shumë e vlefshme, dhe ky person mund të jeni vetë ju. Unë shpesh e kritikoj veten për specifikimin e pamjaftueshëm kur rregullojnë kodin tim. Unë shkruaj më shumë specifikime se sa kod. Prandaj, kur rregulloni kodin, specifikimin gjithmonë duhet ta përditësoni. Së dyti, me çdo rregullim kodi bëhet më i keq, ai bëhet gjithnjë e më i vështirë për t'u lexuar dhe për tu mbështetur. Kjo është një rritje e entropisë. Por nëse nuk filloni me specifikimin, atëherë çdo rresht i shkruar do të jetë një rregullim, dhe kodi që në fillim do të jetë i ngarkuar dhe i vështirë për t'u lexuar.
Siç thoshte , asnjë luftë nuk është fituar sipas planit, dhe asnjë luftë nuk është fituar pa plan. Ai dinte diçka për luftime. Ka një mendim që shkruajtja e specifikimeve është një humbje kohe. Ndonjëherë kjo është e vërtetë, dhe detyra është aq e thjeshtë saqë nuk ka nevojë për mendim. Por gjithmonë duhet të mbani mend se, kur ju këshillohet të mos shkruani specifikime, kjo do të thotë se ju këshillohet të mos mendoni. Dhe për këtë duhet të mendoni çdoherë. Mendimi mbi detyrën nuk garanton se nuk do të bëni gabime. Siç e dimë, askush nuk ka shpikur një magji, dhe programimi është një punë e komplikuar. Por nëse nuk e mendoni detyrën, garantoni që do të bëni gabime.
Për më shumë rreth TLA+ dhe PlusCal mund të lexoni në faqen speciale, mund të hyni nga faqja ime e shtëpisë . Këtu përfundon, faleminderit për vëmendjen.
Ju kujtoj se ky është një përkthim. Kur të shkruani komente, mbani në mend se autori nuk do t'i lexojë. Nëse vërtet dëshironi të komunikoni me autorin, ai do të jetë në konferencën Hydra 2019, e cila do të mbahet më 11-12 korrik 2019 në Shën Petersburg. Biletet mund të blihen. .
Burimi: habr.com
