Questo è un articolo tradotto . Ma prima, una breve introduzione. Come nascono gli zombie? Tutti si sono trovati nella situazione di voler sollevare un amico o un collega al proprio livello, ma non ci riescono. E il «non ci riescono» non riguarda tanto te, quanto lui: da un lato ci sono uno stipendio normale, compiti e così via, dall'altro la necessità di pensare. Pensare è sgradevole e doloroso. Si arrende rapidamente e continua a scrivere codice senza far lavorare il cervello. Ti immagini quanto sforzo ci voglia per superare il confine della impotenza appresa, e semplicemente non lo fai. Così si formano zombie che sembrano guaribili, ma in realtà nessuno se ne occupa.
Quando ho visto che (sì-sì, proprio quel compagno dei libri di testo) e non fa un rapporto, ma una sessione di domande e risposte, sono un po' preoccupato. Per fortuna, Leslie è un rinomato scienziato mondiale, autore di opere fondamentali nel campo del calcolo distribuito, e potresti anche conoscerlo per le lettere La nella parola LaTeX — «Lamport TeX». Un altro fattore preoccupante è la sua richiesta: chiunque venga deve (completamente gratuitamente) ascoltare in anticipo un paio dei suoi interventi, formulare almeno una domanda su di essi e solo allora presentarsi. Ho deciso di vedere cosa dice Lamport — ed è magnifico! È esattamente quel qualcosa, il link magico-pilota per curare la zombificazione. Avverto: il testo potrebbe dare fuoco ai fan delle metodologie super-flessibili e ai non amanti del testing del codice scritto.
Dopo la fase di hub-dropping, inizia la traduzione del seminario. Buona lettura!
Qualunque compito tu decida di affrontare, devi sempre seguire tre passi:
- decidere quale obiettivo vuoi raggiungere;
- stabilire come intendi perseguire il tuo obiettivo;
- raggiungere il tuo obiettivo.
Questo vale anche per la programmazione. Quando scriviamo codice, dobbiamo:
- decidere cosa deve fare esattamente il programma;
- definire esattamente come deve svolgere il suo compito;
- scrivere il codice corrispondente.
L'ultimo passaggio, ovviamente, è molto importante, ma non ne parlerò oggi. Invece, discuteremo dei primi due. Ogni programmatore li esegue prima di iniziare a lavorare. Non ci si siede a scrivere senza aver deciso cosa si sta scrivendo: un browser o un database. Deve esserci una chiara idea dell'obiettivo. E si riflette sempre su cosa farà esattamente il programma, invece di scrivere alla rinfusa nella speranza che il codice si trasformi in un browser.
In che modo avviene esattamente questa pianificazione del codice? Quanto sforzo dovremmo dedicarci? Tutto dipende da quanto è complesso il problema che stiamo cercando di risolvere. Immaginiamo di voler scrivere un sistema distribuito a prova di guasto. In tal caso, dobbiamo riflettere attentamente su tutto prima di metterci al lavoro sul codice. E se dobbiamo semplicemente incrementare una variabile intera di 1? A prima vista, sembra tutto banale e non c'è bisogno di riflettere, ma poi ci ricordiamo che potrebbe verificarsi un overflow. Pertanto, anche solo per capire se il problema è semplice o complesso, è necessario riflettere inizialmente.
Se pianifichi in anticipo le possibili soluzioni a un problema, puoi evitare errori. Ma per fare ciò, è fondamentale avere una mente chiara. Per raggiungere questo obiettivo, è utile annotare i propri pensieri. Mi piace molto la citazione di Dick Hinton: «Quando scrivi, la natura ti mostra quanto sia disordinato il tuo pensiero». Se non scrivi, ti sembra solo di pensare. È importante registrare i propri pensieri sotto forma di specifiche.
Le specifiche svolgono molteplici funzioni, soprattutto nei progetti di grande portata. Tuttavia, voglio concentrarmi su una sola: ci aiutano a pensare in modo chiaro. Pensare chiaramente è estremamente importante e piuttosto difficile, perciò abbiamo bisogno di ogni aiuto possibile. Quale linguaggio dovremmo utilizzare per scrivere le specifiche? Questo è sempre il primo interrogativo per i programmatori: quale lingua utilizzeremo. Non esiste una risposta unica: i problemi che affrontiamo sono troppo vari. Per alcuni, TLA+ è utile — è un linguaggio di specifiche che ho sviluppato. Per altri, può essere più comodo usare il cinese. Dipende dalla situazione.
C'è una domanda più importante: come possiamo ottenere un pensiero più chiaro? La risposta è che dobbiamo pensare come degli scienziati. Questo modo di pensare ha dimostrato di essere efficace negli ultimi 500 anni. Nella scienza, costruiamo modelli matematici della realtà. L'astronomia è stata, probabilmente, la prima scienza in senso stretto. Nel modello matematico utilizzato in astronomia, i corpi celesti sono rappresentati come punti con massa, posizione e impulso, anche se in realtà sono oggetti estremamente complessi, con montagne e oceani, maree e flussi. Questo modello, come tutti gli altri, è stato creato per risolvere problemi specifici. È molto utile per determinare in quale direzione puntare il telescopio se si desidera trovare un pianeta. Ma se si vuole prevedere il tempo su quel pianeta, questo modello non funzionerà.
La matematica ci permette di determinare le proprietà di un modello. E la scienza mostra come queste proprietà si relazionano alla realtà. Parliamo della nostra scienza, computer science. La realtà con cui lavoriamo comprende 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 effetti tutte queste conclusioni sono applicabili 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 di dover scrivere un browser. Affrontiamo tre compiti: progettare la rappresentazione del programma per l'utente, poi scrivere uno schema di alto livello del programma e, infine, scrivere il codice. Durante la scrittura del codice, ci rendiamo conto che dobbiamo creare uno strumento per la formattazione del testo. Anche qui dobbiamo affrontare tre compiti: definire quale testo questo strumento restituirà; scegliere un algoritmo per la formattazione; scrivere il codice. Questo compito ha una sua sottoattività: inserire correttamente il trattino nelle parole. Anche questa sottoattività la risolviamo in tre fasi: come possiamo vedere, si ripetono a molti livelli.
Esaminiamo più nel dettaglio il primo passo: quale problema risolve il programma. Qui modelliamo più spesso il programma come una funzione che riceve alcuni dati in ingresso e produce alcuni dati in uscita. In matematica, una funzione è 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 è composto dai primi elementi di ciascuna 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 le stesse delle funzioni nei linguaggi di programmazione. La matematica è significativamente più semplice. Poiché non ho tempo per esempi complessi, consideriamo un esempio semplice: una funzione in 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 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 numero intero che divide M e N. Come si relaziona questa modello con la realtà? Il modello opera con numeri interi, mentre in C o Java abbiamo 32 bit. -int. Questo modello ci permette di determinare se l'algoritmo è corretto. GCD, ma non impedirà gli errori di overflow. Per questo sarebbe servito un modello più complesso, per il quale non c'è tempo.
Parliamo delle limitazioni della funzione come modello. Il funzionamento di alcuni programmi (ad esempio, sistemi operativi) non si limita a restituire un valore specifico per argomenti specifici; possono operare in modo continuo. Inoltre, la funzione come modello non è adatta per il secondo passo: pianificare il modo di risolvere un problema. L'ordinamento rapido e l'ordinamento a bolle calcolano la stessa funzione, ma sono algoritmi completamente diversi. Pertanto, per descrivere il modo di raggiungere l'obiettivo del programma, utilizzo un altro modello, chiamiamolo modello comportamentale standard. In questo modello, 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 dei valori alle variabili.
Vediamo come apparirà il secondo passo per l'algoritmo di Euclide. Dobbiamo calcolare GCD(M, N). Inizializziamo M ZFS archivia i dati su disco. x, e N ZFS archivia i dati su disco. y, quindi sottraiamo ripetutamente la variabile più piccola da quella più grande finché non sono uguali. Ad esempio, se M = 12, e 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 piccola digressione sulla produttività. Spesso si misura in base al numero di righe di codice scritte in un giorno. Ma il vostro lavoro è molto più utile se siete riusciti a eliminare un certo numero di righe, perché avete ridotto lo spazio per i bug. E rimuovere codice è più facile proprio al primo passo. È del tutto possibile che non abbiate bisogno di tutte quelle complicazioni che cercate di implementare. Il modo più rapido per semplificare un programma e risparmiare tempo è non fare cose che non vale la pena fare. Il secondo passo è al secondo posto per potenziale risparmio di tempo. Se misurate la produttività in base al numero di righe scritte, quindi pensare a un modo per eseguire un compito vi renderà meno produttivi, poiché potrai risolvere lo stesso problema con meno codice. Non posso fornire statistiche precise qui, poiché non ho un modo per contare il numero di righe che non ho scritto grazie al tempo trascorso sulla specifica, cioè sui primi due passi. Inoltre, non è possibile fare un esperimento in questo caso, perché in un esperimento non abbiamo il diritto di eseguire il primo passo, essendo il compito definito in anticipo.
Nelle specifiche informali è facile trascurare molte difficoltà. Non c'è nulla di difficile nella scrittura di specifiche rigorose per le funzioni, non discuterò di questo. Invece, parleremo della scrittura di specifiche rigorose per i modelli comportamentali standard. Esiste un teorema che afferma che qualsiasi insieme di comportamenti può essere descritto tramite la proprietà di sicurezza (safety) e la proprietà di vivacità (liveness). La sicurezza significa che nulla di negativo accadrà, il programma non produrrà risposte errate. La resilienza implica che prima o poi accadrà qualcosa di positivo, ossia il programma fornirà infine la risposta corretta. In generale, la sicurezza è un indicatore di maggiore importanza, poiché gli errori si presentano più frequentemente in questo ambito. Pertanto, per risparmiare tempo, non parlerò della resilienza, benché sia comunque rilevante.
Raggiungiamo la sicurezza definendo, in primo luogo, un gran numero di possibili stati iniziali. In secondo luogo, stabilendo relazioni con tutti i possibili stati successivi per ciascuno stato. Comportiamoci come scienziati e definiamo questi stati in modo matematico. L'insieme degli stati iniziali è descritto dalla formula, ad esempio, nel caso dell'algoritmo euclideo: (x = M) ∧ (y = N). Per determinati valori 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 segnate con un apostrofo, mentre quelle dello stato attuale non lo sono. Nel caso dell'algoritmo euclideo, ci occuperemo della disgiunzione di due formule, in una delle quali x è il valore massimo, mentre nel secondo — y:
Nel primo caso, il nuovo valore di y è uguale al precedente valore di y, mentre il nuovo valore di x si ottiene 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 determina uno stato iniziale unico, (x = 12) ∧ (y = 18). Poi sostituiamo questi valori nella formula sopra e otteniamo:
Qui l'unica 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. Pertanto, abbiamo una specifica completa del secondo passo — come possiamo vedere, è matematica piuttosto ordinaria, 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 spiegare il suo funzionamento non è difficile, ma non c'è tempo adesso. La logica temporale potrebbe essere necessaria solo per la proprietà di vivacità, mentre per la sicurezza non è necessaria. La logica temporale, in quanto tale, non è apprezzata; non è propriamente matematica ordinaria, ma nel caso della vivacità rappresenta un male necessario.
Nell'algoritmo di Euclide, per ogni valore x e y ci sono valori unici x' e y', che rendono vero il rapporto 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 tratto ci siano diversi valori della variabile con tratto, in cui il rapporto con il successivo stato è vero. Non è complicato farlo, ma non fornirò esempi adesso.
Per creare uno strumento funzionante, è necessaria la matematica formale. Come si può rendere formale una specifica? Per questo avremo bisogno di un linguaggio formale, ad esempio, . La specifica dell'algoritmo di Euclide apparirà in questo modo in questo linguaggio:
Il simbolo dell'uguale con il triangolo indica che il valore a sinistra del simbolo è definito come uguale al valore a destra del simbolo. In sostanza, una specifica è una definizione, in questo caso due definizioni. Alla specifica in TLA+ è necessario aggiungere dichiarazioni e una certa sintassi, come mostrato nella slide sopra. In ASCII, apparirà così:
Come possiamo vedere, non c'è nulla di complicato. La specifica in TLA+ può essere verificata, ovvero esplorare tutti i possibili comportamenti in un piccolo modello. In questo caso, quel modello sarà rappresentato da determinati valori. M e N. Questo è un modo molto efficace e semplice per effettuare la verifica, che viene eseguito completamente in modo automatico. Inoltre, è possibile scrivere prove formali di verità e verificarle meccanicamente, ma ciò richiede molto tempo, quindi quasi nessuno lo fa.
Il principale svantaggio di TLA+ è che si tratta di matematica, e i programmatori e i informatici temono la matematica. A prima vista, potrebbe sembrare uno scherzo, ma purtroppo lo dico sul serio. Un mio collega mi ha appena raccontato di come ha cercato di spiegare TLA+ a diversi sviluppatori. Appena sono apparse delle formule sullo schermo, i loro occhi sono diventati di vetro. Quindi, se TLA+ è spaventoso, si può usare , è una sorta di linguaggio di programmazione per giocattoli. Un'espressione in PlusCal può essere qualsiasi espressione TLA+, cioè, in sostanza, qualsiasi espressione matematica. Inoltre, PlusCal ha una sintassi per algoritmi nondeterministici. Poiché in PlusCal è possibile scrivere qualsiasi espressione TLA+, è significativamente più espressivo di qualsiasi linguaggio di programmazione reale. Inoltre, PlusCal viene compilato in una specifica TLA+ facilmente leggibile. Questo non significa, ovviamente, che una specifica complessa in PlusCal si trasformerà in una semplice su TLA+ — c'è una chiara corrispondenza tra di loro, senza aggiungere complessità. Infine, questa specifica può essere verificata utilizzando gli strumenti TLA+. In generale, PlusCal può contribuire a superare la fobia matematica, e può essere facilmente compreso anche da programmatori e scienziati informatici. In passato, ho pubblicato algoritmi su di esso per circa 10 anni.
È possibile che qualcuno obietti che TLA+ e PlusCal siano matematica, e che la matematica funzioni solo su esempi inventati. Tuttavia, in pratica, è 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 uso ha contribuito in modo significativo allo sviluppo, poiché siamo stati in grado di catturare bug pericolosi prima del lancio in produzione e perché ci ha fornito la comprensione e la fiducia necessarie per ottimizzazioni delle prestazioni aggressive che non compromettano la correttezza del programma». Spesso si sente dire che l'uso dei metodi formali porta a codice inefficiente — in pratica, è esattamente il contrario. Inoltre, si crede che sia impossibile convincere i manager della necessità dei metodi formali, anche se i programmatori ne sono convinti della loro utilità. E Newcomb scrive: «I manager ora incoraggiano in tutti i modi a scrivere specifiche in TLA+ e dedicano tempo specificamente a questo». Quindi, quando i manager vedono che TLA+ funziona, sono lieti di adottarlo. Chris Newcomb ha scritto questo circa sei mesi fa (nell'ottobre 2014), e attualmente, per quanto ne so, TLA+ è utilizzato in 14 progetti, non 10. Un altro esempio riguarda la progettazione di Xbox 360. Un tirocinante è andato da Charles Take e ha scritto una specifica per il sistema di memoria. Grazie a questa specifica è stato individuato un bug che altrimenti non sarebbe stato notato 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.
Puoi leggere di più su TLA+ su Internet, ma ora parliamo delle specifiche informali. Raramente dobbiamo scrivere programmi che calcolano il massimo comune divisore e simili. Molto più spesso scriviamo programmi come lo strumento di stampa strutturata (pretty-printer) che ho creato per TLA+. Dopo il trattamento più semplice, il codice in TLA+ apparirebbe nel seguente modo:
Ma nell'esempio fornito, l'utente probabilmente voleva 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, somma e moltiplicazione nella fonte era casuale, quindi una semplice elaborazione è perfettamente 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 dovrebbe fare esattamente il programma, ciò non significa che non dobbiamo pensare al suo funzionamento — al contrario, dovremmo impegnarci ancora di più. La specifica qui è particolarmente importante. Non è possibile definire il programma ottimale per la stampa strutturale, 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. nelle commenti in un file Java. Ecco un esempio di una delle regole: un token left-comment è LeftComment allineato con il suo token di copertura. Questa regola è scritta in un inglese matematico, per così dire: LeftComment allineato, left-comment e token di copertura — termini con definizioni. È così che i matematici descrivono la matematica: scrivono le definizioni dei termini e, sulla base di queste, le regole. Il vantaggio di tale specifica è che comprendere e debugare sei regole è significativamente più facile che 850 righe di codice. Va detto che scrivere queste regole non è stato semplice, ci è voluto parecchio tempo per debuggare. Proprio per questo motivo, ho scritto un codice che comunicava quale regola fosse utilizzata. Grazie al fatto che ho testato queste sei regole su diversi esempi, non ho dovuto debugare 850 righe di codice e i bug si sono rivelati abbastanza facili da trovare. In Java ci sono strumenti eccellenti per questo. Se avessi semplicemente scritto il codice, mi sarebbe servito molto più tempo e il formato sarebbe stato di qualità inferiore.
Perché non poteva essere utilizzata una specifica formale? Da un lato, la correttezza dell'implementazione non è così importante. Una stampa strutturata sicuramente deluderà qualcuno, quindi non dovevo garantire il corretto funzionamento in tutte le situazioni anomale. Ancora più importante è il fatto che non avevo strumenti adeguati. Uno strumento per la verifica dei modelli TLA+ è qui inutile, quindi avrei dovuto scrivere manualmente gli esempi.
La specifica fornita presenta caratteristiche comuni a tutte le specifiche. È di un livello superiore rispetto al codice. Può essere implementata in qualsiasi linguaggio. Non servono strumenti o metodi particolari per scriverla. Nessun corso di programmazione ti aiuterà a scrivere questa specifica. Non esistono strumenti in grado di rendere questa specifica superflua, a meno che tu non stia scrivendo un linguaggio specificamente progettato per scrivere programmi di stampa strutturale in TLA+. Infine, questa specifica non dice nulla su come scriveremo realmente il codice; specifica solo cosa fa quel codice. Scriviamo la specifica per aiutarci a riflettere sul problema prima di iniziare a pensare al codice.
Tuttavia, questa specifica ha anche peculiarità che la distinguono da altre specifiche. Il 95% delle altre specifiche è notevolmente più breve e semplice:
Inoltre, questa specifica è un insieme di regole. Di solito, questa è una caratteristica di una cattiva specifica. Comprendere le conseguenze di un insieme di regole è piuttosto difficile, ed è per questo che ho dovuto dedicare molto tempo alla loro ottimizzazione. Tuttavia, in questo caso, non sono riuscito a trovare un modo migliore.
Vale la pena dire alcune parole sui programmi che funzionano in modo continuo. Di solito, operano in parallelo, come i sistemi operativi o i sistemi distribuiti. Pochi possono districarsi in essi mentalmente o su carta, e io non rientro in questo gruppo, anche se una volta ero in grado di farlo. Pertanto, sono necessari strumenti che verifichino il nostro lavoro, come TLA+ o PlusCal.
Perché era necessario scrivere una specifica se sapevo già cosa doveva fare il codice? In realtà, mi sembrava solo di saperlo. Inoltre, con una specifica, qualcuno che non è coinvolto non ha bisogno di entrare nel codice per capire cosa fa. Ho una regola: non devono esserci regole generali. Ovviamente, esiste un'eccezione a questa regola, che è 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.
Allora, cosa devono sapere i programmatori sul pensiero? In primo luogo, ciò che tutti devono sapere: se non scrivi, ti sembra solo di pensare. Inoltre, è necessario riflettere prima di codificare, e questo significa scrivere prima di codificare. Una specifica è ciò che scriviamo prima di iniziare a codificare. La specifica è necessaria per qualsiasi codice che può essere utilizzato o modificato da chiunque. E questo 'chiunque' può essere lo stesso autore del codice un mese dopo averlo scritto. La specifica è necessaria per grandi programmi e sistemi, per classi, per metodi e, a volte, anche per sezioni complesse di un singolo metodo. Cosa bisogna scrivere riguardo al codice? È necessario descrivere cosa fa, cioè ciò che può essere utile a chiunque utilizzi questo codice. A volte potrebbe anche essere necessario indicare come il codice raggiunga il suo obiettivo. Se il metodo è quello che abbiamo trattato nel corso di algoritmi, lo chiamiamo algoritmo. Se invece si tratta di qualcosa di più specifico e nuovo, lo chiamiamo progettazione ad alto livello. Formalmente non c'è differenza: entrambe le cose sono modelli astratti del programma.
Come si scrive correttamente una specifica di codice? La cosa principale è che deve essere a un livello superiore rispetto al codice stesso. Deve descrivere stati e comportamenti. Deve essere tanto rigorosa quanto lo richiede il compito. Se stai scrivendo una specifica su come realizzare un compito, puoi farlo in pseudocodice o utilizzando PlusCal. È fondamentale imparare a scrivere specifiche su specifiche formali. Questo ti fornirà le abilità necessarie che ti aiuteranno anche con quelle informali. E come si può imparare a scrivere specifiche formali? Quando imparavamo a programmare, scrivevamo programmi e poi li debuggavamo. Lo stesso vale qui: bisogna scrivere una specifica, verificarla con uno strumento di verifica dei modelli e correggere gli errori. TLA+ potrebbe non essere il miglior linguaggio per la specifica formale, e probabilmente un altro linguaggio sarebbe più adatto alle tue esigenze specifiche. Il vantaggio di TLA+ è che insegna excellentemante a pensare in modo matematico.
Come collegare la specifica e il codice? Attraverso commenti che collegano concetti matematici e la loro implementazione. Se stai lavorando con i grafi, a livello di programma avrai array di nodi e array di relazioni. Quindi, devi scrivere come il grafo viene effettivamente implementato da queste strutture di programmazione.
È importante notare che nulla di quanto detto si riferisce al processo di scrittura del codice stesso. Quando scrivi codice, ossia esegui il terzo passo, devi anche pensare e pianificare il programma. Se un sottocompito risulta difficile o poco chiaro, è necessario scrivere una specifica per esso. Ma qui non parlo del codice stesso. Puoi utilizzare qualsiasi linguaggio di programmazione, qualsiasi metodologia, non è di questo che si tratta. Inoltre, nulla di quanto appena detto solleva dalla necessità di testare e fare debug del codice. Anche se il modello astratto è scritto correttamente, nella sua implementazione potrebbero esserci bug.
Scrivere specifiche è un passaggio aggiuntivo nel processo di sviluppo del codice. Grazie a questo, molti errori possono essere individuati con minori sforzi — lo sappiamo per esperienza dai programmatori di Amazon. Con le specifiche, la qualità del software migliora. Perché allora così spesso ci troviamo a farne a meno? Perché scrivere è difficile. E scrivere è difficile perché richiede riflessione, e riflettere è anch'esso difficile. È sempre più semplice dare l'impressione di pensare. Qui si può tracciare un'analogia con la corsa: meno corri, più lentamente correrai. È necessario allenare i propri muscoli e fare pratica nella scrittura. Serve allenamento.
La specifica potrebbe essere errata. Potresti aver commesso un errore da qualche parte, potrebbero essere cambiate le esigenze, oppure potrebbe essere necessario apportare un miglioramento. Qualsiasi codice utilizzato da qualcuno deve essere modificato, quindi prima o poi la specifica smetterà di corrispondere al programma. Idealmente, in questo caso, bisognerebbe scrivere una nuova specifica e riscrivere completamente il codice. Sappiamo benissimo che così non fa nessuno. In pratica, patchiamo il codice e, forse, aggiorniamo la specifica. Se ciò deve necessariamente accadere prima o poi, perché scrivere specifiche? Innanzitutto, per la persona che modificherà il tuo codice, ogni parola di troppo nella specifica sarà preziosa, e quell’individuo potresti essere tu stesso. Spesso mi colpevolizzo per l’insufficienza della specifica quando modifico il mio codice. E scrivo più specifiche che codice. Pertanto, quando modifichi il codice, la specifica deve sempre essere aggiornata. Inoltre, con ogni modifica, il codice diventa peggiore, più difficile da leggere e mantenere. Questa è una crescente entropia. Ma se non parti da una specifica, ogni riga scritta sarà una correzione, e il codice fin dall'inizio sarà ingombrante e difficile da leggere.
Come disse , nessuna battaglia è stata vinta secondo piano e nessuna battaglia è stata vinta senza piano. E lui sapeva qualcosa sulle battaglie. C'è un'opinione che redigere specifiche sia una perdita di tempo. A volte è davvero così, e il compito è così semplice che non c'è niente da elaborare. Ma bisogna sempre ricordare che quando vi consigliano di non scrivere le specifiche, vi stanno consigliando di non pensare. E questo si deve riflettere ogni volta. Progettare il compito non garantisce che non commetterete errori. Come sappiamo, nessuno ha inventato una bacchetta magica e la programmazione è una attività complessa. Ma se non progettate il compito, garantite di commettere errori.. 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'è niente da riflettere. Ma bisogna sempre ricordare che, quando vi dicono di non scrivere specifiche, significa che vi consigliano di non pensare. E su questo bisognerebbe riflettere ogni volta. Riflettere su un compito non garantisce che non commetterete errori. Come sappiamo, nessuno ha inventato la bacchetta magica, e la programmazione è un'attività complessa. Ma se non riflettete sul compito, garantite di fare errori.
Per saperne di più su TLA+ e PlusCal, potete visitare il sito speciale, accessibile dalla mia pagina principale. Questo è tutto per ora, grazie per l'attenzione.
Ricordo che questa è una traduzione. Quando scriverete commenti, ricordate che l'autore non li leggerà. Se desiderate realmente comunicare con l'autore, sarà alla conferenza Hydra 2019, che si terrà l'11-12 luglio 2019 a San Pietroburgo. I biglietti possono essere acquistati. .
Fonte: habr.com
