Questo è un articolo di traduzione . Ma prima c’è una breve introduzione. Come si formano gli zombie? Tutti si sono trovati nella situazione in cui vorrebbero portare un amico o un collega al loro livello, ma non funziona. Inoltre “non funziona” non tanto per te, ma per lui: da un lato della bilancia c'è uno stipendio normale, compiti e così via, e dall'altro c'è la necessità di pensare. Pensare è spiacevole e doloroso. Si arrende rapidamente e continua a scrivere codice senza usare affatto il cervello. Ti rendi conto di quanto sforzo ci vuole per superare la barriera dell'impotenza appresa e semplicemente non lo fai. È così che si formano gli zombi, che sembrano possibile curare, ma sembra che nessuno lo farà.
Quando l'ho visto (sì, lo stesso amico dei libri di testo) e non si tratta di una relazione, ma di una sessione di domande e risposte, ero un po' diffidente. Per ogni evenienza, Leslie è uno scienziato di fama mondiale, autore di lavori fondamentali sull'informatica distribuita, e potresti anche conoscerlo con le lettere La in LaTeX - "Lamport TeX". Il secondo fattore allarmante è la sua esigenza: chiunque venga deve (in modo completamente gratuito) ascoltare in anticipo un paio dei suoi rapporti, formulare almeno una domanda al riguardo e solo dopo venire. Ho deciso di vedere cosa trasmetteva Lamport lì - ed è fantastico! Questa è esattamente quella cosa, una pillola magica per curare gli zombi. Ti avverto: il testo potrebbe scottare seriamente chi ama le metodologie super agili e non ama mettere alla prova ciò che ha scritto.
Dopo l'habrokat inizia effettivamente la traduzione del seminario. Buona lettura!
Qualunque sia il compito che svolgi, devi sempre seguire tre passaggi:
- decidere quale obiettivo vuoi raggiungere;
- decidi esattamente come raggiungerai il tuo obiettivo;
- raggiungi il tuo obiettivo.
Questo vale anche per la programmazione. Quando scriviamo il codice, abbiamo bisogno di:
- decidere cosa dovrebbe fare esattamente il programma;
- determinare esattamente come dovrebbe svolgere il suo compito;
- scrivere il codice appropriato.
L’ultimo passaggio, ovviamente, è molto importante, ma non ne parlerò oggi. Parleremo invece dei primi due. Ogni programmatore li esegue prima di iniziare a lavorare. Non ti siedi per scrivere a meno che tu non abbia deciso cosa scrivere: un browser o un database. Deve essere presente una certa idea dell'obiettivo. E pensi sicuramente a cosa farà esattamente il programma e non lo scrivi a casaccio nella speranza che il codice stesso si trasformi in qualche modo in un browser.
Come avviene esattamente questa pre-pensazione del codice? Quanto impegno dovremmo mettere in questo? Tutto dipende da quanto è complesso il problema che stiamo risolvendo. Diciamo che vogliamo scrivere un sistema distribuito tollerante agli errori. In questo caso, dovremmo riflettere attentamente sulle cose prima di dedicarci al codice. Cosa succede se dobbiamo solo incrementare una variabile intera di 1? A prima vista, qui tutto è banale e non è necessario pensarci, ma poi ricordiamo che può verificarsi un trabocco. Pertanto, anche per capire se un problema è semplice o complesso, bisogna prima pensare.
Se pensi in anticipo alle possibili soluzioni a un problema, puoi evitare errori. Ma questo richiede che il tuo pensiero sia chiaro. Per raggiungere questo obiettivo, devi scrivere i tuoi pensieri. Adoro la citazione di Dick Guindon: "Quando scrivi, la natura ti mostra quanto sia sciatto il tuo pensiero". Se non scrivi, pensi solo di pensare. E devi scrivere i tuoi pensieri sotto forma di specifiche.
Le specifiche svolgono molte funzioni, soprattutto nei grandi progetti. Ma ne parlerò solo di uno: ci aiutano a pensare con lucidità. Pensare chiaramente è molto importante e piuttosto difficile, quindi abbiamo bisogno di aiuto qui. In quale lingua dovremmo scrivere le specifiche? In generale, questa è sempre la prima domanda per i programmatori: in che lingua scriveremo? Non esiste una risposta corretta: i problemi che risolviamo sono troppo diversi. Per alcune persone, TLA+ è un linguaggio di specifica che ho sviluppato. Per altri è più conveniente usare il cinese. Tutto dipende dalla situazione.
La domanda più importante è: come possiamo ottenere un pensiero più chiaro? Risposta: dobbiamo pensare come scienziati. Questo è un modo di pensare che ha funzionato bene negli ultimi 500 anni. Nella scienza costruiamo modelli matematici della realtà. L'astronomia è stata forse la prima scienza nel senso stretto del termine. Nel modello matematico utilizzato in astronomia, i corpi celesti appaiono come punti dotati di massa, posizione e quantità di moto, anche se in realtà sono oggetti estremamente complessi con montagne e oceani, flussi e riflussi. Questo modello, come tutti gli altri, è stato creato per risolvere alcuni problemi. È ottimo per determinare dove puntare un telescopio se vuoi trovare un pianeta. Ma se vuoi prevedere il tempo su questo pianeta, questo modello non funzionerà.
La matematica ci consente di determinare le proprietà di un modello. E la scienza mostra come queste proprietà si relazionano alla realtà. Parliamo della nostra scienza, l'informatica. La realtà con cui lavoriamo è costituita da sistemi informatici di molti tipi diversi: processori, console di gioco, computer che eseguono programmi e così via. Parlerò dell'esecuzione di un programma su un computer, ma, in generale, tutte queste conclusioni si applicano a qualsiasi sistema informatico. Nella nostra scienza utilizziamo molti modelli diversi: la macchina di Turing, insiemi di eventi parzialmente ordinati e molti altri.
Qual è il programma? Questo è qualsiasi codice che può essere considerato da solo. Diciamo che dobbiamo scrivere un browser. Eseguiamo tre compiti: progettiamo la presentazione del programma da parte dell'utente, quindi scriviamo il diagramma di alto livello del programma e infine scriviamo il codice. Mentre scriviamo il codice, ci rendiamo conto che dobbiamo scrivere un formattatore di testo. Anche in questo caso dobbiamo risolvere tre problemi: determinare quale testo restituirà questo strumento; selezionare un algoritmo per la formattazione; scrivere il codice. Questa attività ha una propria attività secondaria: inserire correttamente i trattini nelle parole. Risolviamo anche questa sottoattività in tre passaggi: come vediamo, si ripetono a molti livelli.
Diamo uno sguardo più da vicino al primo passo: quale problema risolve il programma. Qui molto spesso modelliamo un programma come una funzione che accetta input e fornisce output. In matematica, una funzione è solitamente descritta come un insieme ordinato di coppie. Ad esempio, la funzione di quadratura per i numeri naturali è descritta come l'insieme {<0,0>, <1,1>, <2,4>, <3,9>, …}. Il dominio di definizione di tale funzione è l'insieme dei primi elementi di ciascuna coppia, cioè i numeri naturali. Per definire una funzione, dobbiamo specificarne il dominio e la formula.
Ma le funzioni in matematica non sono le stesse funzioni nei linguaggi di programmazione. Il calcolo è molto più semplice. Dato che non ho tempo per esempi complessi, consideriamone uno semplice: una funzione in C o un metodo statico in Java che restituisce il massimo comun divisore di due numeri interi. Nella specifica di questo metodo scriveremo: calcola GCD(M,N) per argomenti M и NDove GCD(M,N) - una funzione il cui dominio è un insieme di coppie di numeri interi e il valore restituito è il più grande intero diviso per M и N. Come si confronta la realtà con questo modello? Il modello funziona con numeri interi e in C o Java abbiamo 32 bit int. Questo modello ci consente di decidere se l'algoritmo è corretto GCD, ma non impedirà gli errori di overflow. Ciò richiederebbe un modello più complesso, per il quale non c’è tempo.
Parliamo dei limiti della funzione come modello. Alcuni programmi (come i sistemi operativi) non si limitano a restituire un valore specifico per determinati argomenti; possono essere eseguiti continuamente. Inoltre, la funzione di modello è poco adatta per il secondo passo: pianificare come risolvere il problema. Quicksort e bubble sort calcolano la stessa funzione, ma sono algoritmi completamente diversi. Pertanto, per descrivere il modo per raggiungere l'obiettivo del programma, utilizzo un altro modello, chiamiamolo modello comportamentale standard. Il programma è rappresentato in esso come un insieme di tutti i comportamenti validi, ciascuno dei quali, a sua volta, è una sequenza di stati e uno stato è l'assegnazione di valori alle variabili.
Vediamo come sarebbe il secondo passaggio dell'algoritmo euclideo. Dobbiamo calcolare GCD(M, N). Inizializziamo M come xE N come y, quindi sottrai ripetutamente la più piccola di queste variabili dalla più grande finché non sono uguali. Ad esempio, se M = 12E N = 18, possiamo descrivere il seguente comportamento:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
A meno che non M = 0 и N = 0? Lo zero è divisibile per tutti i numeri, quindi in questo caso non esiste il massimo divisore. In questa situazione, dobbiamo tornare al primo passo e chiederci: abbiamo davvero bisogno di calcolare il MCD per i numeri non positivi? Se ciò non è necessario, è sufficiente modificare le specifiche.
Qui è opportuna una breve digressione sulla produttività. Viene spesso misurato in numero di righe di codice scritte al giorno. Ma il tuo lavoro è molto più utile se elimini un certo numero di righe, perché hai meno spazio per i bug. E il modo più semplice per eliminare il codice è il primo passaggio. È possibile che tu semplicemente non abbia bisogno di tutti gli fronzoli che stai cercando di implementare. Il modo più veloce per semplificare un programma e risparmiare tempo è non fare cose che non dovrebbero essere fatte. Il secondo passaggio ha il secondo più alto potenziale di risparmio di tempo. Se misuri la produttività in termini di righe scritte, pensare a come completare un'attività ti renderà più forte meno produttivo, perché puoi risolvere lo stesso problema con meno codice. Non posso fornire qui statistiche esatte, perché non ho modo di contare il numero di righe che non ho scritto a causa del tempo che ho dedicato alla specifica, cioè al primo e al secondo passaggio. E nemmeno qui possiamo fare un esperimento, perché in un esperimento non abbiamo il diritto di completare il primo passaggio; il compito è determinato in anticipo.
È facile trascurare molte difficoltà nelle specifiche informali. Non c’è niente di difficile nello scrivere specifiche rigorose per le funzioni; non ne parlerò. Parleremo invece di scrivere specifiche forti per comportamenti standard. Esiste un teorema che afferma che qualsiasi insieme di comportamenti può essere descritto utilizzando la proprietà security (sicurezza) e proprietà di sopravvivenza (vitalità). Sicurezza significa che non accadrà nulla di male, il programma non darà la risposta sbagliata. Sopravvivenza significa che prima o poi accadrà qualcosa di buono, vale a dire che prima o poi il programma darà la risposta corretta. Di norma, la sicurezza è un indicatore più importante, qui si verificano più spesso errori. Pertanto, per risparmiare tempo, non parlerò di sopravvivenza, sebbene anch'essa, ovviamente, sia importante.
Raggiungiamo la sicurezza specificando prima un insieme di possibili stati iniziali. E in secondo luogo, le relazioni con tutti i possibili stati successivi per ciascuno stato. Comportiamoci come scienziati e definiamo matematicamente gli stati. L'insieme degli stati iniziali è descritto dalla formula, ad esempio, nel caso dell'algoritmo euclideo: (x = M) ∧ (y = N). Per certi valori M и N esiste un solo stato iniziale. La relazione con lo stato successivo è descritta da una formula in cui le variabili dello stato successivo sono scritte con un numero primo e le variabili dello stato corrente sono scritte senza numero primo. Nel caso dell'algoritmo euclideo avremo a che fare con la disgiunzione di due formule, in una delle quali x è il valore più grande e nel secondo - y:
Nel primo caso, il nuovo valore di y è uguale al valore precedente di y, e otteniamo il nuovo valore di x sottraendo la variabile più piccola da quella più grande. Nel secondo caso facciamo il contrario.
Torniamo all'algoritmo euclideo. Supponiamo ancora una volta questo M = 12, N = 18. Questo definisce un unico stato iniziale, (x = 12) ∧ (y = 18). Inseriamo quindi questi valori nella formula sopra e otteniamo:
Ecco l'unica soluzione possibile: x' = 18 - 12 ∧ y' = 12e otteniamo il comportamento: [x = 12, y = 18]. Allo stesso modo, possiamo descrivere tutti gli stati del 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 avrà uno stato successivo. Quindi, abbiamo una specificazione completa del secondo passaggio: come vediamo, questa è matematica abbastanza ordinaria, come quella di ingegneri e scienziati, e non strana, come nell'informatica.
Queste due formule possono essere combinate in un'unica formula di logica temporale. È elegante e facile da spiegare, ma non c’è tempo per questo adesso. Potremmo aver bisogno della logica temporale solo per la proprietà della vivacità; per la sicurezza non è necessaria. Non mi piace la logica temporale in quanto tale, non è proprio matematica ordinaria, ma nel caso della vivacità è un male necessario.
Nell'algoritmo euclideo per ogni valore x и y ci sono valori unici x' и y', che rendono vera la relazione con lo stato successivo. In altre parole, l’algoritmo euclideo è deterministico. Per modellare un algoritmo non deterministico, lo stato corrente deve avere più possibili stati futuri e ciascun valore della variabile senza primer deve avere più valori della variabile con primer in modo tale che la relazione con lo stato successivo sia vera. Questo non è difficile da fare, ma non darò esempi ora.
Per creare uno strumento di lavoro, è necessaria la matematica formale. Come rendere formale una specifica? Per fare questo avremo bisogno di un linguaggio formale, ad es. . La specifica dell'algoritmo euclideo in questo linguaggio sarà simile alla seguente:
Il simbolo del segno uguale con un triangolo significa che il valore a sinistra del segno è determinato come uguale al valore a destra del segno. In sostanza, una specificazione è una definizione, nel nostro caso due definizioni. Alla specifica in TLA+ è necessario aggiungere dichiarazioni e un po' di sintassi, come nella slide sopra. In ASCII sarebbe simile a questo:
Come puoi vedere, niente di complicato. La specifica su TLA+ può essere verificata, ovvero è possibile aggirare tutti i possibili comportamenti in un piccolo modello. Nel nostro caso, questo modello avrà determinati valori M и N. Questo è un metodo di verifica molto efficace e semplice, completamente automatico. Inoltre, è possibile scrivere prove formali della verità e controllarle meccanicamente, ma ciò richiede molto tempo, quindi quasi nessuno lo fa.
Lo svantaggio principale di TLA+ è che si tratta di matematica, e programmatori e informatici hanno paura della matematica. A prima vista sembra uno scherzo, ma purtroppo lo dico con tutta serietà. Un mio collega mi stava proprio raccontando di come ha provato a spiegare TLA+ a diversi sviluppatori. Non appena le formule sono apparse sullo schermo, i loro occhi sono diventati immediatamente vitrei. Quindi, se TLA+ fa paura, puoi usare , è una sorta di linguaggio di programmazione giocattolo. Un'espressione in PlusCal può essere qualsiasi espressione TLA+, ovvero sostanzialmente qualsiasi espressione matematica. Inoltre, PlusCal ha una sintassi per algoritmi non deterministici. Poiché PlusCal può scrivere qualsiasi espressione TLA+, è significativamente più espressivo di qualsiasi linguaggio di programmazione reale. Successivamente, PlusCal viene compilato in una specifica TLA+ di facile lettura. Ciò non significa, ovviamente, che la complessa specifica PlusCal si trasformerà in una semplice su TLA+ - solo che la corrispondenza tra loro è ovvia, non apparirà alcuna complessità aggiuntiva. Infine, questa specifica può essere verificata utilizzando gli strumenti TLA+. In generale PlusCal può aiutare a superare la fobia della matematica; è di facile comprensione anche per programmatori e informatici. Ho pubblicato algoritmi su di esso per qualche tempo (circa 10 anni) in passato.
Forse qualcuno obietterà che TLA+ e PlusCal sono matematica, e la matematica funziona solo con esempi inventati. In pratica, è necessario un linguaggio reale con tipi, procedure, oggetti e così via. Questo è sbagliato. Ecco cosa scrive Chris Newcomb, che ha lavorato presso Amazon: "Abbiamo utilizzato TLA+ su dieci progetti di grandi dimensioni e in ogni caso il suo utilizzo ha fatto una differenza significativa per lo sviluppo perché siamo stati in grado di individuare bug pericolosi prima che arrivassero alla produzione e perché ci ha dato la visione e la sicurezza di cui avevamo bisogno per rendere aggressivi ottimizzazioni delle prestazioni senza influenzare la verità del programma". Spesso puoi sentire che quando utilizziamo metodi formali otteniamo codice inefficiente: in pratica, tutto è esattamente l'opposto. Inoltre, c’è la percezione che i manager non possano essere convinti della necessità di metodi formali, anche se i programmatori sono convinti della loro utilità. E Newcomb scrive: "I manager stanno ora spingendo in ogni modo possibile per scrivere le specifiche in TLA+ e stanno dedicando tempo specifico a questo". Pertanto, quando i manager vedono che TLA+ funziona, lo abbracciano. Chris Newcomb ha scritto questo circa sei mesi fa (ottobre 2014), ma ora, per quanto ne so, TLA+ è utilizzato in 14 progetti, non in 10. Un altro esempio riguarda il design dell'XBox 360. Uno stagista è andato da Charles Thacker e ha scritto le specifiche per il sistema di memoria. Grazie a questa specifica è stato scoperto un bug che altrimenti non sarebbe stato rilevato e che avrebbe causato il crash di ogni XBox 360 dopo quattro ore di utilizzo. Gli ingegneri dell'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 calcolino il minimo comune divisore e simili. Molto più spesso scriviamo programmi come lo strumento Pretty-Printer che ho scritto per TLA+. Dopo l'elaborazione più semplice, il codice TLA+ sarebbe simile a questo:
Ma nell'esempio sopra, molto probabilmente l'utente desiderava che la congiunzione e i segni di uguale fossero allineati. Quindi la formattazione corretta sarebbe più simile a questa:
Considera un altro esempio:
Qui, al contrario, l'allineamento dei segni uguali, dell'addizione e della moltiplicazione nella fonte era casuale, quindi l'elaborazione più semplice è abbastanza. In generale, non esiste una definizione matematica esatta della formattazione corretta, perché "corretto" in questo caso significa "ciò che l'utente vuole" e questo non può essere determinato matematicamente.
Sembrerebbe che se non abbiamo una definizione di verità, la specificazione sia inutile. Ma non è vero. Solo perché non sappiamo cosa dovrebbe fare un programma non significa che non dobbiamo pensare a come dovrebbe funzionare: al contrario, dovremmo impegnarci ancora di più. La specifica è particolarmente importante qui. È impossibile determinare il programma ottimale per la stampa strutturata, ma ciò non significa che non dovremmo intraprenderlo affatto, e scrivere il codice come flusso di coscienza non è il caso. Alla fine ho scritto una specifica di sei regole con le definizioni sotto forma di commenti in un file Java. Ecco un esempio di una delle regole: a left-comment token is LeftComment aligned with its covering token. Questa regola è scritta, diciamo, in inglese matematico: LeftComment aligned, left-comment и covering token — Termini con definizioni. È così che i matematici descrivono la matematica: scrivono definizioni di termini e, sulla base di esse, creano regole. Il vantaggio di questa specifica è che sei regole sono molto più facili da comprendere ed eseguire il debug rispetto a 850 righe di codice. Devo dire che scrivere queste regole non è stato facile; ci è voluto parecchio tempo per eseguirne il debug. Ho scritto un codice appositamente per questo scopo che mi diceva quale regola veniva utilizzata. Poiché ho testato queste sei regole con alcuni esempi, non ho dovuto eseguire il debug di 850 righe di codice e i bug sono stati abbastanza facili da trovare. Java ha ottimi strumenti per questo. Se avessi scritto solo il codice, avrei impiegato molto più tempo e la formattazione sarebbe stata di qualità inferiore.
Perché non è possibile utilizzare una specifica formale? Da un lato, qui la corretta esecuzione non è troppo importante. Una stampa strutturata è destinata a essere insoddisfacente per alcuni, quindi non ho dovuto farla funzionare correttamente in tutte le situazioni insolite. Ancora più importante è il fatto che non avevo strumenti adeguati. Il controllo del modello TLA+ è inutile in questo caso, quindi dovrei scrivere gli esempi a mano.
La specifica data ha caratteristiche comuni a tutte le specifiche. È un livello superiore rispetto al codice. Può essere implementato in qualsiasi lingua. Non ci sono strumenti o metodi per scriverlo. Nessun corso di programmazione ti aiuterà a scrivere questa specifica. E non ci sono strumenti che potrebbero rendere superflua questa specifica, a meno che ovviamente non si stia scrivendo un linguaggio specifico per scrivere programmi di stampa strutturati in TLA+. Infine, queste specifiche non dicono nulla su come scriveremo esattamente il codice, ma indicano solo cosa fa il codice. Scriviamo una specifica per aiutarci a riflettere sul problema prima di iniziare a pensare al codice.
Ma questa specifica presenta anche caratteristiche che la distinguono dalle altre specifiche. Il 95% delle altre specifiche sono molto più brevi e semplici:
Inoltre, questa specifica è un insieme di regole. Questo di solito è un segno di specifiche scadenti. Comprendere le conseguenze di un insieme di regole è piuttosto difficile, motivo per cui ho dovuto dedicare molto tempo al loro debug. Tuttavia, in questo caso non sono riuscito a trovare un modo migliore.
Vale la pena spendere qualche parola sui programmi che funzionano continuamente. Tipicamente operano in parallelo, come sistemi operativi o sistemi distribuiti. Pochissime persone riescono a capirli nella loro mente o sulla carta, e io non sono uno di loro, anche se una volta ero in grado di farlo. Pertanto, abbiamo bisogno di strumenti che controllino il nostro lavoro, ad esempio TLA+ o PlusCal.
Perché avevo bisogno di scrivere una specifica se sapevo già cosa avrebbe dovuto fare il codice? In effetti, pensavo solo di saperlo. Inoltre, con una specifica in atto, un estraneo non ha più bisogno di esaminare il codice per capire cosa fa esattamente. Ho una regola: non dovrebbero esserci regole generali. Naturalmente c'è un'eccezione a questa regola, questa è l'unica regola generale che seguo: la specifica di ciò che fa il codice dovrebbe dire alle persone tutto ciò che devono sapere quando utilizzano quel codice.
Quindi cosa devono sapere esattamente i programmatori sul pensiero? Tanto per cominciare, è come per tutti: se non scrivi, ti sembra solo di pensare. Inoltre, devi pensare prima di scrivere codice, il che significa che devi scrivere prima di scrivere codice. Una specifica è ciò che scriviamo prima di iniziare a scrivere codice. È necessaria una specifica per qualsiasi codice che possa essere utilizzato o modificato da chiunque. E questo “qualcuno” potrebbe rivelarsi l'autore del codice un mese dopo che è stato scritto. Una specifica è necessaria per programmi e sistemi di grandi dimensioni, per classi, per metodi e talvolta anche per sezioni complesse di un singolo metodo. Cosa dovresti scrivere esattamente sul codice? Devi descrivere cosa fa, cioè qualcosa che può essere utile a chiunque utilizzi questo codice. A volte può anche essere necessario specificare in che modo esattamente il codice raggiunge il suo obiettivo. Se abbiamo seguito questo metodo nel corso sugli algoritmi, allora lo chiameremo algoritmo. Se si tratta di qualcosa di più specializzato e nuovo, allora lo chiamiamo design di alto livello. Non c'è alcuna differenza formale qui: entrambi sono modelli astratti del programma.
Come dovresti scrivere esattamente una specifica del codice? La cosa principale: dovrebbe essere un livello superiore al codice stesso. Deve descrivere stati e comportamenti. Dovrebbe essere rigoroso quanto richiesto dal compito. Se stai scrivendo una specifica su come implementare un'attività, è possibile scriverla in pseudocodice o utilizzando PlusCal. Devi imparare a scrivere le specifiche utilizzando specifiche formali. Questo ti darà le competenze necessarie che ti aiuteranno anche con quelle informali. Come puoi imparare a scrivere specifiche formali? Quando abbiamo imparato a programmare, abbiamo scritto programmi e poi ne abbiamo eseguito il debug. Stessa cosa qui: devi scrivere una specifica, controllarla con un controllo modello e correggere gli errori. TLA+ potrebbe non essere il linguaggio migliore per una specifica formale e un altro linguaggio sarebbe probabilmente più adatto alle tue esigenze specifiche. La cosa bella di TLA+ è che fa un ottimo lavoro nell'insegnare il pensiero matematico.
Come collegare specifica e codice? Utilizzo di commenti che collegano concetti matematici e la loro implementazione. Se lavori con i grafici, a livello di programma avrai matrici di nodi e matrici di collegamenti. Quindi è necessario scrivere come viene implementato esattamente il grafico da queste strutture di programmazione.
Va notato che nulla di quanto sopra si applica al processo di scrittura del codice stesso. Quando scrivi il codice, cioè esegui il terzo passaggio, devi anche pensare e riflettere attraverso il programma. Se un'attività secondaria risulta complessa o non ovvia, è necessario scriverne una specifica. Ma qui non sto parlando del codice in sé. Puoi utilizzare qualsiasi linguaggio di programmazione, qualsiasi metodologia, non si tratta di loro. Inoltre, nulla di quanto sopra elimina la necessità di testare ed eseguire il debug del codice. Anche se il modello astratto è scritto correttamente, potrebbero esserci dei bug nella sua implementazione.
La scrittura delle specifiche è un passaggio aggiuntivo nel processo di codifica. Grazie ad esso è possibile individuare molti errori con meno sforzo: lo sappiamo dall'esperienza dei programmatori di Amazon. Con le specifiche, la qualità dei programmi diventa più elevata. Allora perché allora ne facciamo così spesso a meno? Perché scrivere è difficile. Ma scrivere è difficile, perché per questo bisogna pensare, e anche pensare è difficile. È sempre più facile far finta di pensare. Qui puoi tracciare un'analogia con la corsa: meno corri, più lentamente corri. Devi allenare i muscoli ed esercitarti a scrivere. Ci vuole pratica.
La specifica potrebbe essere errata. Potresti aver commesso un errore da qualche parte, oppure i requisiti potrebbero essere cambiati o potrebbe essere necessario apportare un miglioramento. Qualsiasi codice utilizzato deve essere modificato, quindi prima o poi le specifiche non corrisponderanno più al programma. Idealmente, in questo caso, è necessario scrivere una nuova specifica e riscrivere completamente il codice. Sappiamo benissimo che nessuno lo fa. In pratica, patchiamo il codice e magari aggiorniamo le specifiche. Se questo è destinato ad accadere prima o poi, allora perché scrivere le specifiche? In primo luogo, per la persona che modificherà il tuo codice, ogni parola in più nella specifica varrà il suo peso in oro, e questa persona potresti essere tu. Spesso mi prendo a calci per non essere abbastanza specifico quando modifico il mio codice. E scrivo più specifiche che codice. Pertanto, quando si modifica il codice, è sempre necessario aggiornare la specifica. In secondo luogo, ad ogni modifica il codice peggiora, diventa più difficile da leggere e mantenere. Questo è un aumento di entropia. Ma se non inizi con una specifica, ogni riga che scrivi sarà una modifica e il codice sarà voluminoso e difficile da leggere fin dall'inizio.
Come detto , nessuna battaglia è stata vinta secondo un piano, e nessuna battaglia è stata vinta senza un piano. E sapeva qualcosa di battaglie. C'è un'opinione secondo cui scrivere le specifiche è una perdita di tempo. A volte questo è vero e il compito è così semplice che non ha senso pensarci a fondo. Ma dovresti sempre ricordare che quando ti viene consigliato di non scrivere le specifiche, significa che ti viene consigliato di non pensare. E dovresti pensarci ogni volta. Pensare attentamente a un compito non garantisce che non commetterai errori. Come sappiamo, nessuno ha inventato la bacchetta magica e programmare è un compito difficile. Ma se non pensi al compito, sei sicuro di commettere errori.
Puoi leggere ulteriori informazioni su TLA+ e PlusCal su un sito Web speciale, a cui puoi accedere dalla mia home page . Per me è tutto, grazie per l'attenzione.
Per favore ricorda che questa è una traduzione. Quando scrivi commenti, ricorda che l'autore non li leggerà. Se vuoi davvero chiacchierare 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