Acest articol este o traducere . Dar înaintea ei o mică prezentare. Cum se formează zombii? Toată lumea a ajuns într-o situație în care vrea să aducă un prieten sau un coleg la nivelul lor, dar nu iese. Și nu este atât de mult cu tine, cât cu el că „nu merge”: pe de o parte a scalei este un salariu normal, sarcini și așa mai departe, iar pe de altă parte, nevoia de a gândi. Gândirea este neplăcută și dureroasă. Renunță rapid și continuă să scrie cod fără să-și dezvolte deloc creierul. Îți imaginezi cât de mult efort este nevoie pentru a depăși bariera neputinței învățate și pur și simplu nu o faci. Așa se formează zombi, care, se pare, pot fi vindecați, dar se pare că nimeni nu o va face.
Când am văzut asta (da, același tovarăș de la manuale) și nu face un raport, ci o sesiune de întrebări și răspunsuri, am fost puțin precaut. Pentru orice eventualitate, Leslie este un om de știință de renume mondial, autorul unor lucrări fundamentale în calculul distribuit și îl puteți cunoaște și prin literele La din cuvântul LaTeX - „Lamport TeX”. Al doilea factor alarmant este cerința lui: toți cei care vin trebuie să asculte (absolut gratuit) câteva dintre rapoartele lui în avans, să vină cu cel puțin o întrebare despre ele și abia apoi să vină. Am decis să văd ce transmite Lamport acolo - și este grozav! Este exact acel lucru, pastilele magice pentru a vindeca zombi. Vă avertizez: din text, iubitorii de metodologii super-flexibile și cei cărora nu le place să testeze ceea ce este scris se pot arde notabil.
După habrokat, de fapt, începe traducerea seminarului. Bucură-te de lectură!
Indiferent de sarcina pe care o îndeplinești, trebuie să treci mereu prin trei pași:
- decideți ce obiectiv doriți să atingeți;
- decide cum îți vei atinge obiectivul;
- vino la scopul tău.
Acest lucru este valabil și pentru programare. Când scriem cod, trebuie să:
- decide ce ar trebui să facă programul;
- determina modul în care ar trebui să-și îndeplinească sarcina;
- scrie codul corespunzător.
Ultimul pas, desigur, este foarte important, dar nu voi vorbi despre el astăzi. În schimb, vom discuta despre primele două. Fiecare programator le execută înainte de a începe să lucreze. Nu vă așezați să scrieți decât dacă ați decis dacă scrieți un browser sau o bază de date. O anumită idee despre obiectiv trebuie să fie prezentă. Și cu siguranță te gândești la ce anume va face programul și nu scrie cumva în speranța că codul se va transforma cumva într-un browser.
Cum se întâmplă exact acest cod pre-gândire? Cât de mult efort ar trebui să depunem în asta? Totul depinde de cât de complexă este problema pe care o rezolvăm. Să presupunem că vrem să scriem un sistem distribuit tolerant la erori. În acest caz, ar trebui să ne gândim bine înainte de a ne așeza la cod. Ce se întâmplă dacă trebuie doar să creștem o variabilă întreagă cu 1? La prima vedere, totul este banal aici și nu este nevoie de gânduri, dar apoi ne amintim că poate apărea un preaplin. Prin urmare, chiar și pentru a înțelege dacă o problemă este simplă sau complexă, trebuie mai întâi să te gândești.
Dacă vă gândiți în avans la posibile soluții la problemă, puteți evita greșelile. Dar asta necesită ca gândirea ta să fie clară. Pentru a realiza acest lucru, trebuie să vă scrieți gândurile. Îmi place foarte mult citatul lui Dick Guindon: „Când scrii, natura îți arată cât de neglijent este gândirea ta”. Dacă nu scrii, crezi doar că te gândești. Și trebuie să vă scrieți gândurile sub formă de specificații.
Specificațiile îndeplinesc multe funcții, în special în proiectele mari. Dar voi vorbi doar despre una dintre ele: ne ajută să gândim clar. A gândi clar este foarte important și destul de dificil, așa că aici avem nevoie de orice ajutor. În ce limbă ar trebui să scriem specificațiile? În general, aceasta este întotdeauna prima întrebare pentru programatori: în ce limbă vom scrie. Nu există un răspuns corect la acesta: problemele pe care le rezolvăm sunt prea diverse. Pentru unii, TLA+ este un limbaj de specificații pe care l-am dezvoltat. Pentru alții, este mai convenabil să folosească limba chineză. Totul depinde de situație.
Mai importantă este o altă întrebare: cum să obțineți o gândire mai clară? Răspuns: Trebuie să gândim ca oamenii de știință. Acesta este un mod de a gândi care s-a dovedit în ultimii 500 de ani. În știință, construim modele matematice ale realității. Astronomia a fost poate prima știință în sensul strict al cuvântului. În modelul matematic folosit în astronomie, corpurile cerești apar ca puncte cu masă, poziție și impuls, deși în realitate sunt obiecte extrem de complexe cu munți și oceane, maree și maree. Acest model, ca oricare altul, a fost creat pentru a rezolva anumite probleme. Este excelent pentru a determina unde să îndreptați telescopul dacă trebuie să găsiți o planetă. Dar dacă vrei să prezici vremea pe această planetă, acest model nu va funcționa.
Matematica ne permite să determinăm proprietățile modelului. Și știința arată cum aceste proprietăți se raportează la realitate. Să vorbim despre știința noastră, informatica. Realitatea cu care lucrăm sunt sistemele de calcul de diverse feluri: procesoare, console de jocuri, calculatoare, programe de execuție etc. Voi vorbi despre rularea unui program pe un computer, dar, în general, toate aceste concluzii se aplică oricărui sistem de calcul. În știința noastră, folosim multe modele diferite: mașina Turing, seturi parțial ordonate de evenimente și multe altele.
Ce este un program? Acesta este orice cod care poate fi considerat independent. Să presupunem că trebuie să scriem un browser. Efectuăm trei sarcini: proiectăm vizualizarea utilizatorului asupra programului, apoi scriem diagrama de nivel înalt a programului și, în final, scriem codul. Pe măsură ce scriem codul, ne dăm seama că trebuie să scriem un formatator de text. Aici trebuie din nou să rezolvăm trei probleme: stabiliți ce text va returna acest instrument; selectați un algoritm pentru formatare; scrie codul. Această sarcină are propria ei sarcină secundară: introduceți corect o cratimă în cuvinte. De asemenea, rezolvăm această sarcină secundară în trei pași - după cum puteți vedea, acestea sunt repetate la mai multe niveluri.
Să luăm în considerare mai detaliat primul pas: ce problemă rezolvă programul. Aici, cel mai adesea modelăm un program ca o funcție care preia o anumită intrare și produce o ieșire. În matematică, o funcție este de obicei descrisă ca un set ordonat de perechi. De exemplu, funcția de pătrat pentru numerele naturale este descrisă ca mulțimea {<0,0>, <1,1>, <2,4>, <3,9>, …}. Domeniul unei astfel de funcții este mulțimea primelor elemente ale fiecărei perechi, adică numerele naturale. Pentru a defini o funcție, trebuie să specificăm domeniul și formula acesteia.
Dar funcțiile din matematică nu sunt aceleași cu funcțiile din limbajele de programare. Matematica este mult mai ușoară. Deoarece nu am timp pentru exemple complexe, să luăm în considerare unul simplu: o funcție în C sau o metodă statică în Java care returnează cel mai mare divizor comun a două numere întregi. În specificarea acestei metode, vom scrie: calcule GCD(M,N) pentru argumente M и NUnde GCD(M,N) - o funcție al cărei domeniu este mulțimea de perechi de numere întregi, iar valoarea returnată este cel mai mare număr întreg care este divizibil cu M и N. Cum se raportează acest model la realitate? Modelul operează pe numere întregi, în timp ce în C sau Java avem un 32 de biți int. Acest model ne permite să decidem dacă algoritmul este corect GCD, dar nu va preveni erorile de overflow. Acest lucru ar necesita un model mai complex, pentru care nu există timp.
Să vorbim despre limitările unei funcții ca model. Unele programe (cum ar fi sistemele de operare) nu returnează doar o anumită valoare pentru anumite argumente, ele pot rula continuu. În plus, funcția ca model nu este potrivită pentru al doilea pas: planificarea modului de rezolvare a problemei. Sortarea rapidă și sortarea cu bule calculează aceeași funcție, dar sunt algoritmi complet diferiți. Prin urmare, pentru a descrie modul în care este atins scopul programului, folosesc un model diferit, să-l numim modelul comportamental standard. Programul din acesta este reprezentat ca un set de toate comportamentele permise, fiecare dintre acestea, la rândul său, o secvență de stări, iar starea este atribuirea de valori variabilelor.
Să vedem cum ar arăta al doilea pas pentru algoritmul Euclid. Trebuie să calculăm GCD(M, N). Inițializam M ca xȘi N ca y, apoi scădeți în mod repetat cea mai mică dintre aceste variabile din cea mai mare până când sunt egale. De exemplu, dacă M = 12Și N = 18, putem descrie următorul comportament:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Și dacă M = 0 и N = 0? Zero este divizibil cu toate numerele, deci nu există cel mai mare divizor în acest caz. În această situație, trebuie să ne întoarcem la primul pas și să ne întrebăm: chiar trebuie să calculăm GCD pentru numerele nepozitive? Dacă acest lucru nu este necesar, atunci trebuie doar să schimbați specificația.
Aici ar trebui să facem o mică digresiune despre productivitate. Este adesea măsurată în numărul de linii de cod scrise pe zi. Dar munca ta este mult mai utilă dacă scapi de un anumit număr de linii, pentru că ai mai puțin loc pentru bug-uri. Și cel mai simplu mod de a scăpa de cod este la primul pas. Este cu totul posibil să nu aveți nevoie de toate clopotele și fluierele pe care încercați să le implementați. Cea mai rapidă modalitate de a simplifica un program și de a economisi timp este să nu faci lucruri care nu ar trebui făcute. Al doilea pas este al doilea potențial de economisire a timpului. Dacă măsurați productivitatea în termeni de rânduri scrise, atunci vă va face să vă gândiți cum să îndepliniți o sarcină mai putin productiv, deoarece puteți rezolva aceeași problemă cu mai puțin cod. Nu pot da statistici exacte aici, pentru că nu am cum să număr numărul de rânduri pe care nu le-am scris din cauza faptului că am petrecut timp pe specificație, adică pe primul și al doilea pas. Și nici aici experimentul nu poate fi pus la punct, pentru că în experiment nu avem dreptul de a parcurge primul pas, sarcina este prestabilită.
Este ușor să treci cu vederea multe dificultăți în specificațiile informale. Nu este nimic dificil să scrii specificații stricte pentru funcții, nu voi discuta despre asta. În schimb, vom vorbi despre scrierea unor specificații puternice pentru comportamentele standard. Există o teoremă care spune că orice set de comportamente poate fi descris folosind proprietatea de securitate (Siguranță) și proprietăți de supraviețuire (viuitate). Securitatea înseamnă că nu se va întâmpla nimic rău, programul nu va da un răspuns incorect. Supraviețuirea înseamnă că, mai devreme sau mai târziu, ceva bun se va întâmpla, adică programul va da răspunsul corect mai devreme sau mai târziu. De regulă, securitatea este un indicator mai important, erorile apar cel mai adesea aici. Prin urmare, pentru a economisi timp, nu voi vorbi despre supraviețuire, deși este, desigur, și importantă.
Obținem securitate prin prescrierea, în primul rând, a setului de stări inițiale posibile. Și în al doilea rând, relațiile cu toate stările următoare posibile pentru fiecare stat. Să ne comportăm ca niște oameni de știință și să definim matematic stările. Setul de stări inițiale este descris printr-o formulă, de exemplu, în cazul algoritmului Euclid: (x = M) ∧ (y = N). Pentru anumite valori M и N există o singură stare inițială. Relația cu starea următoare este descrisă printr-o formulă în care variabilele stării următoare sunt scrise cu prim, iar variabilele stării curente sunt scrise fără prim. În cazul algoritmului lui Euclid, ne vom ocupa de disjuncția a două formule, în una dintre care x este cea mai mare valoare, iar în a doua - y:
În primul caz, noua valoare a lui y este egală cu valoarea anterioară a lui y și obținem noua valoare a lui x scăzând variabila mai mică din variabila mai mare. În al doilea caz, facem invers.
Să revenim la algoritmul lui Euclid. Să presupunem din nou că M = 12, N = 18. Aceasta definește o singură stare inițială, (x = 12) ∧ (y = 18). Apoi introducem acele valori în formula de mai sus și obținem:
Iată singura soluție posibilă: x' = 18 - 12 ∧ y' = 12și obținem comportamentul: [x = 12, y = 18]. În mod similar, putem descrie toate stările din comportamentul nostru: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
In ultima stare [x = 6, y = 6] ambele părți ale expresiei vor fi false, deci nu are următoarea stare. Deci, avem o specificație completă a celui de-al doilea pas - după cum puteți vedea, aceasta este o matematică destul de obișnuită, ca în ingineri și oameni de știință, și nu ciudată, ca în informatică.
Aceste două formule pot fi combinate într-o singură formulă a logicii temporale. Este elegantă și ușor de explicat, dar nu mai are timp pentru ea acum. S-ar putea să avem nevoie de logica temporală doar pentru proprietatea vioicității, nu este necesară pentru securitate. Nu-mi place logica temporală ca atare, nu este matematică chiar obișnuită, dar în cazul vioicității este un rău necesar.
În algoritmul lui Euclid, pentru fiecare valoare x и y au valori unice x' и y', care fac adevărată relația cu următoarea stare. Cu alte cuvinte, algoritmul lui Euclid este determinist. Pentru a modela un algoritm nedeterminist, starea curentă trebuie să aibă mai multe stări posibile viitoare și ca fiecare valoare variabilă neamorsată să aibă mai multe valori variabile amorsate, astfel încât relația cu următoarea stare să fie adevărată. Acest lucru este ușor de făcut, dar nu voi da exemple acum.
Pentru a face un instrument de lucru, aveți nevoie de matematică formală. Cum se face ca specificația formală? Pentru a face acest lucru, avem nevoie de un limbaj formal, de exemplu, . Specificația algoritmului Euclid ar arăta astfel în acest limbaj:
Un simbol de semn egal cu un triunghi înseamnă că valoarea din stânga semnului este definită ca fiind egală cu valoarea din dreapta semnului. În esență, specificația este o definiție, în cazul nostru două definiții. La specificația din TLA+, trebuie să adăugați declarații și o sintaxă, ca în slide-ul de mai sus. În ASCII ar arăta astfel:
După cum puteți vedea, nimic complicat. Specificația pentru TLA+ poate fi testată, adică ocoliți toate comportamentele posibile într-un model mic. În cazul nostru, acest model va avea anumite valori M и N. Aceasta este o metodă de verificare foarte eficientă și simplă, care este complet automată. De asemenea, este posibil să scrieți dovezi formale de adevăr și să le verificați mecanic, dar acest lucru necesită mult timp, așa că aproape nimeni nu face asta.
Principalul dezavantaj al TLA+ este că este matematică, iar programatorilor și informaticienilor le este frică de matematică. La prima vedere, sună ca o glumă, dar, din păcate, o spun cu toată seriozitatea. Colegul meu tocmai îmi spunea cum a încercat să explice TLA+ mai multor dezvoltatori. De îndată ce formulele au apărut pe ecran, au devenit imediat ochi sticloși. Deci, dacă TLA+ te sperie, poți folosi , este un fel de limbaj de programare pentru jucării. O expresie în PlusCal poate fi orice expresie TLA+, adică, în general, orice expresie matematică. În plus, PlusCal are o sintaxă pentru algoritmi nedeterminiști. Deoarece PlusCal poate scrie orice expresie TLA+, PlusCal este mult mai expresiv decât orice limbaj de programare real. În continuare, PlusCal este compilat într-o specificație TLA+ ușor de citit. Acest lucru nu înseamnă, desigur, că specificația complexă PlusCal se va transforma într-una simplă pe TLA + - doar corespondența dintre ele este evidentă, nu va exista o complexitate suplimentară. În cele din urmă, această specificație poate fi verificată de instrumentele TLA+. Una peste alta, PlusCal poate ajuta la depășirea fobiei de matematică și este ușor de înțeles chiar și pentru programatori și informaticieni. În trecut, am publicat algoritmi pe el de ceva timp (aproximativ 10 ani).
Poate cineva va obiecta că TLA + și PlusCal sunt matematică, iar matematica funcționează doar pe exemple inventate. În practică, aveți nevoie de un limbaj real cu tipuri, proceduri, obiecte și așa mai departe. Este gresit. Iată ce scrie Chris Newcomb, care a lucrat la Amazon: „Am folosit TLA+ în zece proiecte majore și, în fiecare caz, a făcut o diferență semnificativă în dezvoltare, deoarece am fost capabili să prindem erori periculoase înainte de a ajunge în producție și pentru că ne-a oferit perspectiva și încrederea de care aveam nevoie pentru a obține performanțe agresive. optimizări fără a afecta adevărul programului". Puteți auzi adesea că atunci când folosim metode formale, obținem cod ineficient - în practică, totul este exact invers. În plus, există opinia că managerii nu pot fi convinși de necesitatea metodelor formale, chiar dacă programatorii sunt convinși de utilitatea lor. Și Newcomb scrie: „Managerii fac acum eforturi pentru a scrie specificații pentru TLA + și pentru a aloca în mod special timp pentru asta”. Deci, atunci când managerii văd că TLA+ funcționează, sunt bucuroși să accepte. Chris Newcomb a scris asta în urmă cu aproximativ șase luni (octombrie 2014), dar acum, din câte știu, TLA+ este folosit în 14 proiecte, nu în 10. Un alt exemplu se referă la designul XBox 360. Un stagiar a venit la Charles Thacker și a scris specificația pentru sistemul de memorie. Datorită acestei specificații, a fost găsit un bug care altfel ar trece neobservat și din cauza căruia fiecare XBox 360 s-ar prăbuși după patru ore de utilizare. Inginerii IBM au confirmat că testele lor nu ar fi găsit această eroare.
Puteți citi mai multe despre TLA + pe Internet, dar acum să vorbim despre specificații informale. Rareori trebuie să scriem programe care calculează cel mai mic divizor comun și altele asemenea. Mult mai des scriem programe precum instrumentul de imprimantă drăguță pe care l-am scris pentru TLA+. După cea mai simplă procesare, codul TLA + ar arăta astfel:
Dar în exemplul de mai sus, cel mai probabil utilizatorul a dorit ca conjuncția și semnele egale să fie aliniate. Deci formatarea corectă ar arăta mai degrabă astfel:
Luați în considerare un alt exemplu:
Aici, dimpotrivă, alinierea semnelor de egalitate, adunare și înmulțire în sursă a fost aleatorie, așa că cea mai simplă prelucrare este suficientă. În general, nu există o definiție matematică exactă a formatării corecte, deoarece „corect” în acest caz înseamnă „ceea ce dorește utilizatorul”, iar acest lucru nu poate fi determinat matematic.
S-ar părea că dacă nu avem o definiție a adevărului, atunci specificația este inutilă. Dar nu este. Doar pentru că nu știm ce trebuie să facă un program, nu înseamnă că nu trebuie să ne gândim la modul în care funcționează - dimpotrivă, trebuie să depunem și mai mult efort în el. Specificația este deosebit de importantă aici. Este imposibil să se determine programul optim pentru imprimarea structurată, dar asta nu înseamnă că nu ar trebui să-l luăm deloc, iar scrierea codului ca flux de conștiință nu este un lucru bun. La final, am scris o specificație de șase reguli cu definiții sub formă de comentarii într-un fișier java. Iată un exemplu de una dintre reguli: a left-comment token is LeftComment aligned with its covering token. Această regulă este scrisă, să spunem, în engleză matematică: LeftComment aligned, left-comment и covering token - termeni cu definiții. Așa descriu matematicienii matematica: ei scriu definiții ale termenilor și, pe baza lor, reguli. Avantajul unei astfel de specificații este că șase reguli sunt mult mai ușor de înțeles și de depanat decât 850 de linii de cod. Trebuie să spun că scrierea acestor reguli nu a fost ușoară, a fost nevoie de destul de mult timp pentru a le depana. În special în acest scop, am scris un cod care a raportat ce regulă a fost folosită. Datorită faptului că am testat aceste șase reguli pe mai multe exemple, nu a trebuit să depanez 850 de linii de cod, iar erorile s-au dovedit a fi destul de ușor de găsit. Java are instrumente grozave pentru asta. Dacă tocmai aș fi scris codul, mi-ar fi luat mult mai mult, iar formatarea ar fi fost de o calitate mai slabă.
De ce nu a putut fi folosită o specificație formală? Pe de o parte, execuția corectă nu este prea importantă aici. Imprimările structurale sunt obligate să nu mulțumească nimănui, așa că nu a trebuit să le fac să funcționeze corect în toate situațiile ciudate. Și mai important este faptul că nu aveam instrumente adecvate. Verificatorul de modele TLA+ este inutil aici, așa că ar trebui să scriu manual exemplele.
Specificația de mai sus are caracteristici comune tuturor specificațiilor. Este un nivel mai înalt decât codul. Poate fi implementat în orice limbă. Orice instrumente sau metode sunt inutile pentru a le scrie. Niciun curs de programare nu vă va ajuta să scrieți această specificație. Și nu există instrumente care ar putea face ca această specificație să fie inutilă, cu excepția cazului în care, desigur, scrieți un limbaj special pentru scrierea programelor de tipărire structurate în TLA+. În cele din urmă, această specificație nu spune nimic despre exact cum vom scrie codul, ea precizează doar ce face acest cod. Scriem specificația pentru a ne ajuta să ne gândim la problemă înainte de a începe să ne gândim la cod.
Dar această specificație are și caracteristici care o deosebesc de alte specificații. 95% din alte specificații sunt semnificativ mai scurte și mai simple:
În plus, această specificație este un set de reguli. De regulă, acesta este un semn de specificație slabă. Înțelegerea consecințelor unui set de reguli este destul de dificilă, motiv pentru care a trebuit să petrec mult timp depanând-le. Cu toate acestea, în acest caz, nu am putut găsi o cale mai bună.
Merită să spuneți câteva cuvinte despre programele care rulează continuu. De regulă, ele funcționează în paralel, de exemplu, sisteme de operare sau sisteme distribuite. Foarte puțini oameni le pot înțelege mental sau pe hârtie, iar eu nu sunt unul dintre ei, deși cândva am putut să o fac. Prin urmare, avem nevoie de instrumente care ne vor verifica munca - de exemplu, TLA + sau PlusCal.
De ce a fost necesar să scriu o specificație dacă știam deja ce trebuie să facă exact codul? De fapt, am crezut că știu. În plus, cu o specificație, un outsider nu mai trebuie să intre în cod pentru a înțelege exact ce face. Am o regulă: nu ar trebui să existe reguli generale. Există o excepție de la această regulă, desigur, este singura regulă generală pe care o urmez: specificarea a ceea ce face codul ar trebui să le spună oamenilor tot ce trebuie să știe când folosesc codul.
Deci, ce anume trebuie să știe programatorii despre gândire? Pentru început, la fel ca toți ceilalți: dacă nu scrii, atunci doar ți se pare că te gândești. De asemenea, trebuie să vă gândiți înainte de a codifica, ceea ce înseamnă că trebuie să scrieți înainte de a codifica. Specificația este ceea ce scriem înainte de a începe codificarea. Este necesară o specificație pentru orice cod care poate fi folosit sau modificat de oricine. Și acest „cineva” poate fi însuși autorul codului la o lună după ce a fost scris. Este necesară o specificație pentru programe și sisteme mari, pentru clase, pentru metode și uneori chiar pentru secțiuni complexe ale unei singure metode. Ce anume ar trebui scris despre cod? Trebuie să descrii ce face, adică ce poate fi util oricărei persoane care utilizează acest cod. Uneori poate fi necesar să se specifice modul în care codul își îndeplinește scopul. Dacă am trecut prin această metodă în cursul algoritmilor, atunci o numim algoritm. Dacă este ceva mai special și mai nou, atunci îl numim design de nivel înalt. Nu există nicio diferență formală aici: ambele sunt un model abstract al unui program.
Cum ar trebui să scrieți mai exact o specificație de cod? Principalul lucru: ar trebui să fie cu un nivel mai mare decât codul în sine. Ar trebui să descrie stări și comportamente. Ar trebui să fie atât de strict pe cât cere sarcina. Dacă scrieți o specificație pentru modul în care va fi implementată o sarcină, o puteți scrie în pseudocod sau cu PlusCal. Trebuie să învățați cum să scrieți specificații pe specificații formale. Acest lucru vă va oferi abilitățile necesare care vă vor ajuta și cu cele informale. Cum înveți să scrii specificații formale? Când am învățat să programăm, am scris programe și apoi le-am depanat. Este la fel și aici: scrieți specificațiile, verificați-o cu verificatorul de modele și remediați erorile. Este posibil ca TLA+ să nu fie cel mai bun limbaj pentru o specificație formală, iar o altă limbă este probabil mai bună pentru nevoile dumneavoastră specifice. Avantajul TLA+ este că învață foarte bine gândirea matematică.
Cum se conectează specificația și codul? Cu ajutorul comentariilor care leagă conceptele matematice și implementarea lor. Dacă lucrați cu grafice, atunci la nivel de program veți avea matrice de noduri și matrice de legături. Prin urmare, trebuie să scrieți exact cum este implementat graficul de aceste structuri de programare.
Trebuie remarcat faptul că niciuna dintre cele de mai sus nu se aplică procesului propriu-zis de scriere a codului. Când scrieți codul, adică efectuați al treilea pas, trebuie să vă gândiți și să vă gândiți la program. Dacă o sarcină secundară se dovedește a fi complexă sau neevidentă, trebuie să scrieți o specificație pentru aceasta. Dar aici nu vorbesc despre codul în sine. Puteți folosi orice limbaj de programare, orice metodologie, nu este vorba despre ele. De asemenea, niciuna dintre cele de mai sus nu elimină necesitatea de a testa și depana codul. Chiar dacă modelul abstract este scris corect, pot exista erori în implementarea lui.
Scrierea specificațiilor este un pas suplimentar în procesul de codificare. Datorită acesteia, multe erori pot fi surprinse cu mai puțin efort - știm acest lucru din experiența programatorilor de la Amazon. Cu specificații, calitatea programelor devine mai mare. Atunci de ce mergem atât de des fără ele? Pentru că scrisul este greu. Iar scrisul este dificil, pentru că pentru asta trebuie să gândești, iar gândirea este, de asemenea, dificilă. Întotdeauna este mai ușor să te prefaci ce gândești. Aici puteți face o analogie cu alergarea - cu cât alergați mai puțin, cu atât alergați mai încet. Trebuie să-ți antrenezi mușchii și să exersezi scrisul. E nevoie de practică.
Specificația poate fi incorectă. S-ar putea să fi făcut o greșeală undeva, sau cerințele s-ar fi schimbat sau ar putea fi necesară o îmbunătățire. Orice cod pe care îl folosește cineva trebuie schimbat, așa că mai devreme sau mai târziu specificația nu se va mai potrivi cu programul. În mod ideal, în acest caz, trebuie să scrieți o nouă specificație și să rescrieți complet codul. Știm foarte bine că nimeni nu face asta. În practică, corectăm codul și eventual actualizăm specificația. Dacă acest lucru se va întâmpla mai devreme sau mai târziu, atunci de ce să scrieți specificații? În primul rând, pentru persoana care vă va edita codul, fiecare cuvânt suplimentar din specificație va valorifica greutatea lui în aur, iar această persoană poate fi chiar dvs. Mă reproșez adesea pentru că nu am suficiente specificații atunci când îmi editez codul. Și scriu mai multe specificații decât cod. Prin urmare, atunci când editați codul, specificația trebuie întotdeauna actualizată. În al doilea rând, cu fiecare revizuire, codul se înrăutățește, devine din ce în ce mai dificil de citit și întreținut. Aceasta este o creștere a entropiei. Dar dacă nu începeți cu o specificație, atunci fiecare linie pe care o scrieți va fi o editare, iar codul va fi greu de manevrat și greu de citit de la început.
După cum am spus , nicio bătălie nu a fost câștigată prin plan și nicio bătălie nu a fost câștigată fără un plan. Și știa ceva sau două despre bătălii. Există opinia că scrierea specificațiilor este o pierdere de timp. Uneori, acest lucru este adevărat, iar sarcina este atât de simplă încât nu trebuie să te gândești la ea. Dar ar trebui să vă amintiți întotdeauna că atunci când vi se spune să nu scrieți specificații, vi se spune să nu gândiți. Și ar trebui să te gândești la asta de fiecare dată. Gândirea la sarcină nu garantează că nu vei face greșeli. După cum știm, nimeni nu a inventat bagheta magică, iar programarea este o sarcină dificilă. Dar dacă nu te gândești la problemă, ești garantat să faci greșeli.
Puteți citi mai multe despre TLA + și PlusCal pe un site special, puteți merge acolo de pe pagina mea de pornire . Asta e tot pentru mine, mulțumesc pentru atenție.
Vă rugăm să rețineți că aceasta este o traducere. Când scrieți comentarii, amintiți-vă că autorul nu le va citi. Dacă doriți cu adevărat să discutați cu autorul, atunci el va fi la conferința Hydra 2019, care va avea loc în perioada 11-12 iulie 2019 la Sankt Petersburg. Biletele pot fi achiziționate .
Sursa: www.habr.com