Ky artikull është një përkthim . Por para saj një prezantim i vogël. Si formohen zombitë? Të gjithë u futën në një situatë ku duan të tërheqin një mik ose koleg në nivelin e tyre, por nuk funksionon. Dhe nuk është aq shumë me ju sesa me të që "nuk funksionon": në njërën anë të peshores është një pagë normale, detyra etj., dhe nga ana tjetër, nevoja për të menduar. Të menduarit është i pakëndshëm dhe i dhimbshëm. Ai shpejt heq dorë dhe vazhdon të shkruajë kode pa e ndezur fare trurin. Ju imagjinoni se sa përpjekje duhet për të kapërcyer pengesën e pafuqisë së mësuar, dhe thjesht nuk e bëni atë. Kështu formohen zombitë, të cilat duket se mund të kurohen, por duket se askush nuk do ta bëjë.
Kur e pashë atë (po, i njëjti shok nga tekstet shkollore) dhe nuk bën raport, por pyetje-përgjigje, isha pak i kujdesshëm. Për çdo rast, Leslie është një shkencëtar me famë botërore, autor i veprave themelore në llogaritjen e shpërndarë, dhe ju mund ta njihni atë edhe me shkronjat La në fjalën LaTeX - "Lamport TeX". Faktori i dytë alarmues është kërkesa e tij: kushdo që vjen duhet (absolutisht pa pagesë) të dëgjojë paraprakisht disa nga raportet e tij, të bëjë të paktën një pyetje për to dhe vetëm atëherë të vijë. Vendosa të shikoja se çfarë transmetonte Lamport atje - dhe është e mrekullueshme! Është pikërisht ajo gjë, pilula magjike e lidhjes për të kuruar zombitë. Ju paralajmëroj: nga teksti, adhuruesit e metodologjive super fleksibël dhe ata që nuk u pëlqen të testojnë atë që shkruhet, mund të digjen dukshëm.
Pas habrokatit, në fakt, fillon përkthimi i seminarit. Shijojeni leximin!
Çfarëdo detyre që merrni përsipër, gjithmonë duhet të kaloni nëpër tre hapa:
- vendosni se çfarë qëllimi dëshironi të arrini;
- vendosni se si do ta arrini qëllimin tuaj;
- ejani në qëllimin tuaj.
Kjo vlen edhe për programimin. Kur shkruajmë kodin, duhet të:
- vendosni se çfarë duhet të bëjë programi;
- të përcaktojë se si duhet të kryejë detyrën e tij;
- shkruani kodin përkatës.
Hapi i fundit, natyrisht, është shumë i rëndësishëm, por nuk do të flas për të sot. Në vend të kësaj, ne do të diskutojmë dy të parat. Çdo programues i kryen ato përpara se të fillojë të punojë. Ju nuk uleni për të shkruar nëse nuk keni vendosur nëse jeni duke shkruar një shfletues ose një bazë të dhënash. Duhet të jetë e pranishme një ide e caktuar e qëllimit. Dhe ju patjetër mendoni se çfarë saktësisht do të bëjë programi dhe mos shkruani disi me shpresën se kodi do të kthehet disi në një shfletues.
Si ndodh saktësisht ky paramendim i kodit? Sa përpjekje duhet të bëjmë për këtë? E gjitha varet nga sa kompleks është problemi që po zgjidhim. Supozoni se duam të shkruajmë një sistem të shpërndarë me tolerancë ndaj gabimeve. Në këtë rast, ne duhet t'i mendojmë gjërat me kujdes përpara se të ulemi për të koduar. Po sikur të na duhet thjesht të rrisim një ndryshore numër të plotë me 1? Në pamje të parë, gjithçka është e parëndësishme këtu dhe nuk nevojitet asnjë mendim, por më pas kujtojmë se mund të ndodhë një tejmbushje. Prandaj, edhe për të kuptuar nëse një problem është i thjeshtë apo kompleks, së pari duhet të mendoni.
Nëse mendoni për zgjidhjet e mundshme të problemit paraprakisht, mund të shmangni gabimet. Por kjo kërkon që mendimi juaj të jetë i qartë. Për ta arritur këtë, duhet të shkruani mendimet tuaja. Më pëlqen shumë thënia e Dick Guindon: "Kur shkruani, natyra të tregon se sa i ngathët është të menduarit". Nëse nuk shkruani, ju vetëm mendoni se jeni duke menduar. Dhe ju duhet të shkruani mendimet tuaja në formën e specifikimeve.
Specifikimet kryejnë shumë funksione, veçanërisht në projekte të mëdha. Por unë do të flas vetëm për njërën prej tyre: ato na ndihmojnë të mendojmë qartë. Të mendosh qartë është shumë e rëndësishme dhe mjaft e vështirë, ndaj këtu kemi nevojë për ndonjë ndihmë. Në cilën gjuhë duhet të shkruajmë specifikimet? Në përgjithësi, kjo është gjithmonë pyetja e parë për programuesit: në cilën gjuhë do të shkruajmë. Nuk ka asnjë përgjigje të saktë për të: problemet që ne po zgjidhim janë shumë të ndryshme. Për disa, TLA+ është një gjuhë specifikimi që kam zhvilluar. Për të tjerët, është më i përshtatshëm për të përdorur kinezisht. Gjithçka varet nga situata.
Më e rëndësishme është një pyetje tjetër: si të arrihet një mendim më i qartë? Përgjigje: Ne duhet të mendojmë si shkencëtarë. Kjo është një mënyrë e të menduarit që e ka provuar veten gjatë 500 viteve të fundit. Në shkencë, ne ndërtojmë modele matematikore të realitetit. Astronomia ishte ndoshta shkenca e parë në kuptimin e ngushtë të fjalës. Në modelin matematikor të përdorur në astronomi, trupat qiellorë shfaqen si pika me masë, pozicion dhe vrull, megjithëse në realitet ato janë objekte jashtëzakonisht komplekse me male dhe oqeane, baticë dhe baticë. Ky model, si çdo tjetër, u krijua për të zgjidhur probleme të caktuara. Është e shkëlqyeshme për të përcaktuar se ku ta drejtoni teleskopin nëse keni nevojë të gjeni një planet. Por nëse doni të parashikoni motin në këtë planet, ky model nuk do të funksionojë.
Matematika na lejon të përcaktojmë vetitë e modelit. Dhe shkenca tregon se si këto veti lidhen me realitetin. Le të flasim për shkencën tonë, shkencën kompjuterike. Realiteti me të cilin ne punojmë është sisteme informatike të llojeve të ndryshme: procesorë, konzolla lojërash, kompjuterë, programe ekzekutuese, etj. Unë do të flas për ekzekutimin e një programi në një kompjuter, por në përgjithësi, të gjitha këto përfundime vlejnë për çdo sistem kompjuterik. Në shkencën tonë, ne përdorim shumë modele të ndryshme: makinën Turing, grupe ngjarjesh të renditura pjesërisht dhe shumë të tjera.
Çfarë është një program? Ky është çdo kod që mund të konsiderohet në mënyrë të pavarur. Supozoni se duhet të shkruajmë një shfletues. Ne kryejmë tre detyra: dizajnojmë pamjen e përdoruesit të programit, më pas shkruajmë diagramin e nivelit të lartë të programit dhe në fund shkruajmë kodin. Ndërsa shkruajmë kodin, kuptojmë se duhet të shkruajmë një formatues teksti. Këtu përsëri duhet të zgjidhim tre probleme: të përcaktojmë se çfarë teksti do të kthejë ky mjet; zgjidhni një algoritëm për formatim; shkruani kodin. Kjo detyrë ka nëndetyrën e saj: futni saktë një vizë në fjalë. Ne gjithashtu e zgjidhim këtë nëndetyrë në tre hapa - siç mund ta shihni, ato përsëriten në shumë nivele.
Le të shqyrtojmë më në detaje hapin e parë: çfarë problemi zgjidh programi. Këtu, ne më së shpeshti modelojmë një program si një funksion që merr disa hyrje dhe prodhon disa dalje. Në matematikë, një funksion zakonisht përshkruhet si një grup çiftesh të renditura. Për shembull, funksioni katror për numrat natyrorë përshkruhet si bashkësia {<0,0>, <1,1>, <2,4>, <3,9>, …}. Fusha e një funksioni të tillë është bashkësia e elementeve të parë të çdo çifti, domethënë numrat natyrorë. Për të përcaktuar një funksion, ne duhet të specifikojmë qëllimin dhe formulën e tij.
Por funksionet në matematikë nuk janë të njëjta me funksionet në gjuhët e programimit. Matematika është shumë më e lehtë. Meqenëse nuk kam kohë për shembuj kompleksë, le të shqyrtojmë një të thjeshtë: një funksion në C ose një metodë statike në Java që kthen pjesëtuesin më të madh të përbashkët të dy numrave të plotë. Në specifikimin e kësaj metode do të shkruajmë: llogarit GCD(M,N) për argumente M и NKu GCD(M,N) - një funksion domeni i të cilit është bashkësia e çifteve të numrave të plotë dhe vlera e kthimit është numri i plotë më i madh që pjesëtohet me M и N. Si lidhet ky model me realitetin? Modeli funksionon në numra të plotë, ndërsa në C ose Java kemi një 32-bit int. Ky model na lejon të vendosim nëse algoritmi është i saktë GCD, por nuk do të parandalojë gabimet e tejmbushjes. Kjo do të kërkonte një model më kompleks, për të cilin nuk ka kohë.
Le të flasim për kufizimet e një funksioni si model. Disa programe (të tilla si sistemet operative) jo vetëm që kthejnë një vlerë të caktuar për argumente të caktuara, ato mund të funksionojnë vazhdimisht. Për më tepër, funksioni si model nuk është i përshtatshëm për hapin e dytë: planifikimin se si të zgjidhet problemi. Renditja e shpejtë dhe renditja me flluskë llogaritin të njëjtin funksion, por ato janë algoritme krejtësisht të ndryshme. Prandaj, për të përshkruar se si arrihet qëllimi i programit, unë përdor një model tjetër, le ta quajmë atë modeli standard i sjelljes. Programi në të përfaqësohet si një grup i të gjitha sjelljeve të lejueshme, secila prej të cilave, nga ana tjetër, është një sekuencë gjendjesh, dhe gjendja është caktimi i vlerave për ndryshoret.
Le të shohim se si do të dukej hapi i dytë për algoritmin e Euklidit. Duhet të llogarisim GCD(M, N). Ne inicializojmë M si xDhe N si y, pastaj zbritni në mënyrë të përsëritur më të voglin e këtyre variablave nga më i madhi derisa të jenë të barabarta. Për shembull, nëse M = 12Dhe N = 18, mund të përshkruajmë sjelljen e mëposhtme:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Dhe nëse M = 0 и N = 0? Zero është i pjesëtueshëm me të gjithë numrat, kështu që nuk ka pjesëtues më të madh në këtë rast. Në këtë situatë, ne duhet të kthehemi në hapin e parë dhe të pyesim: a duhet vërtet të llogarisim GCD për numrat jo pozitivë? Nëse kjo nuk është e nevojshme, atëherë thjesht duhet të ndryshoni specifikimet.
Këtu duhet të bëjmë një digresion të vogël për produktivitetin. Shpesh matet në numrin e rreshtave të kodit të shkruar në ditë. Por puna juaj është shumë më e dobishme nëse hiqni qafe një numër të caktuar rreshtash, sepse keni më pak vend për defekte. Dhe mënyra më e lehtë për të hequr qafe kodin është në hapin e parë. Është plotësisht e mundur që thjesht të mos keni nevojë për të gjitha këmbanat dhe bilbilat që po përpiqeni të zbatoni. Mënyra më e shpejtë për të thjeshtuar një program dhe për të kursyer kohë është të mos bëni gjëra që nuk duhen bërë. Hapi i dytë është potenciali i dytë që kursen kohë. Nëse e matni produktivitetin në terma të rreshtave të shkruar, atëherë do t'ju bëjë të mendoni se si të përmbushni një detyrë më pak produktive, sepse mund ta zgjidhni të njëjtin problem me më pak kod. Nuk mund të jap statistika të sakta këtu, sepse nuk kam asnjë mënyrë për të numëruar numrin e rreshtave që nuk kam shkruar për faktin se kalova kohë në specifikimin, domethënë në hapin e parë dhe të dytë. Dhe eksperimenti nuk mund të vendoset as këtu, sepse në eksperiment nuk kemi të drejtë të kryejmë hapin e parë, detyra është e paracaktuar.
Është e lehtë të anashkalohen shumë vështirësi në specifikimet joformale. Nuk ka asgjë të vështirë për të shkruar specifikime strikte për funksionet, unë nuk do ta diskutoj këtë. Në vend të kësaj, ne do të flasim për shkrimin e specifikimeve të forta për sjelljet standarde. Ekziston një teoremë që thotë se çdo grup sjelljesh mund të përshkruhet duke përdorur veçorinë e sigurisë (siguria) dhe vetitë e mbijetesës (gjallëria). Siguria do të thotë që asgjë e keqe nuk do të ndodhë, programi nuk do të japë një përgjigje të pasaktë. Mbijetueshmëria do të thotë që herët a vonë diçka e mirë do të ndodhë, pra programi do të japë përgjigjen e saktë herët a vonë. Si rregull, siguria është një tregues më i rëndësishëm, gabimet më shpesh ndodhin këtu. Prandaj, për të kursyer kohë, nuk do të flas për mbijetesën, megjithëse është, natyrisht, gjithashtu e rëndësishme.
Ne e arrijmë sigurinë duke përshkruar, së pari, grupin e gjendjeve fillestare të mundshme. Dhe së dyti, marrëdhëniet me të gjitha shtetet e mundshme të ardhshme për secilin shtet. Le të veprojmë si shkencëtarë dhe të përcaktojmë gjendjet matematikisht. Grupi i gjendjeve fillestare përshkruhet me një formulë, për shembull, në rastin e algoritmit Euklidi: (x = M) ∧ (y = N). Për vlera të caktuara M и N ka vetëm një gjendje fillestare. Marrëdhënia me gjendjen e ardhshme përshkruhet me një formulë në të cilën variablat e gjendjes së ardhshme shkruhen me një të thjeshtë, dhe variablat e gjendjes aktuale shkruhen pa një të thjeshtë. Në rastin e algoritmit të Euklidit, do të merremi me ndarjen e dy formulave, në njërën prej të cilave x është vlera më e madhe, dhe në të dytën - y:
Në rastin e parë, vlera e re e y është e barabartë me vlerën e mëparshme të y, dhe ne marrim vlerën e re të x duke zbritur variablin më të vogël nga ajo më e madhe. Në rastin e dytë, ne bëjmë të kundërtën.
Le të kthehemi te algoritmi i Euklidit. Le të supozojmë përsëri se M = 12, N = 18. Kjo përcakton një gjendje të vetme fillestare, (x = 12) ∧ (y = 18). Më pas i lidhim ato vlera në formulën e mësipërme dhe marrim:
Këtu është e vetmja zgjidhje e mundshme: x' = 18 - 12 ∧ y' = 12dhe marrim sjelljen: [x = 12, y = 18]. Në mënyrë të ngjashme, 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, pra nuk ka gjendje tjetër. Pra, ne kemi një specifikim të plotë të hapit të dytë - siç mund ta shihni, kjo është matematikë krejt e zakonshme, si te inxhinierët dhe shkencëtarët, dhe jo e çuditshme, si në shkencat kompjuterike.
Këto dy formula mund të kombinohen në një formulë të logjikës kohore. Ajo është elegante dhe e lehtë për t'u shpjeguar, por nuk ka kohë për të tani. Mund të na duhet logjika kohore vetëm për pronën e gjallërisë, nuk është e nevojshme për sigurinë. Nuk më pëlqen logjika kohore si e tillë, nuk është matematikë krejt e zakonshme, por në rastin e gjallërisë është një e keqe e domosdoshme.
Në algoritmin e Euklidit, për çdo vlerë x и y kanë vlera unike x' и y', të cilat e bëjnë të vërtetë lidhjen me gjendjen tjetër. Me fjalë të tjera, algoritmi i Euklidit është determinist. Për të modeluar një algoritëm jo-përcaktues, gjendja aktuale duhet të ketë gjendje të shumëfishta të mundshme në të ardhmen, dhe se çdo vlerë e variablit të paprekur ka vlera të shumëfishta të variablave të paracaktuara, të tilla që lidhja me gjendjen tjetër të jetë e vërtetë. Kjo është e lehtë për t'u bërë, por nuk do të jap shembuj tani.
Për të bërë një mjet pune, ju duhet matematikë formale. Si ta bëni specifikimin zyrtar? Për ta bërë këtë, na duhet një gjuhë zyrtare, për shembull, . Specifikimi i algoritmit të Euklidit do të dukej kështu në këtë gjuhë:
Një simbol i shenjës së barabartë me një trekëndësh do të thotë që vlera në të majtë të shenjës është përcaktuar të jetë e barabartë me vlerën në të djathtë të shenjës. Në thelb, specifikimi është një përkufizim, në rastin tonë dy përkufizime. Tek specifikimi në TLA+, duhet të shtoni deklarata dhe disa sintaksë, si në rrëshqitjen e mësipërme. Në ASCII do të duket kështu:
Siç mund ta shihni, asgjë e komplikuar. Specifikimi për TLA+ mund të testohet, d.m.th të anashkalojë të gjitha sjelljet e mundshme në një model të vogël. Në rastin tonë, ky model do të ketë vlera të caktuara M и N. Kjo është një metodë shumë efikase dhe e thjeshtë verifikimi që është plotësisht automatike. Është gjithashtu e mundur të shkruhen prova formale të së vërtetës dhe t'i kontrolloni ato mekanikisht, por kjo kërkon shumë kohë, kështu që pothuajse askush nuk e bën këtë.
Disavantazhi kryesor i TLA+ është se është matematikë, dhe programuesit dhe shkencëtarët e kompjuterave kanë frikë nga matematika. Në pamje të parë, kjo tingëllon si një shaka, por, për fat të keq, e kam parasysh me gjithë seriozitetin. Kolegu im thjesht po më tregonte se si u përpoq t'u shpjegonte TLA+ disa zhvilluesve. Sapo formulat u shfaqën në ekran, ato u bënë menjëherë sy të qelqtë. Pra, nëse TLA+ ju frikëson, mund ta përdorni , është një lloj gjuhe programimi lodër. Një shprehje në PlusCal mund të jetë çdo shprehje TLA+, domethënë, në përgjithësi, çdo shprehje matematikore. Përveç kësaj, PlusCal ka një sintaksë për algoritme jo-përcaktuese. Për shkak se PlusCal mund të shkruajë çdo shprehje TLA+, PlusCal është shumë më shprehës se çdo gjuhë programimi real. Më pas, PlusCal përpilohet në një specifikim TLA+ lehtësisht të lexueshëm. Kjo nuk do të thotë, natyrisht, që specifikimi kompleks PlusCal do të shndërrohet në një të thjeshtë në TLA + - thjesht korrespondenca midis tyre është e dukshme, nuk do të ketë kompleksitet shtesë. Së fundi, ky specifikim mund të verifikohet nga mjetet TLA+. Në përgjithësi, PlusCal mund të ndihmojë në kapërcimin e fobisë së matematikës dhe është i lehtë për t'u kuptuar edhe për programuesit dhe shkencëtarët e kompjuterave. Në të kaluarën, kam botuar algoritme mbi të për ca kohë (rreth 10 vjet).
Ndoshta dikush do të kundërshtojë që TLA + dhe PlusCal janë matematikë, dhe matematika funksionon vetëm në shembuj të shpikur. Në praktikë, ju duhet një gjuhë e vërtetë me lloje, procedura, objekte etj. Kjo eshte e gabuar. Ja çfarë shkruan Chris Newcomb, i cili ka punuar në Amazon: “Ne kemi përdorur TLA+ në dhjetë projekte të mëdha, dhe në secilin rast, përdorimi i tij ka bërë një ndryshim të rëndësishëm në zhvillim, sepse ne ishim në gjendje të kapnim defekte të rrezikshme përpara se të fillonim prodhimin dhe sepse na dha njohurinë dhe besimin që na nevojitej për të bëni optimizime agresive të performancës pa ndikuar në të vërtetën e programit". Shpesh mund të dëgjoni se kur përdorim metoda formale, marrim kod joefikas - në praktikë, gjithçka është saktësisht e kundërta. Për më tepër, ekziston një mendim se menaxherët nuk mund të binden për nevojën e metodave formale, edhe nëse programuesit janë të bindur për dobinë e tyre. Dhe Newcomb shkruan: "Menaxherët tani po bëjnë presion të madh për të shkruar specifikimet për TLA +, dhe në mënyrë specifike të ndajnë kohë për këtë". Pra, kur menaxherët shohin se TLA+ po funksionon, ata janë të lumtur ta pranojnë atë. Chris Newcomb e shkroi këtë rreth gjashtë muaj më parë (tetor 2014), por tani, me sa di unë, TLA+ përdoret në 14 projekte, jo në 10. Një shembull tjetër është në hartimin e XBox 360. Një praktikant erdhi te Charles Thacker dhe shkroi specifikimet për sistemin e memories. Falë këtij specifikimi, u gjet një gabim që përndryshe do të kalonte pa u vënë re, dhe për shkak të të cilit çdo XBox 360 do të rrëzohej pas katër orësh përdorimi. Inxhinierët e IBM konfirmuan se testet e tyre nuk do ta kishin gjetur këtë gabim.
Mund të lexoni më shumë rreth TLA + në internet, por tani le të flasim për specifikimet joformale. Rrallëherë duhet të shkruajmë programe që llogaritin pjesëtuesin më të vogël të përbashkët dhe të ngjashme. Shumë më shpesh ne shkruajmë programe si mjeti i printerit të bukur që kam shkruar për TLA+. Pas përpunimit më të thjeshtë, kodi TLA + do të duket kështu:
Por në shembullin e mësipërm, përdoruesi ka shumë të ngjarë të donte që lidhja dhe shenjat e barabarta të përputheshin. Pra, formatimi i saktë do të dukej më shumë si ky:
Shqyrtoni një shembull tjetër:
Këtu, përkundrazi, rreshtimi i shenjave të barazimit, shtimit dhe shumëzimit në burim ishte i rastësishëm, kështu që përpunimi më i thjeshtë është mjaft i mjaftueshëm. Në përgjithësi, nuk ka një përkufizim të saktë matematikor të formatimit të saktë, sepse "i saktë" në këtë rast do të thotë "ajo që përdoruesi dëshiron", dhe kjo nuk mund të përcaktohet matematikisht.
Duket se nëse nuk kemi një përkufizim të së vërtetës, atëherë specifikimi është i padobishëm. Por nuk është. Vetëm për shkak se ne nuk e dimë se çfarë duhet të bëjë një program nuk do të thotë se nuk kemi nevojë të mendojmë se si funksionon ai - përkundrazi, duhet të bëjmë edhe më shumë përpjekje për të. Specifikimi është veçanërisht i rëndësishëm këtu. Është e pamundur të përcaktohet programi optimal për printim të strukturuar, por kjo nuk do të thotë që nuk duhet ta marrim fare, dhe shkrimi i kodit si rrjedhë e vetëdijes nuk është gjë e mirë. Në fund, shkrova një specifikim prej gjashtë rregullash me përkufizime në formën e komenteve në një skedar java. Këtu është një shembull i një prej rregullave: a left-comment token is LeftComment aligned with its covering token. Ky rregull është shkruar, le të themi, në anglisht matematikore: LeftComment aligned, left-comment и covering token - terma me përkufizime. Kështu e përshkruajnë matematikanët matematikën: ata shkruajnë përkufizime të termave dhe, bazuar në to, rregulla. Përfitimi i një specifikimi të tillë është se gjashtë rregulla janë shumë më të lehta për t'u kuptuar dhe korrigjuar se sa 850 rreshta kodi. Duhet të them që shkrimi i këtyre rregullave nuk ishte i lehtë, u desh mjaft kohë për t'i korrigjuar ato. Sidomos për këtë qëllim, shkrova një kod që raportonte se cili rregull ishte përdorur. Falë faktit që i testova këto gjashtë rregulla në disa shembuj, nuk më duhej të korrigjoja 850 rreshta kodi dhe gabimet doli të ishin mjaft të lehta për t'u gjetur. Java ka mjete të shkëlqyera për këtë. Nëse sapo do të kisha shkruar kodin, do të më kishte marrë shumë më tepër kohë dhe formatimi do të ishte me cilësi më të dobët.
Pse nuk mund të përdoret një specifikim zyrtar? Nga njëra anë, ekzekutimi i saktë nuk është shumë i rëndësishëm këtu. Printimet strukturore nuk do t'i pëlqejnë askujt, kështu që nuk më duhej ta bëja të funksiononte siç duhet në të gjitha situatat e çuditshme. Akoma më i rëndësishëm është fakti që nuk kisha mjete adekuate. Kontrolluesi i modelit TLA+ është i padobishëm këtu, kështu që do të më duhej t'i shkruaja manualisht shembujt.
Specifikimi i mësipërm ka veçori të përbashkëta për të gjitha specifikimet. Është një nivel më i lartë se kodi. Mund të zbatohet në çdo gjuhë. Çdo mjet apo metodë është e padobishme 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ëjnë këtë specifikim të panevojshëm, përveç nëse, sigurisht, po shkruani një gjuhë posaçërisht për të shkruar programe të strukturuara të printimit në TLA+. Së fundi, ky specifikim nuk thotë asgjë se si do ta shkruajmë saktësisht kodin, ai vetëm tregon se çfarë bën ky kod. Ne shkruajmë specifikimet për të na ndihmuar të mendojmë për problemin përpara se të fillojmë të mendojmë për kodin.
Por ky specifikim ka edhe veçori që e dallojnë nga specifikimet e tjera. 95% e specifikimeve të tjera janë dukshëm më të shkurtra dhe më të thjeshta:
Më tej, ky specifikim është një grup rregullash. Si rregull, kjo është një shenjë e specifikimeve të dobëta. Kuptimi i pasojave të një sërë rregullash është mjaft i vështirë, prandaj më duhej të shpenzoja shumë kohë për t'i korrigjuar ato. Megjithatë, në këtë rast, nuk mund të gjeja një mënyrë më të mirë.
Vlen të thuash disa fjalë për programet që funksionojnë vazhdimisht. Si rregull, ato punojnë paralelisht, për shembull, sistemet operative ose sistemet e shpërndara. Shumë pak njerëz mund t'i kuptojnë mendërisht ose në letër, dhe unë nuk jam një prej tyre, megjithëse dikur kam mundur ta bëj këtë. Prandaj, na duhen mjete që do të kontrollojnë punën tonë - për shembull, TLA + ose PlusCal.
Pse ishte e nevojshme të shkruaja një specifikim nëse e dija se çfarë saktësisht duhet të bënte kodi? Në fakt, thjesht mendova se e dija. Për më tepër, me një specifikim, një i huaj nuk ka më nevojë të futet në kod për të kuptuar se çfarë saktësisht bën. Unë kam një rregull: nuk duhet të ketë rregulla të përgjithshme. Ekziston një përjashtim nga ky rregull, sigurisht, është i vetmi rregull i përgjithshëm që unë ndjek: specifikimi i asaj që bën kodi duhet t'u tregojë njerëzve gjithçka që duhet të dinë kur përdorin kodin.
Pra, çfarë saktësisht duhet të dinë programuesit për të menduarit? Si fillim, njësoj si gjithë të tjerët: nëse nuk shkruani, atëherë ju duket vetëm se po mendoni. Gjithashtu, duhet të mendoni përpara se të kodoni, që do të thotë se duhet të shkruani përpara se të kodoni. Specifikimi është ajo që shkruajmë përpara se të fillojmë të kodojmë. Një specifikim nevojitet për çdo kod që mund të përdoret ose modifikohet nga kushdo. Dhe ky “dikush” mund të jetë vetë autori i kodit një muaj pasi është shkruar. Një specifikim nevojitet për programe dhe sisteme të mëdha, për klasa, për metoda dhe ndonjëherë edhe për seksione komplekse të një metode të vetme. Çfarë saktësisht duhet të shkruhet për kodin? Ju duhet të përshkruani atë që bën, domethënë çfarë mund të jetë e dobishme për çdo person që përdor këtë kod. Ndonjëherë mund të jetë gjithashtu e nevojshme të specifikohet se si kodi e përmbush qëllimin e tij. Nëse e kemi kaluar këtë metodë në rrjedhën e algoritmeve, atëherë e quajmë atë një algoritëm. Nëse është diçka më e veçantë dhe e re, atëherë e quajmë dizajn të nivelit të lartë. Këtu nuk ka asnjë ndryshim formal: të dyja janë një model abstrakt i një programi.
Si saktësisht duhet të shkruani një specifikim kodi? Gjëja kryesore: duhet të jetë një nivel më i lartë se vetë kodi. Ai duhet të përshkruajë gjendjet dhe sjelljet. Duhet të jetë aq i rreptë sa kërkon detyra. Nëse jeni duke shkruar një specifikim se si do të zbatohet një detyrë, mund ta shkruani atë në pseudokod ose me PlusCal. Ju duhet të mësoni se si të shkruani specifikimet në specifikimet formale. Kjo do t'ju japë aftësitë e nevojshme që do t'ju ndihmojnë edhe me ato joformale. Si mësoni të shkruani specifikimet zyrtare? Kur mësuam të programonim, shkruanim programe dhe më pas i korrigjuam ato. Është e njëjta gjë këtu: shkruani specifikimet, kontrolloni atë me kontrolluesin e modelit dhe rregulloni gabimet. TLA+ mund të mos jetë gjuha më e mirë për një specifikim formal dhe një gjuhë tjetër ka të ngjarë të jetë më e mirë për nevojat tuaja specifike. Avantazhi i TLA+ është se mëson shumë mirë të menduarit matematik.
Si të lidhni specifikimet dhe kodin? Me ndihmën e komenteve që lidhin konceptet matematikore dhe zbatimin e tyre. Nëse punoni me grafikë, atëherë në nivel programi do të keni vargje nyjesh dhe vargje lidhjesh. Prandaj, duhet të shkruani saktësisht se si zbatohet grafiku nga këto struktura programuese.
Duhet të theksohet se asnjë nga sa më sipër nuk zbatohet për procesin aktual të shkrimit të kodit. Kur shkruani kodin, domethënë kryeni hapin e tretë, duhet gjithashtu të mendoni dhe të mendoni përmes programit. Nëse një nëndetyrë rezulton të jetë komplekse ose jo e dukshme, duhet të shkruani një specifikim për të. Por këtu nuk po flas për vetë kodin. Ju mund të përdorni çdo gjuhë programimi, çdo metodologji, nuk ka të bëjë me to. Gjithashtu, asnjë nga sa më sipër nuk eliminon nevojën për të testuar dhe korrigjuar kodin. Edhe nëse modeli abstrakt është shkruar saktë, mund të ketë gabime në zbatimin e tij.
Shkrimi i specifikimeve është një hap shtesë në procesin e kodimit. Falë tij, shumë gabime mund të kapen me më pak përpjekje - ne e dimë këtë nga përvoja e programuesve nga Amazon. Me specifikimet, cilësia e programeve bëhet më e lartë. Atëherë, pse ne shkojmë kaq shpesh pa to? Sepse shkrimi është i vështirë. Dhe shkrimi është i vështirë, sepse për këtë duhet të mendosh, dhe të menduarit është gjithashtu i vështirë. Është gjithmonë më e lehtë të pretendosh atë që mendon. Këtu mund të vizatoni një analogji me vrapimin - sa më pak të vraponi, aq më ngadalë vraponi. Ju duhet të stërvitni muskujt dhe të praktikoni të shkruarit. Duhet praktikë.
Specifikimi mund të jetë i pasaktë. Ju mund të keni bërë një gabim diku, ose kërkesat mund të kenë ndryshuar, ose mund të duhet të bëhet një përmirësim. Çdo kod që përdor dikush duhet të ndryshohet, kështu që herët a vonë specifikimi nuk do të përputhet më me programin. Idealisht, në këtë rast, ju duhet të shkruani një specifikim të ri dhe të rishkruani plotësisht kodin. Ne e dimë shumë mirë që askush nuk e bën këtë. Në praktikë, ne rregullojmë kodin dhe mundësisht përditësojmë specifikimet. Nëse kjo do të ndodhë herët a vonë, atëherë pse të shkruani fare specifikime? Së pari, për personin që do të modifikojë kodin tuaj, çdo fjalë shtesë në specifikim do të vlejë peshën e saj në ar, dhe ky person mund të jeni ju vetë. Shpesh e qortoj veten që nuk kam specifikime të mjaftueshme kur jam duke redaktuar kodin tim. Dhe unë shkruaj më shumë specifika sesa kode. Prandaj, kur redaktoni kodin, specifikimi gjithmonë duhet të përditësohet. Së dyti, me çdo rishikim, kodi përkeqësohet, bëhet gjithnjë e më i vështirë për t'u lexuar dhe ruajtur. Kjo është një rritje e entropisë. Por nëse nuk filloni me një specifikim, atëherë çdo rresht që shkruani do të jetë një modifikim dhe kodi do të jetë i vështirë dhe i vështirë për t'u lexuar që në fillim.
Siç u tha , asnjë betejë nuk fitohej me plan dhe asnjë betejë nuk fitohej pa plan. Dhe ai dinte një ose dy gjëra për betejat. Ekziston një mendim se shkrimi i 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 duhet të mbani mend gjithmonë se kur ju thuhet të mos shkruani specifikime, ju thuhet të mos mendoni. Dhe ju duhet të mendoni për këtë çdo herë. Mendimi për detyrën nuk garanton që nuk do të bëni gabime. Siç e dimë, askush nuk e shpiku shkopin magjik, dhe programimi është një detyrë e vështirë. Por nëse nuk e kuptoni problemin, me siguri do të bëni gabime.
Mund të lexoni më shumë rreth TLA + dhe PlusCal në një faqe interneti të veçantë, mund të shkoni atje nga faqja ime kryesore . Kjo është e gjitha për mua, faleminderit për vëmendjen tuaj.
Ju lutemi vini re se ky është një përkthim. Kur shkruani komente, mbani mend se autori nuk do t'i lexojë ato. Nëse vërtet dëshironi të bisedoni me autorin, atëherë ai do të jetë në konferencën Hydra 2019, e cila do të mbahet 11-12 korrik 2019 në Shën Petersburg. Biletat mund të blihen .
Burimi: www.habr.com