Scopri come le idee di Tony Hoare—logica di Hoare, Quicksort e mentalità di safety—hanno influenzato tecniche pratiche per scrivere e revisionare software corretto.
Quando le persone dicono che un programma è “corretto”, spesso intendono: “L'ho eseguito qualche volta e l'output sembrava giusto.” È un segnale utile, ma non è correttezza. In parole semplici, la correttezza significa che il programma soddisfa la sua specifica: per ogni input ammesso produce il risultato richiesto e rispetta le regole su modifiche di stato, tempi e errori.
Il problema è che “soddisfa la specifica” è più difficile di quanto sembri.
Prima di tutto, le specifiche sono spesso ambigue. Un requisito di prodotto può dire “ordina la lista”, ma questo significa un ordinamento stabile? Che succede con valori duplicati, liste vuote o elementi non numerici? Se la spec non lo dice, persone diverse assumeranno risposte diverse.
Secondo, i casi limite non sono rari—sono solo meno testati. Valori nulli, overflow, bordi off-by-one, sequenze d'uso insolite e guasti esterni imprevisti possono trasformare “sembra funzionare” in “ha fallito in produzione”.
Terzo, i requisiti cambiano. Un programma può essere corretto rispetto alla specifica di ieri e scorretto rispetto a quella di oggi.
Il contributo principale di Tony Hoare non fu dire che dobbiamo dimostrare tutto sempre. Fu l'idea che possiamo essere più precisi su ciò che il codice deve fare—e ragionarci in modo disciplinato.
In questo post seguiremo tre fili connessi:
La maggior parte dei team non scriverà prove formali complete. Ma anche un ragionamento parziale, “in stile prova”, può rendere i bug più facili da individuare, rendere le review più efficaci e chiarire il comportamento prima che il codice venga rilasciato.
Tony Hoare è uno di quei rari informatici il cui lavoro non è rimasto solo su articoli o in aula. Ha mosso tra accademia e industria, e si è occupato di una domanda pratica che ogni team ancora si pone: come sappiamo che un programma fa quello che pensiamo faccia—soprattutto quando la posta in gioco è alta?
Questo articolo si concentra su alcune idee di Hoare che ricompaiono nei codebase reali:
{P} C {Q}.Non troverai formalismi matematici profondi qui, e non tenteremo una prova completa e verificabile di Quicksort. L'obiettivo è mantenere i concetti accessibili: abbastanza struttura da rendere il tuo ragionamento più chiaro, senza trasformare la review del codice in un seminario di dottorato.
Le idee di Hoare si traducono in decisioni ordinarie: quali assunzioni una funzione richiede, cosa garantisce ai chiamanti, cosa deve rimanere vero a metà di un loop e come individuare cambiamenti “quasi corretti” durante le review. Anche se non scrivi esplicitamente {P} C {Q}, pensare in quella forma migliora API, test e la qualità delle discussioni su codice complesso.
La visione di Hoare è più restrittiva di “ha passato qualche esempio”: la correttezza riguarda il rispetto di una promessa concordata, non l'aspetto giusto su un piccolo campione.
I bug spesso accadono quando i team saltano il passo intermedio: passano dai requisiti direttamente al codice, lasciando la “promessa” vaga.
Due affermazioni diverse vengono frequentemente confuse:
Per i sistemi reali, “non finire mai” può essere tanto dannoso quanto “finire col risultato sbagliato”.
Le affermazioni di correttezza non sono mai universali; si basano su assunzioni su:
Esplicitare le assunzioni trasforma “funziona sulla mia macchina” in qualcosa su cui altri possono ragionare.
Considera una funzione sortedCopy(xs).
Una specifica utile potrebbe essere: “Restituisce una nuova lista ys tale che (1) ys è ordinata in modo crescente, e (2) ys contiene esattamente gli stessi elementi di xs (stesse occorrenze), e (3) xs rimane invariata.”
Ora “corretto” significa che il codice soddisfa quei tre punti sotto le assunzioni dichiarate—non solo che l'output sembrava ordinato in un test veloce.
La logica di Hoare è un modo di parlare del codice con la stessa chiarezza che useresti per un contratto: se inizi in uno stato che soddisfa certe assunzioni e esegui questo frammento di codice, finirai in uno stato che soddisfa certe garanzie.
La notazione centrale è la tripla di Hoare:
{precondition} program {postcondition}
Una precondizione dice cosa deve essere vero prima che il frammento di programma venga eseguito. Non si tratta di ciò che speri sia vero; è ciò di cui il codice ha bisogno.
Esempio: supponi una funzione che calcola la media di due numeri senza controlli di overflow.
a + b rientra nel tipo intero\n- Programma: avg = (a + b) / 2\n- Postcondizione: avg è la media matematica di a e bSe la precondizione non tiene (l'overflow è possibile), la promessa della postcondizione non vale più. La tripla ti costringe a dirlo chiaramente.
Una postcondizione dichiara cosa sarà vero dopo l'esecuzione—assumendo che la precondizione fosse soddisfatta. Buone postcondizioni sono concrete e verificabili. Invece di “il risultato è valido”, dì cosa significa “valido”: ordinato, non negativo, entro limiti, invariato tranne per campi specifici, ecc.
La logica di Hoare scala da piccole istruzioni a blocchi multi-step:
x = x + 1, quali fatti su x sono veri?\n- Sequenza (fai questo, poi quello) concatena le garanzie: se il passo 1 stabilisce la precondizione per il passo 2, il blocco complessivo è più facile da fidare.Il punto non è mettere triplette ovunque. È rendere l'intento leggibile: assunzioni chiare, risultati chiari e meno conversazioni “sembra funzionare” nelle review.
Un'invariante di ciclo è un'affermazione vera prima che il ciclo inizi, che rimane vera dopo ogni iterazione e che è ancora vera quando il ciclo termina. È un'idea semplice con grande rendimento: sostituisce il “sembra funzionare” con un'affermazione che puoi verificare a ogni passo.
Senza un'invariante, una review spesso suona: “Iteriamo sulla lista e gradualmente sistemiamo le cose.” Un'invariante impone precisione: cosa è già corretto adesso, anche se il ciclo non è finito? Quando puoi dirlo chiaramente, errori off-by-one e casi mancanti diventano più facili da individuare, perché si manifestano come momenti in cui l'invariante verrebbe violata.
La maggior parte del codice quotidiano può usare alcuni template affidabili.
Mantieni gli indici in un intervallo sicuro.
0 <= i <= n\n- low <= left <= right <= highQuesto tipo di invariante è ottimo per prevenire accessi fuori range e rendere concreta la ragioneria degli array.
Dividi i dati in una regione “fatta” e una “non ancora”.
a[0..i) sono stati esaminati.”\n- “Ogni elemento spostato in result soddisfa il predicato di filtro.”Questo trasforma un progresso vago in un contratto chiaro su cosa significa “processato”.
Comune in ordinamenti, merge e partizionamenti.
a[0..i) è ordinato.”\n- “Tutti gli elementi in a[0..i) sono <= pivot, e tutti gli elementi in a[j..n) sono >= pivot.”Anche se l'array completo non è ordinato, hai fissato cosa lo è.
La correttezza non riguarda solo l'essere giusti; il ciclo deve anche terminare. Un modo semplice per argomentarlo è nominare una misura che diminuisce a ogni iterazione e non può diminuire indefinitamente.
Esempi:
n - i si riduce di 1 ogni volta.”\n- “Il numero di elementi non processati diminuisce.”Se non trovi una misura che si riduce, potresti aver scoperto un rischio reale: un ciclo infinito su alcuni input.
Quicksort ha una promessa semplice: dato un segmento di array, riorganizza gli elementi affinché risultino in ordine non decrescente, senza perdere o inventare valori. La forma ad alto livello dell'algoritmo è facile da riassumere:
È un ottimo esempio didattico per la correttezza perché è piccolo abbastanza da tenerlo a mente, ma ricco abbastanza da mostrare dove il ragionamento informale fallisce. Un Quicksort che “sembra funzionare” su alcuni test può comunque essere sbagliato in modi che emergono solo su input specifici o casi limite.
Alcuni problemi causano la maggior parte dei bug:
Per argomentare la correttezza in modo Hoare-style, normalmente si separa la prova in due parti:
Questa separazione mantiene il ragionamento gestibile: sistema prima la partizione, poi costruisci la correttezza dell'ordinamento sopra di essa.
La velocità di Quicksort dipende da una routine apparentemente piccola: la partizione. Se la partizione è anche solo leggermente sbagliata, Quicksort può ordinare male, andare in loop infinito o bloccarsi su casi limite.
Useremo lo schema classico di partizione di Hoare (due puntatori che si muovono verso l'interno).
Input: una porzione di array A[lo..hi] e un valore pivot scelto (spesso A[lo]).
Output: un indice p tale che:
A[lo..p] è <= pivot\n- ogni elemento in A[p+1..hi] è >= pivotNota cosa non è promesso: il pivot non necessariamente finisce in posizione p, e gli elementi uguali al pivot possono apparire su entrambi i lati. Va bene così: Quicksort ha solo bisogno di uno split corretto.
Mentre l'algoritmo fa avanzare due indici—i da sinistra e j da destra—un buon ragionamento si concentra su cosa è già “bloccato”. Un insieme pratico di invarianti è:
A[lo..i-1] sono <= pivot (il lato sinistro è pulito)\n- tutti gli elementi in A[j+1..hi] sono >= pivot (il lato destro è pulito)\n- tutto in A[i..j] è non classificato (ancora da controllare)Quando trovi A[i] > pivot e A[j] < pivot, scambiandoli preservi queste invarianti e restringi il segmento non classificato.
i scorre verso destra; la partizione deve comunque terminare e restituire un p sensato.\n- Tutti più grandi del pivot: j scorre verso sinistra; stessa preoccupazione di terminazione.\n- Molti uguali: se le comparazioni sono incoerenti (< vs <=), i puntatori possono bloccarsi. Lo schema di Hoare si basa su una regola coerente per mantenere il progresso.\n- Già ordinato / ordinato inversamente: non deve spezzare il contratto, anche se le prestazioni peggiorano.Esistono diversi schemi di partizione (Lomuto, Hoare, partizionamento a tre vie). L'importante è sceglierne uno, dichiararne il contratto e rivedere il codice rispetto a quel contratto in modo coerente.
La ricorsione è più facile da fidare quando puoi rispondere a due domande chiaramente: quando si ferma? e perché ogni passo è valido? Il pensiero in stile Hoare aiuta perché ti costringe a dire cosa deve essere vero prima di una chiamata e cosa sarà vero dopo il suo ritorno.
Una funzione ricorsiva ha bisogno di almeno un caso base dove non fa ulteriori chiamate ricorsive e soddisfa comunque il risultato promesso.
Per l'ordinamento, un caso base tipico è “array di lunghezza 0 o 1 sono già ordinati.” Qui, “ordinato” dovrebbe essere esplicito: per una relazione ≤, l'array è ordinato se per ogni indice i < j, abbiamo a[i] ≤ a[j]. (Se gli elementi uguali mantengono l'ordine originale è una proprietà separata chiamata stabilità; Quicksort di solito non è stabile a meno che non sia progettato per esserlo.)
Ogni passo ricorsivo deve chiamare se stesso su un input strettamente più piccolo. Questa “riduzione” è l'argomento di terminazione: se la dimensione diminuisce e non può scendere sotto 0, non puoi ricorrere all'infinito.
La riduzione conta anche per la sicurezza dello stack. Anche codice corretto può crashare se la profondità di ricorsione diventa troppo grande. In Quicksort, partizioni sbilanciate possono produrre ricorsione profonda. È un argomento di terminazione ma anche un promemoria pratico per considerare la profondità massima possibile.
Il caso peggiore di Quicksort può degradare a O(n²) quando le partizioni sono molto sbilanciate, ma questo è un problema di prestazioni—non un fallimento di correttezza. L'obiettivo qui è: assumendo che la partizione preservi gli elementi e li divida secondo il pivot, l'ordinamento ricorsivo delle parti più piccole implica che l'intero intervallo soddisfi la definizione di ordinamento.
Testing e ragionamento in stile prova mirano allo stesso obiettivo—fiducia—ma ci arrivano in modi diversi.
I test sono eccellenti per trovare errori concreti: un off-by-one, un caso limite mancante, una regressione. Ma una suite di test può solo campionare lo spazio di input. Anche la “copertura al 100%” non significa “tutti i comportamenti verificati”; per lo più significa “tutte le righe eseguite”.
Il ragionamento in stile prova (in particolare la logica di Hoare) parte da una specifica e chiede: se queste precondizioni valgono, il codice stabilisce sempre le postcondizioni? Quando lo fai bene, non solo trovi un bug: spesso elimini una categoria intera di errori (per esempio “gli accessi agli array restano entro i limiti” o “il loop non viola la proprietà di partizione”).
Una specifica chiara è un generatore di test.
Se la tua postcondizione dice “l'output è ordinato ed è una permutazione dell'input”, ottieni automaticamente idee di test:
La spec ti dice cosa significa “corretto” e i test verificano che la realtà corrisponda.
Il testing basato su proprietà sta tra le prove e gli esempi. Invece di selezionare manualmente pochi casi, dichiari proprietà e lasci a uno strumento la generazione di molti input.
Per l'ordinamento, due proprietà semplici vanno molto lontano:
Queste proprietà sono essenzialmente postcondizioni scritte come check eseguibili.
Una routine leggera che scala:
Se vuoi istituzionalizzarlo, rendi “spec + note di ragionamento + test” parte del template PR o della checklist di code review (vedi anche /blog/code-review-checklist).
Se usi un flusso di lavoro basato su generazione (vibe-coding) da interfacce conversazionali, la stessa disciplina si applica—forse ancora di più. In Koder.ai, per esempio, puoi iniziare in Planning Mode per fissare precondizioni/postcondizioni prima di generare codice, poi iterare con snapshot e rollback mentre aggiungi property-based tests. Lo strumento accelera l'implementazione, ma è la specifica che impedisce al “veloce” di diventare “fragile”.
La correttezza non è solo “il programma restituisce il valore giusto”. La mentalità di safety pone una domanda diversa: quali esiti sono inaccettabili, e come li preveniamo—anche quando il codice è sotto stress, mal usato o parzialmente guasto? In pratica, la safety è la correttezza con un sistema di priorità: alcuni fallimenti sono solo fastidiosi, altri possono causare perdite finanziarie, violazioni della privacy o danni fisici.
Un bug è un difetto nel codice o nel design. Un pericolo (hazard) è una situazione che può portare a un esito inaccettabile. Un bug può essere innocuo in un contesto e pericoloso in un altro.
Esempio: un off-by-one in una galleria di foto può etichettare male un'immagine; lo stesso errore in un calcolatore di dosi mediche potrebbe danneggiare un paziente. La mentalità di safety ti costringe a collegare il comportamento del codice alle conseguenze, non solo alla conformità alla spec.
Non servono metodi formali pesanti per ottenere benefici immediati di safety. I team possono adottare pratiche piccole e ripetibili:
Queste tecniche si abbinano naturalmente al ragionamento in stile Hoare: rendi esplicite le precondizioni (quali input sono accettabili) e assicurati che le postcondizioni includano proprietà di safety (cosa non deve mai accadere).
I controlli orientati alla safety hanno un costo—tempo CPU, complessità o occasionali rifiuti legittimi.
La mentalità di safety è meno sul dimostrare eleganza e più sul prevenire i modi di guasto che non possiamo permetterci.
Le code review sono il luogo dove il pensiero sulla correttezza paga più in fretta, perché puoi individuare assunzioni mancanti molto prima che i bug arrivino in produzione. La mossa centrale di Hoare—enunciare cosa deve essere vero prima e cosa sarà vero dopo—si traduce bene in domande di review.
Quando leggi una modifica, prova a inquadrare ogni funzione chiave come una piccola promessa:
Un'abitudine semplice per il reviewer: se non riesci a dire pre/post in una frase, probabilmente il codice ha bisogno di una struttura più chiara.
Per funzioni rischiose o centrali, aggiungi un piccolo commento contratto sopra la firma. Sii concreto: input, output, effetti collaterali ed errori.
def withdraw(account, amount):
"""Contract:
Pre: amount is an integer > 0; account is active.
Post (success): returns new_balance; account.balance decreased by amount.
Post (failure): raises InsufficientFunds; account.balance unchanged.
"""
...
Questi commenti non sono prove formali, ma danno ai revisori qualcosa di preciso da controllare.
Sii esplicito in modo extra quando rivedi codice che gestisce:
Se la modifica tocca uno di questi ambiti, chiedi: “Quali sono le precondizioni e dove vengono fatte rispettare?” e “Quali garanzie forniamo anche in presenza di errori?”.
Il ragionamento formale non significa trasformare tutto il codebase in un articolo matematico. L'obiettivo è spendere certezza extra dove conviene: parti dove “sembra a posto nei test” non è sufficiente.
Sono indicati quando hai un modulo piccolo e critico su cui tutto il resto dipende (auth, regole di pagamento, permessi, interblocchi di safety), o un algoritmo insidioso dove errori off-by-one si nascondono per mesi (parser, scheduler, caching/eviction, primitive concorrenti, codice con molte frontiere).\n Una regola utile: se un bug può causare danno reale, grossa perdita finanziaria o corruzione silenziosa dei dati, vuoi più di review e test ordinari.
Puoi scegliere dall'“leggero” al “pesante”, e spesso la miglior soluzione combina tecniche:
Decidi la profondità della formalità valutando:
Nella pratica puoi trattare la “formalità” come qualcosa da aggiungere gradualmente: comincia con contratti e invarianti espliciti, poi metti l'automazione a mantenerti onesto. Per team che costruiscono velocemente con Koder.ai—dove generare un front end React, un backend Go e uno schema Postgres avviene in breve—snapshot/rollback e export sorgente rendono più facile iterare in fretta mantenendo contratti via test e analisi statica nella CI abituale.
Usala come gate rapido “dobbiamo formalizzare di più?” in pianificazione o review:
Letture consigliate: design-by-contract, property-based testing, model checking per macchine a stati, analizzatori statici per il tuo linguaggio e materiale introduttivo su proof assistant e specifica formale.
La correttezza significa che il programma soddisfa una specifica concordata: per ogni input ammesso e stato rilevante del sistema, produce gli output e gli effetti collaterali richiesti (e gestisce gli errori come promesso). “Sembra funzionare” di solito significa che hai controllato pochi esempi, non l'intero spazio di input o i casi limite più insidiosi.
I requisiti sono l'obiettivo di business in linguaggio naturale (“ordina la lista per la visualizzazione”). Una specifica è la promessa precisa e verificabile (“restituisce una nuova lista ordinata in ordine crescente, stesso multiset di elementi, input invariato”). L'implementazione è il codice. I bug spesso nascono quando il team salta la specifica e passa direttamente dai requisiti al codice senza definire la promessa verificabile.
Correttezza parziale: se il codice torna, il risultato è corretto. Correttezza totale: il codice torna e il risultato è corretto—quindi la terminazione fa parte dell'affermazione.
Nella pratica, la correttezza totale conta quando “rimanere bloccati” è un guasto visibile all'utente, una perdita di risorse o un rischio per la sicurezza.
Una tripla di Hoare {P} C {Q} si legge come un contratto:
P (precondizione): ciò che deve essere vero prima di eseguire CLe precondizioni sono ciò di cui il codice ha bisogno (per esempio: “gli indici sono nel range”, “gli elementi sono confrontabili”, “il lock è acquisito”). Se una precondizione può essere violata dai chiamanti, o:
Altrimenti, le tue postcondizioni diventano desideri anziché garanzie.
Un'invariante di ciclo è un'affermazione vera prima dell'inizio del ciclo, che rimane vera dopo ogni iterazione e che è ancora vera quando il ciclo finisce. Template utili includono:
0 <= i <= n)Se non riesci a formulare un'invariante, è un segnale che il ciclo fa troppe cose insieme o che i confini non sono chiari.
Tipicamente si nomina una misura (variant) che diminuisce a ogni iterazione e non può diminuire all'infinito, per esempio:
n - i che diminuisce di 1Se non trovi una misura decrescente, potresti aver individuato un rischio reale di non-terminazione (specialmente con duplicati o puntatori che si bloccano).
In Quicksort, la partizione è la routine piccola da cui dipende tutto. Se la partizione è anche leggermente sbagliata, possono verificarsi:
Per questo è utile dichiarare esplicitamente il contratto della partizione: cosa deve essere vero a sinistra, a destra, e che gli elementi sono solo riorganizzati (permutazione).
I duplicati e la gestione degli elementi uguali al pivot sono punti frequenti di rottura. Regole pratiche:
i/j si blocchino)Se i duplicati sono frequenti, considera la partizione a tre vie per ridurre sia i bug sia la profondità di ricorsione.
I test trovano errori concreti; il ragionamento può escludere intere classi di bug (sicurezza dei bordi, preservazione delle invarianti, terminazione). Un flusso pratico ibrido è:
Per l'ordinamento, due proprietà ad alto valore sono:
CQ (postcondizione): ciò che sarà vero dopo che C termina, assumendo che P fosse veraNon serve scrivere la notazione nel codice: usare la struttura nelle review (“assunzioni in, garanzie out”) è il guadagno pratico.