Questo è un articolo di traduzione . Ma prima c'è una breve introduzione. Come si formano gli zombie? Ognuno di noi si è trovato nella situazione di voler elevare un amico o un collega al proprio livello, senza successo. E il «senza successo» non riguarda tanto te, quanto lui: da una parte della bilancia ci sono uno stipendio normale, compiti e così via, dall'altra c'è la necessità di pensare. Pensare è scomodo e doloroso. Si arrende rapidamente e continua a scrivere codice, senza usare il cervello. Hai idea di quante energie siano necessarie per superare la barriera dell'impotenza appresa, e semplicemente non lo fai. Così si formano gli zombie, che sembrano guaribili, ma a quanto pare nessuno si occuperà di loro.
Quando ho visto che (sì-sì, proprio lui, quello dei libri di testo) e non faceva una relazione, ma una sessione di domande e risposte, ero un po' diffidente. Per ogni evenienza, Leslie è un famoso scienziato, autore di opere fondamentali nel calcolo distribuito, e potresti conoscerlo anche per le lettere La nella parola LaTeX — «Lamport TeX». Il secondo fattore inquietante è la sua richiesta: chiunque viaggi deve (completamente gratuitamente) ascoltare in anticipo un paio delle sue presentazioni, formulare almeno una domanda su di esse e solo allora presentarsi. Ho deciso di vedere cosa dice Lamport — ed è magnifico! È esattamente quella cosa, il link magico per curare la zombificazione. Avviso: il testo potrebbe infastidire notevolmente gli amanti delle metodologie super flessibili e quelli che non amano testare ciò che scrivono.
Dopo l'hubrocat, inizia effettivamente la traduzione del seminario. Buona lettura!
Qualunque compito tu stia affrontando, devi sempre seguire tre passaggi:
- decidere quale obiettivo vuoi raggiungere;
- decidere come intendi raggiungere il tuo obiettivo;
- arrivare al tuo obiettivo.
Questo vale anche per la programmazione. Quando scriviamo codice, dobbiamo:
- decidere cosa deve fare esattamente il programma;
- determinare come deve svolgere il suo compito;
- scrivere il codice corrispondente.
L'ultimo passo, ovviamente, è molto importante, ma oggi non ne parlerò. Invece, discuteremo dei primi due. Ogni programmatore li esegue prima di iniziare a lavorare. Non ti siedi a scrivere se non hai deciso cosa stai scrivendo: un browser o un database. Un'idea chiara dell'obiettivo deve essere necessariamente presente. E devi riflettere su cosa farà esattamente il programma, non scrivere alla rinfusa sperando che il codice si trasformi in un browser.
Come avviene esattamente questa preliminare riflessione sul codice? Quanto tempo dobbiamo dedicarvi? Tutto dipende da quanto è complesso il problema che stiamo risolvendo. Supponiamo che vogliamo scrivere un sistema distribuito resistente ai guasti. In questo caso, dobbiamo riflettere a lungo prima di sederci a scrivere il codice. E se abbiamo solo bisogno di incrementare una variabile intera di 1? A prima vista, tutto ciò sembra banale, e non c'è bisogno di riflessioni, ma poi ricordiamo che potrebbe verificarsi unOverflow. Pertanto, anche solo per capire se si tratta di un problema semplice o complesso, è necessario riflettere in anticipo.
Se si riflettono preventivamente le possibili soluzioni a un problema, si possono evitare errori. Ma per fare ciò, è necessario avere un pensiero chiaro. Per ottenere ciò, bisogna annotare i propri pensieri. Mi piace molto la citazione di Dick Gindin: «Quando scrivi, la natura ti mostra quanto sia disordinato il tuo pensiero». Se non scrivi, ti sembra solo di pensare. E annotare i propri pensieri deve avvenire sotto forma di specifiche.
Le specifiche svolgono molte funzioni, specialmente in progetti di grandi dimensioni. Ma parlerò solo di una di esse: ci aiutano a pensare chiaramente. Pensare chiaramente è molto importante e piuttosto difficile, quindi qui abbiamo bisogno di qualsiasi supporto. In quale lingua dovremmo scrivere le specifiche? Questa è sempre la prima domanda per i programmatori: in quale lingua scriveremo. Non c'è una risposta giusta: i problemi che risolviamo sono troppo variegati. Per alcuni è utile TLA+ — è un linguaggio di specifiche che ho sviluppato. Per altri è più comodo utilizzare il cinese. Tutto dipende dalla situazione.
Ciò che è più importante è un'altra domanda: come ottenere un pensiero più chiaro? Risposta: dobbiamo pensare come scienziati. Questo è un modo di pensare che ha dimostrato la propria efficacia negli ultimi 500 anni. Nella scienza costruiamo modelli matematici della realtà. L'astronomia è stata probabilmente la prima scienza nel senso rigoroso del termine. Nel modello matematico utilizzato in astronomia, i corpi celesti si presentano come punti dotati di massa, posizione e impulso, anche se in realtà sono oggetti estremamente complessi con montagne e oceani, maree e flussi. Questo modello, come qualsiasi altro, è stato creato per risolvere compiti specifici. È perfetto per determinare dove indirizzare il telescopio se vogliamo trovare un pianeta. Ma se vuoi prevedere il tempo su quel pianeta, questo modello non funziona.
La matematica ci consente di determinare le proprietà del modello. E la scienza mostra come queste proprietà si rapportano alla realtà. Parliamo della nostra scienza, informatica. La realtà con cui lavoriamo sono i sistemi computazionali di vario tipo: processori, console di gioco, computer che eseguono programmi e così via. Parlerò dell'esecuzione di un programma su un computer, ma, in linea di massima, tutte queste conclusioni si applicano a qualsiasi sistema computazionale. Nella nostra scienza utilizziamo molti modelli diversi: la macchina di Turing, insiemi di eventi parzialmente ordinati e molti altri.
Cos'è un programma? È qualsiasi codice che può essere considerato autonomamente. Supponiamo che dobbiamo scrivere un browser. Affrontiamo tre compiti: progettiamo la rappresentazione del programma per l'utente, poi scriviamo uno schema ad alto livello del programma e, infine, scriviamo il codice. Durante la scrittura del codice, ci rendiamo conto che dobbiamo creare uno strumento per formattare il testo. Qui dobbiamo nuovamente affrontare tre compiti: determinare quale testo restituirà questo strumento; scegliere un algoritmo per la formattazione; scrivere il codice. Questo compito ha la sua sottoattività: inserire correttamente il tratto in parole. Anche questa sottoattività la risolviamo in tre passaggi: come possiamo vedere, si ripetono a molti livelli.
Esaminiamo più nel dettaglio il primo passo: quale problema risolve il programma. Qui modelliamo normalmente il programma come una funzione, che riceve determinati dati in ingresso e restituisce alcuni dati in uscita. In matematica, una funzione viene solitamente descritta come un insieme ordinato di coppie. Ad esempio, la funzione di elevamento al quadrato per i numeri naturali è descritta come l'insieme {, , , , …}. L'insieme di definizione di tale funzione è l'insieme dei primi elementi di ogni coppia, cioè i numeri naturali. Per definire una funzione, dobbiamo specificare il suo insieme di definizione e la formula.
Ma le funzioni in matematica non sono la stessa cosa delle funzioni nei linguaggi di programmazione. La matematica è notevolmente più semplice. Poiché non ho tempo per esempi complessi, consideriamo un esempio semplice: una funzione nel linguaggio C o un metodo statico in Java che restituisce il massimo comune divisore di due numeri interi. Nella specifica di questo metodo scriveremo: calcola GCD(M,N) per gli argomenti M e N, dove GCD(M,N) — una funzione il cui insieme di definizione è l'insieme delle coppie di numeri interi, e il valore restituito è il più grande intero che divide M e N. Come si relaziona questo modello con la realtà? Il modello opera con numeri interi, mentre in C o Java abbiamo un inta 32 bit. Questo modello ci consente di determinare se l'algoritmo GCDè corretto, ma non previene gli errori di overflow. Per farlo servirebbe un modello più complesso, per il quale non c'è tempo.
Parliamo delle limitazioni della funzione come modello. Il funzionamento di alcuni programmi (ad esempio, i sistemi operativi) non si riduce a restituire un valore specifico per argomenti specifici; possono essere eseguiti continuamente. Inoltre, la funzione come modello non si adatta bene al secondo passo: pianificazione del modo di risolvere il problema. L'ordinamento rapido e l'ordinamento a bolle calcolano la stessa funzione, ma sono algoritmi completamente diversi. Pertanto, per descrivere il modo in cui raggiungere l'obiettivo del programma, utilizzo un altro modello, chiamiamolo modello comportamentale standard. In esso, il programma è rappresentato come un insieme di tutti i comportamenti ammissibili, ognuno dei quali, a sua volta, è una sequenza di stati, e uno stato è l'assegnazione di valori alle variabili.
Vediamo come apparirà il secondo passaggio per l'algoritmo di Euclide. Dobbiamo calcolare GCD(M, N). Inizializziamo M come x, ma N come y, poi sottraiamo ripetutamente il valore minore da quello maggiore finché non sono uguali. Ad esempio, se M = 12, ma N = 18, possiamo descrivere il seguente comportamento:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
E se M = 0 e N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Qui vale la pena fare una breve digressione sulla produttività. Spesso viene misurata nel numero di righe di codice scritte in un giorno. Ma il tuo lavoro è molto più utile se riesci a eliminare un certo numero di righe, perché avrai meno spazio per i bug. E eliminare codice è più semplice proprio nel primo passaggio. È del tutto possibile che tu non abbia bisogno di tutti quegli extra che stai cercando di attuare. Il modo più veloce per semplificare un programma e risparmiare tempo è non fare cose che non dovresti fare. Il secondo passaggio è al secondo posto per potenziale risparmio di tempo. Se misuri la produttività in base al numero di righe scritte, allora pensare a un modo per completare un compito ti renderà meno produttivo, poiché potrai risolvere lo stesso compito con meno codice. Non posso fornire statistiche esatte qui, poiché non ho modo di contare quante righe non ho scritto grazie al tempo speso nella specificazione, cioè nei primi e secondi passaggi. E anche qui non possiamo condurre esperimenti, perché nell'esperimento non abbiamo il diritto di eseguire il primo passaggio, l'incarico è definito in anticipo.
Nelle specifiche informali è facile non tenere conto di molte difficoltà. Non c'è nulla di difficile nello scrivere specifiche rigorose per le funzioni, non ne discuterò. Invece, parleremo di come scrivere specifiche rigorose per i modelli comportamentali standard. Esiste un teorema che afferma che ogni insieme di comportamenti può essere descritto utilizzando la proprietà di sicurezza (safety) e la proprietà di vivacità (liveness). La sicurezza significa che non accadrà nulla di male, il programma non fornirà risposte errate. La resilienza significa che, prima o poi, succederà qualcosa di buono, vale a dire che il programma darà, prima o poi, la risposta corretta. In generale, la sicurezza è un indicatore più importante, gli errori si verificano più spesso proprio qui. Pertanto, per risparmiare tempo, non parlerò della resilienza, anche se essa è ovviamente importante.
Otteniamo la sicurezza definendo, prima di tutto, numerosi possibili stati iniziali. E, in secondo luogo, le relazioni con tutti i possibili stati successivi per ciascuno stato. Comportiamoci come scienziati e definiamo gli stati matematicamente. L'insieme degli stati iniziali è descritto da una formula, per esempio, nel caso dell'algoritmo di Euclide: (x = M) ∧ (y = N). Per valori specifici M e N esiste solo uno stato iniziale. La relazione con lo stato successivo è descritta da una formula in cui le variabili dello stato successivo sono scritte con un apice, mentre quelle dello stato attuale sono senza apice. Nel caso dell'algoritmo di Euclide, ci confronteremo con la disgiunzione di due formule, in una delle quali x è il valore massimo, e nell'altra — y:
Nel primo caso, il nuovo valore di y è uguale al vecchio valore di y, mentre il nuovo valore di x lo otteniamo sottraendo la variabile minore da quella maggiore. Nel secondo caso, facciamo l'opposto.
Torniamo all'algoritmo di Euclide. Supponiamo di nuovo che M = 12, N = 18. Questo definisce un unico stato iniziale, (x = 12) ∧ (y = 18). Poi sostituiamo questi valori nella formula sopra e otteniamo:
Qui c'è una sola soluzione possibile: x' = 18 - 12 ∧ y' = 12, e otteniamo il comportamento: [x = 12, y = 18]. Allo stesso modo, possiamo descrivere tutti gli stati nel nostro comportamento: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Nell'ultimo stato [x = 6, y = 6] entrambe le parti dell'espressione saranno false, quindi non c'è uno stato successivo. Quindi, abbiamo una specifica completa del secondo passo: come vediamo, è matematica del tutto normale, come quella degli ingegneri e degli scienziati, e non strana, come in computer science.
Queste due formule possono essere unite in un'unica formula di logica temporale. È elegante e spiegarla non è difficile, ma attualmente non c'è tempo per farlo. La logica temporale potrebbe essere necessaria solo per la proprietà di vivacità, mentre per la sicurezza non è necessaria. La logica temporale in sé non è gradita, non è esattamente matematica comune, ma nel caso della vivacità è un male necessario.
Nell'algoritmo di Euclide per ogni valore x e y ci sono valori unici x' e y', che rendono vera la relazione con il successivo stato. In altre parole, l'algoritmo di Euclide è deterministico. Per modellare un algoritmo non deterministico, è necessario che lo stato attuale abbia diversi possibili stati futuri, e che per ogni valore della variabile senza segno ci siano più valori della variabile con segno per i quali la relazione con il successivo stato è vera. Non è difficile da fare, ma al momento non fornirò esempi.
Per creare uno strumento funzionante, è necessaria la matematica formale. Come rendere formale una specifica? Per questo avremo bisogno di un linguaggio formale, ad esempio, . La specifica dell'algoritmo di Euclide apparirà in questo linguaggio come segue:
Il simbolo dell'uguale con un triangolo indica che il valore a sinistra dell'uguale è definito come uguale al valore a destra dell'uguale. In sostanza, la specifica è una definizione, nel nostro caso due definizioni. Nella specifica in TLA+ bisogna aggiungere dichiarazioni e una certa sintassi, come mostrato nella slide sopra. In ASCII apparirà così:
Come vediamo, nulla di complicato. La specifica in TLA+ può essere verificata, cioè si possono esaminare tutti i comportamenti possibili in un piccolo modello. In questo caso, questo modello saranno valori specifici M e N. È un modo molto efficace e semplice di verifica, che si esegue completamente in modo automatico. Inoltre, è possibile scrivere prove formali di verità e verificarle meccanicamente, ma ci vorrebbe molto tempo, perciò quasi nessuno lo fa.
Il principale svantaggio di TLA+ è che si tratta di matematica, e i programmatori e gli informatici temono la matematica. A prima vista sembra uno scherzo, ma purtroppo lo dico sul serio. Un mio collega mi stava raccontando di come ha cercato di spiegare TLA+ a diversi sviluppatori. Non appena le formule sono apparse sullo schermo, i loro occhi si sono subito riempiti di confusione. Quindi, se TLA+ spaventa, si può usare , che è una sorta di linguaggio di programmazione giocattolo. Un'espressione in PlusCal può essere qualunque espressione TLA+, cioè, in grande misura, qualunque espressione matematica. Inoltre, in PlusCal c'è una sintassi per algoritmi non deterministici. Poiché in PlusCal è possibile scrivere qualunque espressione TLA+, è significativamente più espressivo di qualsiasi linguaggio di programmazione reale. Inoltre, PlusCal viene compilato in una specifica TLA+ di facile lettura. Ciò non significa, ovviamente, che una specifica complessa di PlusCal si trasformerà in una semplice su TLA+: c'è una corrispondenza ovvia tra di loro, senza apparire ulteriore complessità. Infine, questa specifica può essere verificata con gli strumenti TLA+. In generale, PlusCal può aiutare a superare la fobia della matematica, è facile da comprendere anche per programmatori e informatici. In passato ho pubblicato per un certo periodo (circa 10 anni) algoritmi in esso.
È possibile che qualcuno obietti che TLA+ e PlusCal siano matematica e che la matematica funzioni solo su esempi inventati. Nella pratica, tuttavia, è necessario un linguaggio reale con tipi, procedure, oggetti e così via. Non è così. Ecco cosa scrive Chris Newcomb, che ha lavorato in Amazon: «Abbiamo utilizzato TLA+ in dieci grandi progetti, e in ogni caso il suo utilizzo ha fornito un contributo significativo allo sviluppo, perché siamo riusciti a catturare bug pericolosi prima che arrivassero in produzione, e perché ci ha fornito la comprensione e la fiducia necessarie per ottimizzazioni aggressive delle prestazioni, senza compromettere la validità del programma». Spesso si sente dire che utilizzando metodi formali otteniamo codice inefficiente; in pratica, tuttavia, è esattamente l'opposto. Inoltre, si pensa che sia impossibile convincere i manager della necessità dei metodi formali, anche se i programmatori sono convinti della loro utilità. E Newcomb scrive: «I manager ora spingono in tutti i modi per scrivere specifiche in TLA+, e dedicano tempo a questo». Quindi quando i manager vedono che TLA+ funziona, lo accettano con piacere. Chris Newcomb ha scritto questo circa sei mesi fa (a ottobre 2014), e adesso, per quanto ne so, TLA+ è utilizzato in 14 progetti, e non 10. Un altro esempio riguarda la progettazione di XBox 360. A Charles Tecker si è presentato uno stagista che ha scritto una specifica per il sistema di memoria. Grazie a questa specifica è stato trovato un bug che altrimenti sarebbe stato trascurato, e che avrebbe causato il crash di ogni XBox 360 dopo quattro ore di utilizzo. Gli ingegneri di IBM hanno confermato che i loro test non avrebbero rilevato questo bug.
Potete leggere maggiori dettagli su TLA+ su internet, ma ora parliamo delle specifiche informali. Raramente ci capita di scrivere programmi che calcolano il massimo comune divisore e simili. Molto più spesso scriviamo programmi come uno strumento di stampa strutturata (pretty-printer) che ho creato per TLA+. Dopo la più semplice elaborazione, il codice in TLA+ apparirebbe come segue:
Ma nell'esempio fornito, l'utente voleva probabilmente che i segni di congiunzione e uguaglianza fossero allineati. Quindi la formattazione corretta apparirebbe piuttosto così:
Consideriamo un altro esempio:
Qui, al contrario, l'allineamento dei segni di uguaglianza, addizione e moltiplicazione nel sorgente era casuale, quindi la più semplice elaborazione è più che sufficiente. In generale, non esiste una definizione matematica precisa di una formattazione corretta, perché «corretto» in questo caso significa «quello che desidera l'utente», e questo non può essere definito matematicamente.
Sembrerebbe che se non abbiamo una definizione di verità, la specifica sia inutile. Ma non è così. Se non sappiamo cosa debba fare il programma, non significa che non dobbiamo riflettere sul suo funzionamento: al contrario, dobbiamo investire ancora più sforzi. In questo caso la specifica è particolarmente importante. Determinare il programma ottimale per la stampa strutturata è impossibile, ma ciò non significa che non dobbiamo occuparcene affatto, e scrivere codice come un flusso di coscienza non è la soluzione. Alla fine, ho scritto una specifica di sei regole con definizioni in forma di commenti nel file Java. Ecco un esempio di una delle regole: un token di commento a sinistra è LeftComment allineato con il suo token di copertura. Questa regola è scritta in un inglese, diciamo così, matematico: LeftComment allineato, commento a sinistra e token di copertura — termini con definizioni. Questo è come i matematici descrivono la matematica: scrivono definizioni dei termini e sulla base di esse — regole. Il vantaggio di tale specifica è che capire e debuggare sei regole è notevolmente più semplice che 850 righe di codice. Va detto che scrivere queste regole non è stato semplice, ci è voluto parecchio tempo per debuggare. Appositamente per questo scopo ho scritto un codice che segnalava quale regola specifica veniva utilizzata. Grazie al fatto che ho testato queste sei regole su diversi esempi, non ho dovuto debuggare 850 righe di codice e i bug sono stati piuttosto facili da trovare. In Java ci sono ottimi strumenti per questo. Se avessi semplicemente scritto il codice, ci sarebbero voluti molto più tempo e la formattazione ne sarebbe risultata di qualità inferiore.
Perché non è stato possibile utilizzare una specifica formale? Da un lato, la correttezza dell'esecuzione non è particolarmente importante qui. Una stampa strutturale sicuramente non piacerà a qualcuno, quindi non ho dovuto garantire il corretto funzionamento in tutte le situazioni anomale. È ancora più importante il fatto che non avevo strumenti adeguati. Gli strumenti per la verifica dei modelli TLA+ qui sono inutili, quindi avrei dovuto scrivere manualmente gli esempi.
La specifica fornita ha caratteristiche comuni a tutte le specifiche. È a un livello più alto rispetto al codice. Può essere implementata in qualsiasi linguaggio. Per scriverla, non servono strumenti o metodi. Nessun corso di programmazione ti aiuterà a scrivere questa specifica. E non esistono strumenti che possano rendere questa specifica superflua, a meno che tu non stia scrivendo un linguaggio appositamente per scrivere programmi di stampa strutturale in TLA+. Infine, questa specifica non dice nulla su come scriveremo effettivamente il codice, indica solo cosa fa questo codice. Scriviamo una specifica per aiutarci a riflettere sul problema prima di iniziare a pensare al codice.
Ma questa specifica ha anche caratteristiche che la distinguono dalle altre specifiche. Il 95% delle altre specifiche è significativamente più breve e più semplice:
Inoltre, questa specifica è un insieme di regole. Di norma, è un segno di una cattiva specifica. Comprendere le conseguenze di un insieme di regole è piuttosto difficile, ed è per questo che ho dovuto spendere molto tempo a correggerle. Tuttavia, in questo caso non ho trovato un modo migliore.
Vale la pena dire qualche parola sui programmi che funzionano continuamente. Di norma, essi operano in parallelo, ad esempio i sistemi operativi o i sistemi distribuiti. Capirli a mente o su carta può essere possibile solo per pochissimi, e non sono parte di questo gruppo, anche se un tempo mi era possibile. Pertanto, sono necessari strumenti che controllino il nostro lavoro, come TLA+ o PlusCal.
Perché scrivere una specifica, se sapevo già cosa doveva fare il codice? In realtà, avevo solo l'impressione di conoscerlo. Inoltre, con una specifica, una persona esterna non deve più tuffarsi nel codice per capire cosa faccia esattamente. Ho una regola: non devono esserci regole generali. Questa regola, ovviamente, ha un'eccezione, ed è l'unica regola generale che seguo: la specifica di ciò che fa il codice deve comunicare alle persone tutto ciò che devono sapere per utilizzare quel codice.
Quindi, cosa devono sapere i programmatori sul pensiero? Innanzitutto, la stessa cosa che chiunque altro: se non scrivi, ti sembra solo di pensare. Inoltre, bisogna riflettere prima di codificare, e questo significa che bisogna scrivere prima di codificare. La specifica è ciò che scriviamo prima di iniziare a codificare. La specifica è necessaria per qualsiasi codice che possa essere utilizzato o modificato da chiunque. E questo "chiunque" potrebbe essere lo stesso autore del codice un mese dopo la sua scrittura. La specifica è necessaria per programmi e sistemi complessi, per classi, per metodi e talvolta anche per sezioni complicate di un singolo metodo. Cosa bisogna scrivere sul codice? Bisogna descrivere cosa fa, cioè ciò che può essere utile a qualsiasi persona che utilizza questo codice. A volte può anche essere necessario indicare come il codice raggiunge il suo obiettivo. Se questo metodo è stato trattato nel corso di algoritmi, lo chiamiamo algoritmo. Se invece si tratta di qualcosa di più speciale e nuovo, lo chiamiamo progettazione di alto livello. Non c'è una differenza formale qui: entrambi sono modelli astratti di un programma.
Come si dovrebbe scrivere una specifica del codice? La cosa principale: deve essere a un livello superiore rispetto al codice stesso. Deve descrivere stati e comportamenti. Deve essere rigorosa quanto richiede il compito. Se stai scrivendo una specifica del metodo di realizzazione del compito, può essere scritta in pseudocodice o usando PlusCal. Bisogna imparare a scrivere specifiche su specifiche formali. Questo ti darà le competenze necessarie che ti aiuteranno anche con le non formali. E come imparare a scrivere specifiche formali? Quando studiavamo programmazione, scrivevamo programmi e poi li debuggiavamo. Lo stesso vale qui: devi scrivere una specifica, verificarla con uno strumento di verifica di modelli e correggere gli errori. TLA+, forse, non è il miglior linguaggio per la specifica formale, e probabilmente un altro linguaggio è più adatto alle tue esigenze specifiche. Il vantaggio di TLA+ è che insegna ottimamente a pensare in modo matematico.
Come collegare la specifica al codice? Attraverso commenti che collegano i concetti matematici alla loro implementazione. Se si sta lavorando con grafi, a livello di programma avrete array di nodi e array di connessioni. Pertanto, dovete scrivere come esattamente il grafo viene implementato da queste strutture di programmazione.
È importante notare che nulla di quanto sopra si riferisce al processo stesso di scrittura del codice. Quando scrivete codice, cioè eseguite il terzo passo, dovete anche pensare e riflettere sul programma. Se un sotto-compito risulta complicato o poco chiaro, dovete scrivere una specifica per esso. Ma non parlo qui del codice. Potete utilizzare qualsiasi linguaggio di programmazione, qualsiasi metodologia, non è di questo che si tratta. Inoltre, nulla di quanto sopra elimina la necessità di testare e fare debugging del codice. Anche se il modello astratto è scritto correttamente, nella sua implementazione potrebbero esserci bug.
Scrivere specifiche è un'importante fase aggiuntiva nel processo di scrittura del codice. Grazie a questo, molti errori possono essere catturati con minori sforzi — lo sappiamo per esperienza degli sviluppatori di Amazon. Con le specifiche, la qualità dei programmi migliora. Allora perché spesso ci passiamo senza? Perché scrivere è difficile. E scrivere è difficile perché richiede di pensare, e pensare è difficile. È sempre più semplice far finta di pensare. Qui si può fare un'analogia con la corsa: più si corre poco, più lentamente si corre. È necessario allenare i propri muscoli e esercitarsi nella scrittura. Serve pratica.
La specifica potrebbe essere errata. Potreste aver commesso un errore da qualche parte, oppure i requisiti potrebbero essere cambiati, oppure potrebbe essere stato necessario apportare dei miglioramenti. Qualsiasi codice che qualcuno utilizza deve essere modificato, quindi prima o poi la specifica smetterà di corrispondere al programma. Idealmente, in questo caso, sarebbe necessario scrivere una nuova specifica e riscrivere completamente il codice. Sappiamo benissimo che nessuno lo fa. Nella pratica, patchiamo il codice e, forse, aggiorniamo la specifica. Se questo accade necessariamente prima o poi, perché scrivere specifiche? Prima di tutto, per la persona che modificherà il vostro codice, ogni parola in più nella specifica sarà preziosa, e quella persona potreste essere voi stessi. Spesso mi rimprovero per una specifica insufficiente quando modifico il mio codice. E scrivo più specifiche che codice. Quindi, quando modificate il codice, è sempre necessario aggiornare la specifica. In secondo luogo, ad ogni modifica, il codice diventa peggiore, diventa sempre più difficile da leggere e mantenere. Questo è un aumento dell'entropia. Ma se non iniziate con la specifica, ogni riga scritta sarà una modifica, e il codice sin dall'inizio sarà ingombrante e difficile da leggere.
Come diceva , nessuna battaglia è stata vinta secondo il piano, e nessuna battaglia è stata vinta senza piano. E lui sapeva qualcosa sulle battaglie. C'è l'opinione che scrivere specifiche sia una perdita di tempo. A volte è davvero così, e il compito è così semplice che non c'è nulla da pianificare. Ma bisogna sempre ricordare che, quando vi viene consigliato di non scrivere specifiche, significa che vi viene consigliato di non pensare. E su questo bisogna sempre riflettere. Pianificare un compito non garantisce che non si commettano errori. Come sappiamo, nessuno ha inventato la bacchetta magica, e la programmazione è un'attività complessa. Ma se non pianificate il compito, farete certamente errori.
Potete leggere ulteriormente su TLA+ e PlusCal su un sito apposito, a cui potete accedere dalla mia homepage . Questo è tutto per ora, grazie per l'attenzione.
Ricordo che si tratta di una traduzione. Quando scriverete commenti, ricordate che l'autore non li leggerà. Se desiderate davvero parlare con l'autore, sarà alla conferenza Hydra 2019, che si svolgerà dall'11 al 12 luglio 2019 a San Pietroburgo. I biglietti sono disponibili per l'acquisto. .
Fonte: habr.com
