Acesta este un articol-traducere . Dar înainte de aceasta, o scurtă introducere. Cum se formează zombi? Fiecare a fost în situația în care vrea să-și ajute un prieten sau un coleg să ajungă la același nivel, dar nu reușește. Și „nu reușește” nu este atât de mult un problemă a ta, cât a lui: pe o parte a balanței se află un salariu decent, sarcini și așa mai departe, iar pe cealaltă — necesitatea de a gândi. Gânditul este neplăcut și dureros. El cedează rapid și continuă să scrie cod, fără să-și folosească mintea. Îți poți imagina cât de mult efort trebuie investit pentru a depăși bariera neputinței învățate, și pur și simplu nu o faci. Așa se formează zombii, pe care pare că-i poți trata, dar poate că nimeni nu se va ocupa de asta.
Când am văzut că (da, exact același tip din manuale) și nu face o prelegere, ci o sesiune de întrebări și răspunsuri, m-am simțit puțin suspect. De dragul precizării, Leslie este un cunoscut cercetător mondial, autor al unor lucrări fundamentale în calculul distribuit, și îl mai cunoașteți poate și din literele La din cuvântul LaTeX — „Lamport TeX”. Al doilea factor îngrijorător este cerința sa: fiecare persoană care va veni trebuie (total gratuit) să asculte în prealabil câteva dintre prelegerile sale, să formuleze cel puțin o întrebare despre acestea și abia apoi să vină. Am decis să văd ce anume transmite Lamport — și este minunat! Este exact aceea superba legătură-medicament pentru tratarea zombismului. Vă avertizez: textul ar putea provoca o reacție puternică pasionaților de metodologii ultra-flexibile și celor care nu iubesc să testeze ceea ce au scris.
După această introducere, începem efectiv traducerea seminarului. Lectură plăcută!
Indiferent de sarcina pe care o alegeți, trebuie să treceți întotdeauna prin trei pași:
- să vă determinați care este obiectivul pe care doriți să-l atingeți;
- să decideți cum anume veți urmări acest obiectiv;
- să ajungeți la obiectivul vostru.
Asta se aplică și programării. Când scriem cod, trebuie să:
- stabiliți ce ar trebui să facă programul;
- decideți cum anume ar trebui să își îndeplinească sarcina;
- să scrieți codul corespunzător.
Ultimul pas este, desigur, foarte important, dar despre el nu voi vorbi astăzi. În schimb, vom discuta despre primele două. Fiecare programator le îndeplinește înainte de a începe să lucreze. Nu te așezi să scrii dacă nu ai decis ce anume scrii: un browser sau o bază de date. O reprezentare clară a scopului trebuie să fie întotdeauna prezentă. Și te gândești mereu la ceea ce programul va face, nu scrii la întâmplare, sperând că codul se va transforma singur într-un browser.
Cum se desfășoară exact această gândire prealabilă a codului? Cât de mult efort ar trebui să investim în asta? Totul depinde de complexitatea problemei pe care o rezolvăm. Să presupunem că vrem să scriem un sistem distribuit rezistent la erori. În acest caz, ar trebui să analizăm totul cu atenție înainte de a ne apuca de cod. Dar dacă trebuie doar să incrementăm o variabilă întreagă cu 1? La prima vedere, pare trivial și nu este nevoie de reflecție, dar apoi ne amintim că poate apărea o depășire. Prin urmare, chiar și pentru a înțelege dacă o problemă este simplă sau complexă, trebuie să ne gândim la început.
Dacă analizezi dinainte soluțiile posibile pentru problemă, poți evita greșelile. Dar pentru asta, trebuie să ai un gândire clară. Pentru a realiza acest lucru, trebuie să îți notezi gândurile. Îmi place foarte mult o citat de Dick Hinton: „Când scrii, natura îți arată cât de haotic este gândirea ta.” Dacă nu scrii, doar ți se pare că gândești. Iar gândurile trebuie consemnate sub formă de specificații.
Specificațiile îndeplinesc numeroase funcții, în special în proiecte mari. Dar voi vorbi doar despre una dintre ele: ele ne ajută să gândim clar. Gândirea clară este foarte importantă și destul de dificilă, astfel că avem nevoie de orice sprijin. În ce limbă ar trebui să scriem specificațiile? Aceasta este întotdeauna prima întrebare pentru programatori: în ce limbă vom scrie. Nu există un singur răspuns corect la asta: problemele pe care le rezolvăm sunt prea diverse. Pentru unii, TLA+ este util - este un limbaj de specificații pe care l-am dezvoltat. Pentru alții, este mai convenabil să folosească chineză. Totul depinde de situație.
O întrebare mai importantă este: cum putem obține o gândire mai clară? Răspuns: trebuie să gândim ca niște oameni de știință. Aceasta este o modalitate de gândire care s-a dovedit extrem de eficientă în ultimele 500 de ani. În știință, construim modele matematice ale realității. Astronomia a fost, fără îndoială, prima știință în sensul strict al cuvântului. În modelul matematic utilizat în astronomie, corpurile cerești sunt reprezentate ca puncte cu masă, poziție și impuls, deși în realitate ele sunt obiecte extrem de complexe, cu munți și oceane, maree și reflux. Acest model, ca orice alt model, este creat pentru a rezolva anumite sarcini. Este excelent pentru a determina unde trebuie să direcționăm telescoapele atunci când dorim să găsim o planetă. Dar dacă vrem să prezicem vremea pe această planetă, acest model nu este adecvat.
Matematica ne permite să determinăm proprietățile modelului. Și știința arată cum aceste proprietăți se corelează cu realitatea. Să vorbim despre știința noastră, informatica. Realitatea cu care lucrăm este reprezentată de sisteme de calcul de diferite tipuri: procesoare, console de jocuri, computere care rulează programe și așa mai departe. Voi discuta despre execuția unui program pe un computer, dar, în mare, toate aceste concluzii sunt aplicabile oricărui sistem de calcul. În știința noastră folosim multe modele diferite: mașina Turing, mulțimi parțial ordonate de evenimente și multe altele.
Ce este un program? Este orice cod care poate fi considerat de sine stătător. Să presupunem că trebuie să scriem un browser. Executăm trei sarcini: proiectăm modul de prezentare a programului pentru utilizator, apoi scriem un schema de nivel înalt a programului și, în final, scriem codul. Pe măsură ce scriem codul, realizăm că trebuie să creăm un instrument pentru formatarea textului. Aici, din nou, trebuie să rezolvăm trei sarcini: să stabilim ce text va returna acest instrument; să alegem un algoritm pentru formatare; să scriem codul. Această sarcină are și ea o sub-sarcină: să inserăm corect cratima în cuvinte. Această sub-sarcină o rezolvăm și în trei pași – după cum vedem, ele se repetă la multe niveluri.
Să analizăm mai detaliat primul pas: ce problemă rezolvă programul. Aici, de cele mai multe ori, modelăm programul ca o funcție care primește anumite date de intrare și returnează anumite date de ieșire. În matematică, o funcție este de obicei descrisă ca un set ordonat de perechi. De exemplu, funcția de ridicare la pătrat pentru numere naturale este descrisă ca mulțimea {, , , , …}. Domeniul de definiție al acestei 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 său de definiție și formula.
Dar funcțiile în matematică nu sunt același lucru cu funcțiile din limbajele de programare. Matematica este mult mai simplă. Deoarece nu am timp pentru exemple complicate, să luăm unul simplu: o funcție în limbajul C sau o metodă statică în Java care returnează cel mai mare divizor comun al două numere întregi. În specificația acestei metode vom scrie: calculează GCD(M,N) pentru argumentele M și N, unde GCD(M,N) — o funcție, al cărei domeniu de definiție este mulțimea perechilor de numere întregi, iar valoarea returnată este cel mai mare număr întreg care împarte M și N. Cum se corelează această modelare cu realitatea? Modelul operează cu numere întregi, iar în C sau Java avem un intde 32 de biți. Acest model ne permite să stabilim dacă algoritmul este corect GCD, dar nu va preveni erorile de depășire. Pentru aceasta, ar fi nevoie de un model mai complex, pentru care nu este timp.
Să discutăm despre limitările funcției ca model. Funcționarea unora dintre programe (de exemplu, sistemele de operare) nu se rezumă la a returna o valoare specifică pentru argumente specifice, ele pot funcționa continuu. În plus, funcția ca model se potrivește prost pentru al doilea pas: planificarea modalității de rezolvare a problemei. Sortarea rapidă și sortarea prin bule calculează aceeași funcție, dar sunt algoritmi complet diferiți. De aceea, pentru a descrie modalitatea de atingere a obiectivului programului, voi folosi un alt model, să-l numim modelul comportamental standard. Programul este prezentat ca un set de toate comportamentele admisibile, fiecare fiind, la rândul său, o secvență de stări, iar starea este o atribuire de valori variabilelor.
Să vedem cum va arăta al doilea pas pentru algoritmul Euclidian. Trebuie să calculăm GCD(M, N). Vom iniția M cum x, iar N cum Stabiliți o parolă și păstrați-o în siguranță!, apoi scădem din nou cea mai mică dintre aceste variabile din cea mai mare până când devin egale. De exemplu, dacă M = 12, iar N = 18, putem descrie următoarea comportare:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Și dacă M = 0 și N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Aici ar trebui să facem o mică digresiune despre productivitate. Aceasta este adesea măsurată în numărul de linii de cod scrise pe zi. Dar munca dumneavoastră este mult mai utilă dacă ați eliminat un anumit număr de linii, deoarece ați redus astfel șansele de erori. Iar eliminarea codului este cel mai ușor de realizat chiar în primul pas. Este foarte posibil să nu aveți nevoie de toate acele caracteristici pe care încercați să le implementați. Cea mai rapidă modalitate de a simplifica programul și de a economisi timp este să nu faceți lucruri care nu merită făcute. Al doilea pas este pe locul doi în ceea ce privește potențialul de economisire a timpului. Dacă măsurați productivitatea în numărul de linii scrise, atunci gândirea la un mod de a rezolva o sarcină vă va face mai puțin productiv, deoarece veți putea rezolva aceeași sarcină cu un volum mai mic de cod. Nu pot oferi statistici exacte aici, deoarece nu am un mod de a număra numărul de linii pe care nu le-am scris datorită timpului petrecut pentru specificare, adică pentru primele două etape. Și un experiment nu se poate realiza aici, pentru că în experiment nu avem dreptul să efectuăm primul pas, sarcina fiind definită dinainte.
În specificațiile informale, este ușor să nu țineți cont de multe dificultăți. Nu e nimic complicat în a scrie specificații stricte pentru funcții, nu voi discuta asta. În schimb, vom vorbi despre scrierea specificațiilor stricte pentru modelele comportamentale standard. Există o teoremă care afirmă că orice mulțime de comportamente poate fi descrisă prin proprietăți de siguranță (safety) și proprietăți de durabilitate (liveness). Securitatea înseamnă că nu se va întâmpla nimic rău, programul nu va da un răspuns incorrect. Viabilitatea înseamnă că, mai devreme sau mai târziu, se va întâmpla ceva bun, adică programul va oferi în cele din urmă un răspuns corect. De obicei, securitatea este un indicator mai important, iar erorile apar cel mai frecvent aici. De aceea, pentru a economisi timp, nu voi vorbi despre viabilitate, deși aceasta este, desigur, importantă.
Obținem securitate specificând, pe de o parte, numeroase stări inițiale posibile. Și, pe de altă parte, relațiile cu toate stările următoare posibile pentru fiecare stare. Ne vom comporta ca niște oameni de știință și vom defini stările matematic. Setul de stări inițiale este descris printr-o formulă, de exemplu, în cazul algoritmului lui Euclid: (x = M) ∧ (y = N). Pentru anumite valori M și N există doar o singură stare inițială. Relația cu starea următoare este descrisă de o formulă în care variabilele stării următoare sunt scrise cu apostrof, iar cele ale stării curente fără apostrof. În cazul algoritmului lui Euclid, vom avea de-a face cu o disjuncție a două formule, în una dintre care x este valoarea maximă, iar în cealaltă — Stabiliți o parolă și păstrați-o în siguranță!:
În primul caz, noua valoare y este egală cu valoarea anterioară a lui y, iar noua valoare x o obținem scăzând din variabila mai mare pe cea mai mică. În al doilea caz, facem invers.
Să ne întoarcem la algoritmul lui Euclid. Să presupunem din nou că M = 12, N = 18. Aceasta determină o singură stare inițială, (x = 12) ∧ (y = 18). Apoi, introducem aceste valori în formula de mai sus și obținem:
Aici, singura soluție posibilă este: x' = 18 - 12 ∧ y' = 12, și obținem comportarea: [x = 12, y = 18]. La fel, putem descrie toate stările din comportamentul nostru: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
În ultima stare [x = 6, y = 6] ambele părți ale expresiei vor fi false, deci nu va exista o stare următoare. Așadar, avem o specificație completă a celui de-al doilea pas — așa cum vedem, este matematică destul de obișnuită, ca la ingineri și oameni de știință, nu ciudată, așa cum este în știința computerelor.
Aceste două formule pot fi unite într-o singură formulă de logică temporală. Este elegantă și explicarea ei nu este dificilă, însă nu avem timp pentru asta acum. Logica temporală ne-ar putea fi necesară doar pentru proprietatea de viu, pentru siguranță nu este nevoie. Logica temporală, ca atare, nu este pe placul meu, nu este o matematică complet obișnuită, dar în cazul vieții ea este un rău necesar.
În algoritmul lui Euclid pentru fiecare valoare x și Stabiliți o parolă și păstrați-o în siguranță! există valori unice x' și y', care fac ca relația cu următoarea stare să fie adevărată. Cu alte cuvinte, algoritmul lui Euclid este determinist. Pentru a modela un algoritm nedeterminist, trebuie ca starea curentă să aibă mai multe stări viitoare posibile, iar fiecare valoare a variabilei fără cratimă să aibă mai multe valori ale variabilei cu cratimă, pentru care relația cu următoarea stare este adevărată. Nu este greu de realizat, dar acum nu voi da exemple.
Pentru a crea un instrument funcțional, este necesară o matematică formală. Cum putem face o specificație formală? Pentru asta ne va trebui un limbaj formal, de exemplu, . Specificația algoritmului lui Euclid va arăta astfel în acest limbaj:
Simbolul semnului egal cu triunghi indică faptul că valoarea din stânga semnului este definită ca fiind egală cu valoarea din dreapta semnului. Practic, specificația este o definiție, în cazul nostru două definiții. Specificației în TLA+ trebuie să-i adăugăm declarații și o anumită sintaxă, ca în diapozitivul de mai sus. În ASCII, aceasta va arăta astfel:
După cum vedem, nu este nimic complicat. Specificația în TLA+ poate fi verificată, adică se pot explora toate comportamentele posibile într-un model mic. În cazul nostru, acest model va fi valori definite M și N. Este o metodă foarte eficientă și simplă de verificare, care se desfășoară complet automat. În plus, se pot scrie dovezi formale ale adevărului și se pot verifica mecanic, dar pentru asta este nevoie de mult timp, de aceea aproape nimeni nu face asta.
Principalul dezavantaj al TLA+ este că este matematică, iar programatorii și informaticienii se tem de matematică. La prima vedere, poate suna ca o glumă, dar, din păcate, o spun complet serios. Colegul meu tocmai mi-a povestit cum a încercat să explice TLA+ câtorva dezvoltatori. De îndată ce formulele au apărut pe ecran, ochii lor au devenit vid. Așa că, dacă TLA+ intimidează, se poate folosi , care este un fel de limbaj de programare pentru jocuri. O expresie în PlusCal poate fi orice expresie TLA+, adică, în mare parte, orice expresie matematică. În plus, PlusCal dispune de o sintaxă pentru algoritmi nedeterministici. Datorită faptului că în PlusCal se poate scrie orice expresie TLA+, acesta este semnificativ mai expresiv decât orice limbaj de programare real. Mai mult, PlusCal se compilează într-o specificație TLA+ ușor de citit. Aceasta nu înseamnă, desigur, că o specificație complexă PlusCal se va transforma într-una simplă pe TLA+ — doar că corespondența dintre ele este evidentă, fără a apărea complexitate suplimentară. În cele din urmă, această specificație poate fi verificată cu uneltele TLA+. În general, PlusCal poate ajuta la depășirea fobiei matematice, fiind ușor de înțeles chiar și pentru programatori și informaticieni. În trecut, am publicat algoritmi folosind acest limbaj timp de aproximativ 10 ani.
Poate că cineva ar putea obiecta că TLA+ și PlusCal sunt matematică și că matematica funcționează doar cu exemple inventate. Totuși, în practică este nevoie de un limbaj real cu tipuri, proceduri, obiecte și așa mai departe. Nu este adevărat. Iată ce scrie Chris Newcomb, care a lucrat la Amazon: „Am folosit TLA+ în zece proiecte mari, iar în fiecare caz utilizarea sa a contribuit semnificativ la dezvoltare, deoarece am reușit să prindem bug-uri periculoase înainte de a ajunge în producție și pentru că ne-a oferit înțelegerea și încrederea necesare pentru optimizări agresive ale performanței, fără a afecta corectitudinea programului.”. Adesea se aude că utilizarea metodelor formale duce la cod ineficient — în practică, cu totul opus. În plus, există o opinie conform căreia este imposibil să convingi managerii de necesitatea metodelor formale, chiar dacă programatorii sunt convinsi de utilitatea lor. Iar Newcomb scrie: „Managerii acum îndeamnă pe toată lumea să scrie specificații în TLA+, și alocă în mod special timp pentru aceasta“. Așadar, când managerii observă că TLA+ funcționează, îl acceptă cu bucurie. Chris Newcomb a scris asta acum aproximativ șase luni (în octombrie 2014), iar acum, cât știu eu, TLA+ este utilizat în 14 proiecte, nu 10. Un alt exemplu se referă la proiectarea Xbox 360. Un stagiar a venit la Charles Ticker și a scris o specificație pentru sistemul de memorie. Datorită acestui document, a fost descoperită o eroare care altfel ar fi trecut neobservată, și din cauza căreia fiecare Xbox 360 s-ar fi prăbușit după patru ore de utilizare. Inginerii de la IBM au confirmat că testele lor nu ar fi descoperit această eroare.
Puteți citi mai multe despre TLA+ pe internet, dar acum haideți să discutăm despre specificațiile informale. Rareori suntem nevoiți să scriem programe care calculează cel mai mare divizor comun și lucruri de genul acesta. Mult mai des scriem programe precum un instrument de formatare (pretty-printer), pe care l-am scris pentru TLA+. După cea mai simplă procesare, codul TLA+ ar arăta în felul următor:
Dar în exemplul dat, utilizatorul ar fi vrut cel mai probabil ca simbolurile de conjuncție și egalitate să fie aliniate. Așadar, formatul corect ar arăta mai degrabă așa:
Să luăm în considerare un alt exemplu:
Aici, dimpotrivă, alinierea simbolurilor de egalitate, adunare și înmulțire în sursă a fost aleatorie, așa că cea mai simplă procesare este suficientă. În general, nu există o definiție matematică exactă a unui format corect, deoarece „corect” în acest caz înseamnă „așa cum își dorește utilizatorul”, iar acest lucru nu poate fi definit matematic.
Se pare că, dacă nu avem o definiție a veridicității, specificația este inutilă. Dar nu este așa. Dacă nu știm ce ar trebui să facă programul, nu înseamnă că nu trebuie să ne gândim la modul său de funcționare — dimpotrivă, ar trebui să investim și mai mult efort. Specificația este aici deosebit de importantă. Nu putem determina programul optim pentru formatarea structurală, dar asta nu înseamnă că nu ar trebui să ne ocupăm deloc de asta, iar a scrie cod ca un flux de conștiință nu este o soluție. În cele din urmă, am scris o specificație din șase reguli cu definiții sub formă de comentarii în fișierul Java. Iată un exemplu al uneia dintre reguli: un token de comentariu stâng este LeftComment aliniat cu tokenul său de acoperire. Această regulă este scrisă într-un, să-i spunem, englezesc matematic: LeftComment aliniat, comentariu stâng și token de acoperire — termeni cu definiții. Așa cum matematicienii descriu matematica: scriu definiții ale termenilor și pe baza acestora — reguli. Avantajul unei astfel de specificații este că este mult mai ușor să înțelegi și să depanezi șase reguli decât 850 de linii de cod. Trebuie spus că a redacta aceste reguli a fost dificil, a durat destul de mult timp pentru a le depana. Special pentru acest scop, am scris un cod care raportează ce regulă este utilizată. Datorită faptului că am verificat aceste șase reguli pe câteva exemple, nu a trebuit să depanez 850 de linii de cod, iar bug-urile s-au dovedit a fi destul de ușor de găsit. În Java, există instrumente excelente pentru asta. Dacă aș fi scris doar cod, mi-ar fi luat mult mai mult timp și formatarea ar fi fost de o calitate inferioară.
De ce nu s-a putut folosi specificația formală? Pe de o parte, corectitudinea execuției aici nu este foarte importantă. Imprimarea structurală va deranja cu siguranță pe cineva, așa că nu a trebuit să mă asigur că funcționează corect în toate situațiile neobișnuite. Mai important este faptul că nu am avut instrumentele adecvate. Un instrument pentru verificarea modelelor TLA+ este inutil aici, așa că ar fi trebuit să scriu manual exemple.
Specificația prezentată are trăsături comune cu toate specificațiile. Este la un nivel superior față de cod. Poate fi implementată în orice limbaj. Pentru a o redacta, nu sunt utile niciun fel de instrumente sau metode. Niciun curs de programare nu te va ajuta să redactezi această specificație. Și nu există instrumente care să facă această specificație inutilă, cu excepția cazului în care scrii un limbaj special pentru redactarea programelor de imprimare structurală în TLA+. În cele din urmă, această specificație nu spune nimic despre cum vom scrie codul, ea doar indică ce face acest cod. Scriem specificația pentru a ne ajuta să gândim problema înainte de a începe să ne gândim la cod.
Dar această specificație are și trăsături care o diferențiază de alte specificații. 95% din alte specificații sunt semnificativ mai scurte și mai simple:
În continuare, această specificație este un set de reguli. De obicei, acesta este un semn al unei specificații slabe. Înțelegerea consecințelor unui set de reguli este destul de dificilă, iar din acest motiv am fost nevoit să petrec mult timp la debugarea lor. Cu toate acestea, în acest caz, nu am găsit o modalitate mai bună.
Merită să spun câteva cuvinte despre programele care funcționează continuu. De obicei, acestea funcționează în paralel, cum ar fi sistemele de operare sau sistemele distribuite. Foarte puțini pot să se descurce cu ele în minte sau pe hârtie, iar eu nu fac parte din această categorie, deși cândva îmi era ușor. De aceea sunt necesare instrumente care să verifice munca noastră — de exemplu, TLA+ sau PlusCal.
De ce a fost nevoie să scriu o specificație, dacă știați deja ce ar trebui să facă codul? De fapt, doar mi se părea că știu. În plus, având o specificație, o persoană din afară nu mai are nevoie să se bage în cod pentru a înțelege ce face acesta. Am o regulă: nu ar trebui să existe reguli generale. Această regulă are evident o excepție, care este singura regulă generală pe care o respect: specificația a ceea ce face codul trebuie să ofere oamenilor tot ceea ce trebuie să știe atunci când folosesc acest cod.
Deci, ce trebuie să știe programatorii despre gândire? În primul rând, același lucru ca toată lumea: dacă nu scrii, doar îți închipui că gândești. În plus, trebuie să gândești înainte de a codifica, ceea ce înseamnă că trebuie să scrii înainte de a codifica. Specificația este ceea ce scriem înainte de a începe să codificăm. O specificație este necesară pentru orice cod care poate fi folosit sau modificat de cineva. Iar acel „cineva” poate fi chiar autorul codului, la o lună după scrierea acestuia. O specificație este necesară pentru programe și sisteme mari, pentru clase, pentru metode și uneori chiar pentru porțiuni complexe dintr-o metodă individuală. Ce trebuie să scriem despre cod? Trebuie să descriem ce face, adică ceea ce poate fi util oricărei persoane care folosește acest cod. Uneori, poate fi, de asemenea, necesar să indicăm cum anume codul își atinge scopul. Dacă aceasta metodă a fost studiată în cursul algoritmilor, atunci numim asta algoritm. Dacă este ceva mai special și nou, atunci o numim proiectare la un nivel înalt. Nu există o diferență formală aici: ambele sunt modele abstracte ale programului.
Cum ar trebui să scriem specificația codului? Principalul: trebuie să fie cu un nivel mai sus decât codul în sine. Aceasta trebuie să descrie stările și comportamentele. Trebuie să fie la fel de riguroasă cât cere sarcina. Dacă scrieți o specificație a modulului de realizare a sarcinii, atunci o puteți scrie în pseudocod sau folosind PlusCal. Trebuie să învățați să scrieți specificații pe baza specificațiilor formale. Aceasta vă va oferi abilitățile necesare, care vor ajuta și cu cele informale. Și cum învățăm să scriem specificații formale? Atunci când învățam programarea, scriam programe și apoi le debbugam. Același lucru se aplică aici: trebuie să scrieți o specificație, să o verificați folosind un instrument de verificare a modelului și să corectați erorile. TLA+ nu este, poate, cel mai bun limbaj pentru specificații formale, iar pentru nevoile dvs. specifice s-ar putea să fie mai potrivit un alt limbaj. Avantajul TLA+ este că învață excelent gândirea matematică.
Cum să legați specificațiile de cod? Prin comentarii care corelează conceptele matematice cu implementarea lor. Dacă lucrați cu grafuri, veți avea, la nivel de program, matrice de noduri și matrice de legături. Prin urmare, trebuie să scrieți cum este implementat graf în aceste structuri de programare.
Este important de menționat că nimic din cele de mai sus nu se referă la procesul de scriere a codului. Atunci când scrieți cod, adică atunci când executați al treilea pas, trebuie, de asemenea, să gândiți și să planificați programul. Dacă o subtaskă se dovedește a fi complicată sau neclară, trebuie să scrieți o specificație pentru aceasta. Dar nu vorbesc aici despre codul în sine. Puteți folosi orice limbaj de programare, orice metodologie, nu despre asta este vorba. În plus, nimic din cele de mai sus nu scutește de necesitatea de a testa și debugga codul. Chiar dacă modelul abstract este scris corect, în implementarea sa pot apărea bug-uri.
Scrierea specificațiilor este o etapă suplimentară în procesul de scriere a codului. Datorită acesteia, multe erori pot fi detectate cu mai puțin efort — știm aceasta din experiența programatorilor de la Amazon. Cu specificații, calitatea programelor devine mai bună. Atunci, de ce ne descurcăm atât de des fără ele? Pentru că este greu să scrii. Și este greu să scrii pentru că trebuie să gândești, iar a gândi este, de asemenea, greu. Întotdeauna este mai simplu să faci că gândești. Aici se poate trasa o analogie cu alergatul — cu cât alergi mai puțin, cu atât alergi mai încet. Trebuie să îți antrenezi mușchii și să exersezi scrisul. Este nevoie de practică.
Specificația poate fi greșită. Este posibil să fi făcut o greșeală undeva sau cerințele s-au putut schimba sau a fost necesară vreo îmbunătățire. Orice cod pe care cineva îl utilizează trebuie modificat, așa că, mai devreme sau mai târziu, specificația va înceta să corespundă programului. Ideal, în acest caz, ar trebui să scrieți o nouă specificație și să rescrieți complet codul. Știm foarte bine că nimeni nu face așa. În practică, reparăm codul și, poate, actualizăm specificația. Dacă acest lucru este obligatoriu s-o faci mai devreme sau mai târziu, atunci de ce să scrii specificații? În primul rând, pentru persoana care va modifica codul tău, fiecare cuvânt de prisos în specificație va fi inestimabil, iar acea persoană poți fi chiar tu. Mă cert adesea că nu am scris o specificație suficientă când editez codul meu. Și scriu mai multe specificații decât cod. Așadar, când editezi codul, specificația trebuie actualizată întotdeauna. În al doilea rând, cu fiecare modificare, codul devine mai rău, devine din ce în ce mai greu de citit și de întreținut. Aceasta este o acumulare de entropie. Dar dacă nu începi cu o specificație, atunci fiecare linie scrisă va fi o modificare, iar codul va fi de la bun început voluminos și greu de citit.
Așa cum spunea , nicio bătălie nu a fost câștigată conform planului, și nicio bătălie nu a fost câștigată fără un plan. Iar el știa câte ceva despre bătălii. Există o părere că scrierea specificațiilor este o pierdere de timp. Uneori este într-adevăr așa, iar sarcina este atât de simplă încât nu este necesar să te gândești prea mult la ea. Dar trebuie să ții mereu minte că, atunci când ți se recomandă să nu scrii specificații, ți se recomandă de fapt să nu gândești. Și acest lucru merită să fie gândit de fiecare dată. Gândirea la sarcină nu garantează că nu vei face greșeli. Așa cum știm, nimeni nu a inventat o baghetă magică, iar programarea este o activitate complexă. Dar dacă nu te gândești la sarcină, vei face cu siguranță greșeli.
Mai multe despre TLA+ și PlusCal pot fi citite pe un site special, la care poți ajunge de pe pagina mea de start . Asta e tot din partea mea, mulțumesc pentru atenție.
Vă reamintesc că acesta este un traducere. Atunci când vă scrieți comentariile, amintiți-vă că autorul acestora nu le va citi. Dacă doriți cu adevărat să comunicați cu autorul, acesta va fi la conferința Hydra 2019, care va avea loc pe 11-12 iulie 2019 în Sankt Petersburg. Biletele pot fi achiziționate .
Sursa: habr.com
