Questu articulu hè una traduzzione . Ma davanti à ella una piccula presentazione. Cumu sò formati i zombies? Ognunu si mette in una situazione induve volenu tirà un amicu o un cullegu finu à u so livellu, ma ùn viaghja micca. È ùn hè micca tantu cun voi cum'è cun ellu chì "ùn funziona micca": da una parte di a scala hè un salariu normale, compiti, è cusì, è da l'altru, a necessità di pensà. U pensamentu hè dispiacevule è doloroso. Rinunce rapidamente è cuntinueghja à scrive codice senza accende u cervellu. Immaginate quantu sforzu ci vole à superà a barrera di l'impotenza appresa, è ùn fate micca solu. Hè cusì chì i zombies sò furmati, chì, pare, ponu esse guariti, ma pare chì nimu hà da fà.
Quandu aghju vistu chì (iè, u listessu camarade di i libri di testu) è ùn face micca un rapportu, ma una sessione di dumande è risposte, era un pocu attentu. Solu in casu, Leslie hè un scientist famosu in u mondu sanu, l'autore di l'opere fundamentale in l'informatica distribuita, è pudete ancu cunnosce cù e lettere La in a parolla LaTeX - "Lamport TeX". U sicondu fattore alarmante hè u so esigenza: tutti quelli chì venenu devenu (assolutamente gratuitu) à sente un paru di i so rapporti in anticipu, vene cun almenu una quistione nantu à elli, è solu dopu vene. Aghju decisu di vede ciò chì Lamport trasmette quì - è hè fantasticu! Hè esattamente quella cosa, a pillola magica di link per curà i zombies. Vi avvistu: da u testu, l'amatori di metodulugii super-flexibili è quelli chì ùn piacenu micca à pruvà ciò chì hè scrittu ponu notevolmente brusgià.
Dopu à l'habrokat, in fattu, a traduzzione di u seminariu principia. Prufittate a lettura!
Qualunque sia u compitu chì pigliate, avete sempre bisognu di passà per trè passi:
- decide quale scopu vulete ghjunghje;
- decide cumu uttene u vostru scopu;
- vene à u vostru scopu.
Questu hè ancu applicà à a prugrammazione. Quandu scrivimu codice, avemu bisognu di:
- decide ciò chì u prugramma deve fà;
- determinà cumu si deve fà u so compitu;
- scrive u codice currispundente.
L'ultimu passu, sicuru, hè assai impurtante, ma ùn ne parleraghju micca oghje. Invece, discutemu i primi dui. Ogni programatore li eseguisce prima di cumincià à travaglià. Ùn site micca pusatu per scrive, salvu chì ùn avete decisu s'ellu scrive un navigatore o una basa di dati. Una certa idea di u scopu deve esse presente. È definitivamente pensate à ciò chì esattamente u prugramma farà, è ùn scrive micca in una certa manera in a speranza chì u codice diventerà in qualchì modu in un navigatore.
Cumu hè esattamente questu codice pre-pensante succede? Quantu sforzu duvemu mette in questu? Tuttu dipende di quantu cumplessu u prublema risolvemu. Suppone chì vulemu scrive un sistema distribuitu tolerante à i difetti. In questu casu, duvemu pensà à e cose cù cura prima di pusà à u codice. E s'ellu ci hè solu bisognu di incrementà una variabile intera da 1? À u primu sguardu, tuttu hè triviale quì, è ùn ci hè bisognu di pensà, ma poi ricurdemu chì un overflow pò accade. Dunque, ancu per capiscenu s'ellu un prublema hè simplice o cumplessu, avete prima bisognu di pensà.
Se pensate à e pussibuli suluzioni à u prublema in anticipu, pudete evitari i sbagli. Ma questu hè bisognu chì u vostru pensamentu sia chjaru. Per ottene questu, avete bisognu di scrive i vostri pinsamenti. Mi piace assai a citazione di Dick Guindon: "Quandu scrivi, a natura ti mostra quantu hè sloppy u vostru pensamentu". Se ùn scrivite micca, pensate solu chì pensate. È avete bisognu di scrive i vostri pinsamenti in forma di specificazioni.
E specificazioni facenu parechje funzioni, in particulare in grandi prughjetti. Ma parlu solu di unu di elli: ci aiutanu à pensà chjaramente. Pensà chjaramente hè assai impurtante è abbastanza difficiule, cusì quì avemu bisognu di aiutu. In quale lingua duvemu scrive e specificazioni? In generale, questu hè sempre a prima quistione per i programatori: in quale lingua scriveremu. Ùn ci hè una risposta curretta à questu: i prublemi chì risolvemu sò troppu diversi. Per alcuni, TLA + hè una lingua di specificazione chì aghju sviluppatu. Per altri, hè più còmuda di utilizà u cinese. Tuttu dipende di a situazione.
A più impurtante hè una altra quistione: cumu per ottene un pensamentu più chjaru? Risposta: Avemu da pensà cum'è scientisti. Questu hè un modu di pensà chì hà pruvatu in l'ultimi 500 anni. In a scienza, custruemu mudelli matematichi di a realità. L'astronomia era forse a prima scienza in u sensu strettu di a parolla. In u mudellu matimàticu utilizatu in l'astronomia, i corpi celesti appariscenu cum'è punti cù massa, pusizioni è momentum, ancu s'ellu in realtà sò ogetti estremamente cumplessi cù muntagne è oceani, maree è maree. Stu mudellu, cum'è qualsiasi altru, hè statu creatu per risolve certi prublemi. Hè grande per determinà induve puntà u telescopiu se avete bisognu di truvà un pianeta. Ma s'è vo vulete predice u tempu nantu à stu pianeta, stu mudellu ùn hà micca travagliatu.
A matematica ci permette di determinà e proprietà di u mudellu. È a scenza mostra cumu queste proprietà sò in relazione cù a realità. Parlemu di a nostra scienza, di l'informatica. A realità cù quale travagliammu hè sistemi di computing di varii tipi: processori, console di ghjocu, computer, esecutivu di prugrammi, etc. Parlaraghju di eseguisce un prugramma in un computer, ma in generale, tutte queste cunclusioni s'applicanu à qualsiasi sistema di computing. In a nostra scienza, avemu aduprà parechji mudelli diffirenti: a macchina di Turing, insemi parzialmente urdinati di avvenimenti, è assai altri.
Chì ghjè un prugramma? Questu hè qualsiasi codice chì pò esse cunsideratu indipindente. Suppone chì avemu bisognu di scrive un navigatore. Facemu trè compiti: cuncepemu a vista di l'utilizatori di u prugramma, dopu scrivemu u diagramma di altu livellu di u prugramma, è infine scrivimu u codice. Mentre scrivemu u codice, avemu capitu chì avemu bisognu di scrive un formattatore di testu. Quì avemu di novu bisognu di risolve trè prublemi: determinà quale testu torna stu strumentu; selezziunà un algoritmu per furmatu; scrive u codice. Stu compitu hà u so propiu subtask: inserisci currettamente un trattino in parolle. Risolvemu ancu questu subtask in trè passi - cum'è pudete vede, sò ripetuti à parechji livelli.
Fighjemu in più detail u primu passu: quale prublema risolve u prugramma. Quì, u più spessu modellu un prugramma cum'è una funzione chì piglia qualchì input è pruduce qualchì output. In matematica, una funzione hè generalmente descritta cum'è un inseme urdinatu di coppie. Per esempiu, a funzione di quadratura per i numeri naturali hè descritta cum'è l'inseme {<0,0>, <1,1>, <2,4>, <3,9>, ...}. U duminiu di una tale funzione hè u settore di i primi elementi di ogni paru, vale à dì i numeri naturali. Per definisce una funzione, avemu bisognu di specificà u so scopu è a formula.
Ma e funzioni in matematica ùn sò micca listessi cum'è funzioni in linguaggi di prugrammazione. A matematica hè assai più faciule. Siccomu ùn aghju micca tempu per esempi cumplessi, cunsideremu un simplice: una funzione in C o un metudu staticu in Java chì torna u più grande divisore cumuni di dui interi. In a specificazione di stu metudu, scriveremu: calcula GCD(M,N) per argumenti M и Ninduve GCD(M,N) - una funzione chì u duminiu hè l'inseme di coppie di numeri interi, è u valore di ritornu hè u più grande integer chì hè divisibile per M и N. Cumu hè questu mudellu in relazione à a realità? U mudellu opera nantu à interi, mentri in C o Java avemu un 32-bit int. Stu mudellu ci permette di decide se l'algoritmu hè currettu GCD, ma ùn impedisce micca l'errori di overflow. Questu averebbe bisognu di un mudellu più cumplessu, per quale ùn ci hè micca tempu.
Parlemu di e limitazioni di una funzione cum'è mudellu. Certi prugrammi (cum'è i sistemi operativi) ùn tornanu micca solu un certu valore per certi argumenti, ponu esse cuntinuu. Inoltre, a funzione cum'è un mudellu ùn hè micca bè adattatu per u sicondu passu: pianificà cumu risolve u prublema. A sorta rapida è a sorta di bolle calculanu a stessa funzione, ma sò algoritmi completamente differenti. Per quessa, per discrive cumu u scopu di u prugramma hè rializatu, aghju utilizatu un mudellu diversu, chjamemu u mudellu di cumportamentu standard. U prugramma in questu hè rapprisintatu cum'è un inseme di tutti i cumpurtamenti permissibili, ognunu di i quali, à u turnu, hè una sequenza di stati, è u statu hè l'assignazione di valori à variàbili.
Videmu ciò chì u sicondu passu per l'algoritmu di Euclide pare. Avemu bisognu di calculà GCD(M, N). Avemu inizializatu M quantu xe N quantu y, poi sottrae ripetutamente u più chjucu di sti variàbili da u più grande finu à ch'elli sò uguali. Per esempiu, se M = 12e N = 18, pudemu discrive u cumportamentu seguente:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
E si M = 0 и N = 0? Zeru hè divisibule da tutti i numeri, cusì ùn ci hè micca u più grande divisore in questu casu. In questa situazione, avemu bisognu di vultà à u primu passu è dumandà: avemu veramente bisognu di calculà GCD per i numeri non pusitivi? Se questu ùn hè micca necessariu, allora basta à cambià a specificazione.
Quì duvemu fà una piccula digressione nantu à a produtividade. Hè spessu misurata in u numeru di linee di codice scritte per ghjornu. Ma u vostru travagliu hè assai più utile si sbarazzate di un certu numaru di linii, perchè avete menu spaziu per i bug. È u modu più faciule per sguassà u codice hè in u primu passu. Hè interamente pussibule chì ùn avete micca bisognu di tutte e campane è fischi chì pruvate à implementà. U modu più veloce per simplificà un prugramma è risparmià tempu hè di ùn fà micca cose chì ùn deve micca esse fattu. U sicondu passu hè u sicondu u putenziale di risparmiu di tempu. Se misurate a produtividade in termini di linee scritte, allora pensendu à cumu fà un compitu vi farà menu pruduttivu, perchè pudete risolve u listessu prublema cù menu codice. Ùn possu micca dà statistiche precise quì, perchè ùn aghju micca manera di cuntà u nùmeru di linii chì ùn aghju micca scrittu per u fattu chì aghju passatu u tempu nantu à a specificazione, vale à dì à u primu è u sicondu passu. È l'esperimentu ùn pò esse stallatu ancu quì, perchè in l'esperimentu ùn avemu micca u dirittu di compie u primu passu, u compitu hè predeterminatu.
Hè facilitu trascuratà parechje difficultà in specificazioni informali. Ùn ci hè nunda difficiule à scrive specificazioni strette per e funzioni, ùn discuteraghju micca questu. Invece, parleremu di scrive specificazioni forti per i cumpurtamenti standard. Ci hè un teorema chì dice chì ogni inseme di cumpurtamenti pò esse discrittu cù a pruprietà di sicurità (sicurezza) e proprietà di sopravvivenza (vivenza). Sicurezza significa chì nunda di male ùn succederà, u prugramma ùn darà micca una risposta incorrecta. A sopravvivenza significa chì prima o poi qualcosa di bonu succederà, vale à dì chì u prugramma darà a risposta curretta prima o dopu. In regula, a sicurità hè un indicatore più impurtante, l'errori sò più spessu quì. Dunque, per risparmià tempu, ùn parleraghju micca di survivabilità, ancu s'ellu hè, sicuru, ancu impurtante.
Ottenemu a sicurità per prescribe, prima, l'inseme di stati iniziali pussibuli. E siconda, relazioni cù tutti i stati pussibuli per ogni statu. Facemu cum'è scientisti è definisce stati matematicamente. L'inseme di stati iniziali hè discritta da una formula, per esempiu, in u casu di l'algoritmu Euclide: (x = M) ∧ (y = N). Per certi valori M и N ci hè solu un statu iniziale. A rilazioni cù u prossimu statu hè scritta da una formula in quale i variàbili di u prossimu statu sò scritti cù un primu, è e variàbili di u statu attuale sò scritti senza un primu. In u casu di l'algoritmu di Euclide, avemu da trattà cù a disjunzione di duie formule, in una di quali x hè u valore più grande, è in u sicondu - y:
In u primu casu, u novu valore di y hè uguali à u valore precedente di y, è avemu u novu valore di x sottraendu a variabile più chjuca da a variabile più grande. In u sicondu casu, facemu u cuntrariu.
Riturnemu à l'algoritmu di Euclide. Assumimu di novu chì M = 12, N = 18. Questu definisce un unicu statu iniziale, (x = 12) ∧ (y = 18). Dopu inserimu quelli valori in a formula sopra è uttene:
Eccu l'unica suluzione pussibule: x' = 18 - 12 ∧ y' = 12è avemu u cumpurtamentu: [x = 12, y = 18]. In listessu modu, pudemu discrive tutti i stati in u nostru cumpurtamentu: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
In l'ultimu statu [x = 6, y = 6] e duie parte di l'espressione seranu falsi, perchè ùn hà micca statu prossimu. Dunque, avemu una specificazione cumpleta di u sicondu passu - cum'è pudete vede, questu hè una matematica abbastanza ordinaria, cum'è in ingegneri è scientisti, è micca strana, cum'è in l'informatica.
Sti dui formule ponu esse cumminati in una formula di logica tempurale. Hè elegante è faciule da spiegà, ma ùn ci hè micca tempu per ella avà. Pudemu bisognu di logica tempurale solu per a pruprietà di vivacità, ùn hè micca necessariu per a sicurità. Ùn mi piace micca a logica tempurale cum'è tale, ùn hè micca abbastanza matematica ordinaria, ma in u casu di vivacità hè un male necessariu.
In l'algoritmu di Euclide, per ogni valore x и y avè valori unichi x' и y', chì facenu a relazione cù u prossimu statu veru. In altri palori, l'algoritmu di Euclide hè deterministicu. Per mudificà un algoritmu non-deterministicu, u statu attuale hà bisognu à avè parechje stati futuri pussibuli, è chì ogni valore variabile unprimed hà parechji valori variabili primati tali chì a relazione cù u prossimu statu hè vera. Questu hè faciule da fà, ma ùn daraghju micca esempi avà.
Per fà un strumentu di travagliu, avete bisognu di matematica formale. Cumu fà a specificazione formale? Per fà questu, avemu bisognu di una lingua formale, per esempiu, . A specificazione di l'algoritmu d'Euclidi pareva cusì in questa lingua:
Un simbulu di signu uguali cù un triangulu significa chì u valore à a manca di u signu hè definitu per esse uguali à u valore à a diritta di u signu. In essenza, a specificazione hè una definizione, in u nostru casu duie definizioni. À a specificazione in TLA +, avete bisognu di aghjunghje dichjarazioni è qualchì sintassi, cum'è in a slide sopra. In ASCII serebbe cusì:
Comu pudete vede, nunda di complicatu. A specificazione per TLA + pò esse pruvata, vale à dì aggira tutti i cumpurtamenti pussibuli in un picculu mudellu. In u nostru casu, stu mudellu serà certu valori M и N. Questu hè un metudu di verificazione assai efficace è simplice chì hè completamente automaticu. Hè ancu pussibule di scrive e prove di verità formale è cuntrollanu meccanicamente, ma questu pigghia assai tempu, cusì quasi nimu ùn face questu.
U principale svantaghju di TLA + hè chì hè matematica, è i programatori è l'informatica anu a paura di a matematica. À u primu sguardu, questu sona cum'è un scherzu, ma, sfurtunatamenti, dicu in tutta a seriu. U mo cullega mi diceva solu cumu hà pruvatu à spiegà TLA + à parechji sviluppatori. Appena e formule apparsu nantu à u screnu, subitu diventanu ochji vetru. Allora se TLA + ti spaventa, pudete aduprà , hè una specie di lingua di prugrammazione di ghjoculi. Una espressione in PlusCal pò esse qualsiasi espressione TLA+, vale à dì, in generale, qualsiasi espressione matematica. Inoltre, PlusCal hà una sintassi per algoritmi non deterministici. Perchè PlusCal pò scrive qualsiasi espressione TLA+, PlusCal hè assai più espressivu chè qualsiasi lingua di prugrammazione reale. Dopu, PlusCal hè cumpilatu in una specificazione TLA + facilmente leggibile. Questu ùn significa micca, sicuru, chì a specificazione cumplessa PlusCal diventerà in una simplicità in TLA + - solu a currispundenza trà elli hè ovvia, ùn ci sarà micca cumplessità supplementu. Infine, sta specificazione pò esse verificata da i strumenti TLA +. In tuttu, PlusCal pò aiutà à superà a fobia di matematica è hè faciule da capisce ancu per i programatori è l'informatica. In u passatu, aghju publicatu algoritmi nantu à questu per qualchì tempu (circa 10 anni).
Forsi qualcunu hà da ughjettu chì TLA + è PlusCal sò matematiche, è a matematica travaglia solu nantu à esempi inventati. In pratica, avete bisognu di una lingua vera cù tipi, prucedure, ogetti, etc. Questu hè sbagliatu. Eccu ciò chì Chris Newcomb, chì hà travagliatu in Amazon, scrive: "Avemu utilizatu TLA + in dece prughjetti maiò, è in ogni casu, u so usu hà fattu una differenza significativa per u sviluppu perchè eramu capaci di catturà bug periculosi prima di ghjunghje à a produzzione, è perchè ci hà datu l'intuizione è a fiducia chì avemu bisognu Fate ottimisazioni aggressive di rendiment senza affettà a verità di u prugramma ". Pudete spessu sente chì quandu si usa i metudi formali, avemu un codice inefficace - in pratica, tuttu hè esattamente u cuntrariu. Inoltre, ci hè una opinione chì i gestori ùn ponu micca cunvinta di a necessità di metudi formali, ancu s'è i programatori sò cunvinti di a so utilità. È Newcomb scrive: "I gestori sò avà spinghjendu duramente per scrive specificazioni per TLA +, è specificamente attribuisce u tempu per questu". Allora, quandu i gestori vedenu chì TLA+ funziona, sò felici di accettà. Chris Newcomb hà scrittu questu circa sei mesi fa (uttobre 2014), ma avà, quantu a so, TLA + hè utilizatu in 14 prughjetti, micca 10. Un altru esempiu hè in u disignu di l'XBox 360. Un internu hè vinutu à Charles Thacker è hà scrittu specificazioni per u sistema di memoria. Grazie à questa specificazione, hè statu trovu un bug chì altrimenti passassi inosservatu, è per via di quale ogni XBox 360 s'avaria dopu à quattru ore di usu. L'ingegneri IBM anu cunfirmatu chì e so teste ùn anu micca truvatu stu bug.
Pudete leghje più nantu à TLA + in Internet, ma avà parlemu di specificazioni informali. Avemu raramente à scrive prugrammi chì calculanu u minimu divisore cumuni è simili. Moltu più spessu scrivemu prugrammi cum'è l'utile di stampante bella chì aghju scrittu per TLA +. Dopu à u più simplice di trasfurmazioni, u codice TLA + parerebbe cusì:
Ma in l'esempiu di sopra, l'utilizatore assai prubabilmente vulia chì a cunghjunzione è i segni uguali sò allinati. Allora u furmatu currettu parerebbe più cusì:
Cunsideremu un altru esempiu:
Quì, à u cuntrariu, l'alineazione di l'uguali, l'aghjunzione è i segni di multiplicazione in a fonte era casuale, cusì u prucessu più simplice hè abbastanza. In generale, ùn ci hè micca una definizione matematica esatta di furmatu currettu, perchè "corretta" in questu casu significa "ciò chì l'utilizatore vole", è questu ùn pò micca esse determinatu matematicamente.
Sembra chì s'ellu ùn avemu micca una definizione di verità, allora a specificazione hè inutile. Ma ùn hè micca. Solu perchè ùn sapemu micca ciò chì un prugramma deve fà, ùn significa micca chì ùn avemu micca bisognu di pensà à cumu si travaglia - à u cuntrariu, avemu da mette ancu più sforzu in questu. A specificazione hè particularmente impurtante quì. Hè impussibile di determinà u prugramma ottimali per a stampa strutturata, ma questu ùn significa micca chì ùn duvemu micca piglià à tuttu, è scrive u codice cum'è un flussu di cuscenza ùn hè micca una bona cosa. In fine, aghju scrittu una specificazione di sei regule cù definizione in forma di cumenti in un schedariu java. Eccu un esempiu di una di e regule: a left-comment token is LeftComment aligned with its covering token. Sta regula hè scritta in, dicemu, inglese matematicu: LeftComment aligned, left-comment и covering token - termini cù definizione. Hè cusì chì i matematichi descrizanu a matematica: scrivenu definizioni di termini è, basatu nantu à elli, regule. U benefiziu di una tale specificazione hè chì sei regule sò assai più faciuli di capiscenu è di debug di 850 linee di codice. Devu dì chì scrive queste regule ùn era micca faciule, ci hà pigliatu assai tempu per debug. In particulare per questu scopu, aghju scrittu un codice chì informava quale regula hè stata utilizata. Grazie à u fattu chì aghju pruvatu sti sei regule nantu à parechji esempii, ùn aghju micca bisognu di debug 850 linee di codice, è i bug si sò stati assai faciuli di truvà. Java hà grandi strumenti per questu. S'ellu avia ghjustu scrittu u codice, mi averia pigliatu assai più longu, è u furmatu hè statu di qualità più povira.
Perchè ùn puderia micca esse aduprata una specificazione formale? Da una banda, l'esekzione curretta ùn hè micca troppu impurtante quì. I stampati strutturali sò obligati à ùn piace à nimu, cusì ùn aghju micca bisognu di fà u funziunamentu bè in tutte e situazioni strane. Ancu più impurtante hè u fattu chì ùn aghju micca arnesi adattati. U verificatore di mudellu TLA + hè inutilità quì, cusì avissi da scrive manualmente l'esempii.
A specificazione sopra hà caratteristiche cumuni à tutte e specificazioni. Hè un livellu più altu ch'è u codice. Pò esse implementatu in ogni lingua. Ogni arnesi o metudi sò inutili per scrive. Nisun cursu di prugrammazione vi aiuterà à scrive sta specificazione. È ùn ci sò micca strumenti chì puderanu fà sta specificazione innecessaria, salvu chì, sicuru, scrivite una lingua specificamente per scrive prugrammi stampati strutturati in TLA+. Infine, sta specificazione ùn dice nunda di esattamente cumu scriveremu u codice, dice solu ciò chì face stu codice. Scrivemu a specificazione per aiutà à pensà à u prublema prima di cumincià à pensà à u codice.
Ma sta specificazione hà ancu caratteristiche chì a distinguenu da altre specificazioni. U 95% di l'altri specs sò significativamente più brevi è simplici:
Inoltre, sta specificazione hè un inseme di regule. En règle générale, il s'agit d'un signe de mauvaise spécification. Capisce e cunsequenze di un inseme di regule hè abbastanza difficiule, per quessa, aghju avutu à passà assai tempu per debugging. Tuttavia, in stu casu, ùn pudia truvà un modu megliu.
Hè vale a pena dì uni pochi di parolle nantu à i prugrammi chì funzionanu continuamente. Comu regula, travaglianu in parallelu, per esempiu, sistemi operativi o sistemi distribuiti. Pochi pirsuni ponu capiscenu mentalmente o nantu à carta, è ùn sò micca unu d'elli, ancu s'è una volta era capaci di fà. Dunque, avemu bisognu di strumenti chì verificanu u nostru travagliu - per esempiu, TLA + o PlusCal.
Perchè era necessariu di scrive una specificazione se sapia digià ciò chì esattamente u codice duverebbe fà? In fatti, pensu solu chì a sapia. Inoltre, cù una specificazione, un forasteru ùn hà più bisognu di entre in u codice per capisce ciò chì faci esattamente. Aghju una regula: ùn deve esse micca regule generale. Ci hè una eccezzioni à sta regula, sicuru, hè l'unica regula generale chì seguite: a specificazione di ciò chì u codice face deve dì à e persone tuttu ciò chì deve sapè quandu si usa u codice.
Allora chì esattamente i programatori anu bisognu di sapè à pensà? Per principianti, u listessu cum'è tutti l'altri: s'ellu ùn scrivite micca, allora vi pare solu chì pensate. Inoltre, avete bisognu di pensà prima di codice, chì significa chì avete bisognu di scrive prima di codice. A specificazione hè ciò chì scrivimu prima di cumincià à codificà. Una specificazione hè necessaria per qualsiasi codice chì pò esse usatu o mudificatu da qualcunu. È questu "qualchissia" pò esse l'autore di u codice stessu un mesi dopu chì hè statu scrittu. Una specificazione hè necessaria per i grandi prugrammi è sistemi, per classi, per metudi, è à volte ancu per sezzioni cumplessi di un solu metudu. Chì esattamente deve esse scrittu annantu à u codice? Avete bisognu di discrive ciò chì face, vale à dì ciò chì pò esse utile à ogni persona chì usa stu codice. Calchì volta pò ancu esse necessariu di specificà cumu u codice rializeghja u so scopu. Sè avemu passatu stu mètudu in u cursu di l'algoritmi, allora chjamemu un algoritmu. S'ellu hè qualcosa di più speciale è novu, allora chjamemu u disignu d'altu livellu. Ùn ci hè micca una differenza formale quì: i dui sò un mudellu astrattu di un prugramma.
Cumu esattamente duvete scrive una specificazione di codice? A cosa principal: deve esse un livellu più altu ch'è u codice stessu. Deve descriverà stati è cumpurtamenti. Deve esse strettu cum'è u compitu esige. Sè vo scrivite una specificazione per cumu si deve esse implementatu un compitu, pudete scrive in pseudocode o cù PlusCal. Avete bisognu à amparà à scrive specificazioni nantu à e specificazioni formali. Questu vi darà e cumpetenze necessarie chì vi aiuterà ancu cù quelli informali. Cumu amparà à scrive specificazioni formali? Quandu avemu amparatu à prugrammà, avemu scrittu prugrammi è poi debugged. Hè listessa quì: scrivite a spec, verificate cù u verificatore di mudelli, è corregge i bug. TLA + pò esse micca a megliu lingua per una specificazione formale, è una altra lingua hè prubabilmente megliu per i vostri bisogni specifichi. U vantaghju di TLA + hè chì insegna assai bè u pensamentu matematicu.
Cumu ligà specificazione è codice? Cù l'aiutu di cumenti chì liganu cuncetti matematichi è a so implementazione. Se travagliate cù gràfiche, allora à u livellu di u prugramma avete arrays of nodes è arrays of links. Dunque, avete bisognu di scrive esattamente cumu u graficu hè implementatu da queste strutture di prugrammazione.
Semu devi esse nutatu chì nimu di ciò chì sopra s'applica à u prucessu propiu di scrittura di codice. Quandu scrivite u codice, vale à dì, fate u terzu passu, avete ancu bisognu di pensà è di pensà à u prugramma. Se un subtask risulta esse cumplessu o micca ovvi, avete bisognu di scrive una specificazione per questu. Ma ùn sò micca parlatu di u codice stessu quì. Pudete aduprà qualsiasi lingua di prugrammazione, qualsiasi metodulugia, ùn si tratta micca di elli. Inoltre, nimu di u sopra elimina a necessità di pruvà è debug codice. Ancu s'è u mudellu astrattu hè scrittu currettamente, pò esse bugs in a so implementazione.
Scrizzione di specificazioni hè un passu supplementu in u prucessu di codificazione. Grazie à questu, parechji errori ponu esse catturati cù menu sforzu - sapemu questu da l'esperienza di i programatori di Amazon. Cù specificazioni, a qualità di i prugrammi diventa più altu. Allora perchè, allora, andemu cusì spessu senza elli ? Perchè a scrittura hè dura. È a scrittura hè difficiule, perchè per questu avete bisognu di pensà, è u pensamentu hè ancu difficiule. Hè sempre più faciule per finta ciò chì pensate. Quì pudete disegnà una analogia cù a corsa - più menu corre, più lenta corre. Avete bisognu di furmà i vostri musculi è praticà a scrittura. Avete bisognu di pratica.
A specificazione pò esse sbagliata. Puderete avè fattu un sbagliu in qualchì locu, o i requisiti puderanu avè cambiatu, o un migliuramentu puderia esse bisognu. Qualchese codice chì qualchissia usa deve esse cambiatu, cusì prima o dopu a specificazione ùn currisponde più à u prugramma. Ideale, in questu casu, avete bisognu di scrive una nova specificazione è riscrive completamente u codice. Sapemu bè chì nimu ùn face cusì. In pratica, patch u codice è possibbilmente aghjurnà a specificazione. Se questu hè obligatu à succede prima o dopu, allora perchè scrive specificazioni à tuttu? Prima, per a persona chì hà da edità u vostru codice, ogni parolla extra in a specificazione valerà u so pesu in oru, è sta persona pò esse tù stessu. Spessu mi rimproveru per ùn avè micca abbastanza specificazione quandu aghju editatu u mo codice. E scrivu più specificazioni cà codice. Dunque, quandu editate u codice, a specificazione deve esse sempre aghjurnata. Siconda, cù ogni rivisione, u codice s'aggrava, diventa sempre più difficiuli di leghje è mantene. Questu hè un aumentu di l'entropia. Ma s'ellu ùn principia micca cù una spec, allora ogni linea chì scrivite serà una edizione, è u codice serà imbustu è difficiule di leghje da u principiu.
Comu dettu , nisuna battaglia hè stata vinta per pianu, è nisuna battaglia hè stata vinta senza un pianu. È sapia una cosa o duie di battaglie. Ci hè una opinione chì scrive specificazioni hè una perdita di tempu. A volte questu hè veru, è u compitu hè cusì simplice chì ùn ci hè nunda di pensà. Ma duvete sempre ricurdà chì quandu vi hè dettu di ùn scrive micca specificazioni, vi sò dettu di ùn pensà. È duvete pensà à questu ogni volta. Pensendu à u compitu ùn guarantisci micca chì ùn fate micca sbagli. Comu sapemu, nimu hà inventatu a bacchetta magica, è a prugrammazione hè un compitu difficiule. Ma s'ellu ùn pensate micca à u prublema, vi sò garantitu di fà sbagli.
Pudete leghje più nantu à TLA + è PlusCal in un situ web speciale, pudete andà da a mo pagina di casa . Hè tuttu per mè, grazie per a vostra attenzione.
Per piacè nutate chì questu hè una traduzzione. Quandu scrivite cumenti, ricordate chì l'autore ùn li leghje micca. Se vulete veramente chjamà cù l'autore, allora ellu serà in a cunferenza Hydra 2019, chì si terrà 11-12 di lugliu 2019 in San Pietroburgo. I biglietti ponu esse acquistati .
Source: www.habr.com