KomuraSoft LLC
Contatti
Menu

Introduzione alla verifica formale con SPARK ── Dai contratti Ada alla dimostrazione matematica

· · Ada, SPARK, Verifica Formale, GNATprove, Progettazione per Contratto, Alta Integrità, Linguaggio di Programmazione, Alta Affidabilità

1. Introduzione ── Oltre l’«eseguire e verificare»

Il modo più comune per garantire la qualità del software è il testing.

Test: verifica che il programma si comporti correttamente per gli input selezionati

Ma il testing ha limiti intrinseci. Il numero di input possibili è infinito, e i test da soli non possono dimostrare la correttezza per tutti.

Qui entra in gioco la verifica formale (Formal Verification).

Verifica formale: dimostra matematicamente che una proprietà vale per tutti gli input possibili

L’articolo precedente, «Il fascino del linguaggio Ada», ha offerto una panoramica di Ada e ha accennato brevemente a SPARK.

Questo articolo si concentra specificamente sulla verifica formale pratica con SPARK e affronta i seguenti punti:

Cos'è SPARK e il suo rapporto con Ada
Come scrivere contratti (Pre/Post)
Come dimostrarli con GNATprove
Come progettare invarianti di ciclo
Come gestire gli effetti collaterali con i contratti di flusso dati (Global/Depends)
Una strategia di adozione graduale tramite i livelli di dimostrazione (da Stone a Platinum)
Come integrare SPARK in progetti reali

L’obiettivo è farvi vivere il passaggio dal testing alla dimostrazione attraverso esempi di codice funzionanti.

I frammenti di codice di questo articolo sono disponibili, organizzati per capitolo, come raccolta di riferimento su GitHub.

ada-spark-formal-verification - komurasoft-blog-samples (GitHub)

2. Cos’è SPARK ── Il sottoinsieme di Ada come porta d’accesso al mondo della dimostrazione

SPARK è un sottoinsieme del linguaggio Ada.

Essere un sottoinsieme è una scelta progettuale deliberata.

Ada completo → altamente espressivo, ma verificarlo interamente non è realistico
SPARK        → ristretto alle funzionalità verificabili, il che rende la dimostrazione realistica

Le principali restrizioni imposte da SPARK sono:

Gestione dinamica della memoria tramite puntatori (tipi access) → controllata da un modello di ownership
Uso libero dei gestori di eccezioni                              → consentito in forma ristretta
Strutture dati ricorsive                                          → ristrette perché difficili da dimostrare
Uso libero del tasking                                            → ristretto tramite il profilo Ravenscar

Il termine «restrizioni» può sembrare limitante, ma queste restrizioni sono il prezzo della dimostrabilità.

Il cuore degli strumenti SPARK è GNATprove, fornito da AdaCore.

Come funziona GNATprove:
1. Analizza codice Ada annotato con SPARK
2. Traduce i contratti (Pre/Post) e le asserzioni nel linguaggio intermedio Why3
3. Tenta dimostrazioni con dimostratori automatici come Z3, CVC4 e Alt-Ergo
4. Riporta i risultati come messaggi direttamente sul codice sorgente

Un aspetto cruciale: SPARK è costruito sopra Ada.

Codice SPARK = codice Ada + annotazioni contrattuali

In altre parole, SPARK è un’estensione naturale dello sviluppo Ada quotidiano. Non c’è bisogno di imparare una sintassi completamente nuova.

3. Installare GNATprove e la prima dimostrazione

Iniziamo preparando un ambiente per eseguire GNATprove.

Con Alire è possibile creare un progetto pronto per SPARK con il seguente comando:

alr init --bin spark_demo
cd spark_demo

Poiché GNATprove è incluso nel compilatore GNAT, il comando gnatprove è disponibile non appena il progetto compila con alr build.

Come primo obiettivo di dimostrazione, scriviamo una funzione che restituisce il valore assoluto.

package Simple_Proof with SPARK_Mode is

   function Abs_Value (X : Integer) return Integer
     with Post => Abs_Value'Result >= 0;

end Simple_Proof;

package body Simple_Proof with SPARK_Mode is

   function Abs_Value (X : Integer) return Integer is
   begin
      if X < 0 then
         return -X;
      else
         return X;
      end if;
   end Abs_Value;

end Simple_Proof;

Punti chiave da notare:

with SPARK_Mode va aggiunto sia alla specifica del pacchetto sia al corpo
La condizione Post dichiara la proprietà «il risultato è non negativo»
L'attributo 'Result permette di riferirsi al valore restituito dalla funzione

Ora eseguiamo GNATprove su questo codice:

gnatprove -P spark_demo.gpr

Il risultato sarà simile a questo:

SUMMARY
-------
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
simple_proof.adb:5:15: info: range check proved
simple_proof.adb:6:16: info: range check proved
simple_proof.ads:3:19: info: postcondition proved

Il messaggio postcondition proved significa che è stato matematicamente dimostrato che, per tutti i possibili input Integer, il valore restituito è non negativo.

Questa è l’esperienza d’ingresso in SPARK.

4. Fondamenti della progettazione per contratto ── Scrivere Pre e Post

Le dimostrazioni SPARK iniziano con la scrittura dei contratti.

I contratti sono una funzionalità del linguaggio Ada 2012, ma in SPARK diventano l’input della dimostrazione.

procedure Transfer (From, To : in out Account; Amount : Positive)
  with Pre  => From.Balance >= Amount,
       Post => From.Balance = From.Balance'Old - Amount
                and then
                To.Balance = To.Balance'Old + Amount;

Linee guida per progettare Pre e Post:

Pre (precondizione):
  Responsabilità del chiamante
  «Se mi chiami soddisfacendo questa condizione, garantisco la Post»
  Abbastanza debole da essere soddisfacibile, abbastanza forte da essere utile

Post (postcondizione):
  Responsabilità dell'implementazione
  «Dopo la chiamata, il mondo si trova in questo stato»
  L'attributo 'Old permette di riferirsi ai valori precedenti alla chiamata
  Troppo forte rende l'implementazione troppo vincolata; troppo debole non dimostra nulla di utile

Errori comuni e come evitarli:

Errore 1: Pre troppo forte
  Pre => X > 0 and X < 100 and X /= 50 and ...
  → Verificare: il chiamante può sempre soddisfare questa condizione?
  → Non restringere Pre solo perché i test passano

Errore 2: Post troppo debole
  Post => True
  → Non garantisce nulla. La dimostrazione è priva di significato.

Errore 3: Dimenticare gli effetti collaterali in Post
  Post => Result = X * 2  (aggiornamento di una variabile globale trascurato)
  → Rendere espliciti gli effetti collaterali con i contratti Global/Depends (sezione 9)

5. Dimostrare l’assenza di overflow ── Garantire la sicurezza numerica

Una delle cose più preziose in pratica che SPARK può dimostrare è l’assenza di overflow.

Considerate questo codice:

procedure Increment (X : in out Integer)
  with SPARK_Mode,
       Pre  => X < Integer'Last,
       Post => X = X'Old + 1;

Pre => X < Integer'Last è la chiave. Con questo contratto, GNATprove può dimostrare che l’addizione non andrà in overflow.

Senza contratto, GNATprove avverte di un possibile overflow:

medium: overflow check might fail

Lo stesso vale per calcoli più complessi:

function Average (A, B : Integer) return Integer
  with SPARK_Mode,
       Pre  => (if A >= 0 and B >= 0 then A <= Integer'Last - B
                elsif A < 0 and B < 0 then A >= Integer'First - B),
       Post => (if A <= B then A <= Average'Result and Average'Result <= B
                else B <= Average'Result and Average'Result <= A);

La Pre appare complessa, ma esprime semplicemente che «la somma A+B non va in overflow», con una distinzione dei casi basata sul segno.

Punto chiave:
  L'essenza della dimostrazione di assenza di overflow consiste nel
  dichiarare in Pre che il risultato di un'addizione o moltiplicazione
  rientra nei limiti del tipo
  Può sembrare noioso, ma una volta scritto, non vi affliggerà mai più
  un bug di overflow

6. Invarianti di ciclo ── Dimostrare le proprietà dei cicli

Una delle parti più difficili della verifica formale è la dimostrazione dei cicli.

I cicli si eseguono un numero arbitrario di volte, quindi il testing non può coprire tutti i casi. SPARK utilizza a questo scopo gli invarianti di ciclo (Loop Invariants).

function Sum_Of_Naturals (N : Natural) return Natural
  with SPARK_Mode,
       Post => Sum_Of_Naturals'Result = (N * (N + 1)) / 2;

function Sum_Of_Naturals (N : Natural) return Natural is
   Result : Natural := 0;
begin
   for I in 1 .. N loop
      Result := Result + I;
      pragma Loop_Invariant (Result = (I * (I + 1)) / 2);
   end loop;
   return Result;
end Sum_Of_Naturals;

Progettare invarianti di ciclo richiede il seguente approccio:

1. Scrivere una proprietà vera all'inizio di ogni iterazione
2. Sceglierne una che, dopo l'ultima iterazione, implichi la Post desiderata
3. L'invariante esprime come formula il calcolo parziale svolto fino a quel punto

Ecco un altro esempio: la ricerca in un array.

function Find (Arr : Array_Of_Integer; Target : Integer) return Natural
  with SPARK_Mode,
       Post => (if Find'Result = 0 then
                  (for all K in Arr'Range => Arr (K) /= Target)
                else
                  Arr (Find'Result) = Target);

function Find (Arr : Array_Of_Integer; Target : Integer) return Natural is
begin
   for I in Arr'Range loop
      if Arr (I) = Target then
         return I;
      end if;
      pragma Loop_Invariant
        (for all K in Arr'First .. I => Arr (K) /= Target);
   end loop;
   return 0;
end Find;

L’invariante qui è: «nell’intervallo esaminato finora, Target non esiste».

Principi per la progettazione di invarianti di ciclo:
  Esprimere come formula: «dopo n iterazioni, cosa possiamo affermare?»
  Nei cicli su array, lo schema tipico è «per l'intervallo già elaborato, vale P»
  Un invariante troppo forte non si riesce a dimostrare; troppo debole non implica la Post
  Trovare il giusto equilibrio è l'arte vera e propria della dimostrazione sui cicli

7. Pragma di asserzione ── Proprietà parziali nel codice

Oltre ai contratti (Pre/Post), SPARK consente di scrivere asserzioni (Assert) direttamente nel corpo del codice.

procedure Divide (A, B : Integer; Q, R : out Integer)
  with SPARK_Mode,
       Pre  => B /= 0,
       Post => A = Q * B + R and R >= 0 and R < abs (B);

procedure Divide (A, B : Integer; Q, R : out Integer) is
begin
   Q := A / B;
   R := A rem B;

   pragma Assert (A = Q * B + R);
   pragma Assert (R >= 0);
   pragma Assert (R < abs (B));
end Divide;

Uso dei diversi pragma:

Pre/Post:       Promesse all'ingresso e all'uscita del sottoprogramma
Assert:         Una proprietà che deve valere in un punto specifico del codice
Loop_Invariant: Una proprietà mantenuta a ogni iterazione del ciclo
Loop_Variant:   Una quantità decrescente per dimostrare la terminazione del ciclo

Buoni casi d’uso per Assert:

Verificare risultati intermedi di calcoli complessi
Controllare lo stato dopo un ramo if/else
Confermare proprietà dei valori restituiti dopo una chiamata di procedura
Fornire lemmi che facilitano le dimostrazioni successive

8. Contratti di flusso dati ── Global e Depends

Una delle funzionalità potenti di SPARK sono i contratti di flusso dati.

Dichiarano esplicitamente quali variabili globali un sottoprogramma legge e scrive.

package Counter_Unit with SPARK_Mode is

   Count : Natural := 0;

   procedure Increment
     with Global => (In_Out => Count);

   procedure Reset
     with Global => (Output => Count);

   function Get_Value return Natural
     with Global => (Input => Count);

end Counter_Unit;

I modi del contratto Global sono:

Input:  sola lettura (per le funzioni)
Output: sola scrittura (per l'inizializzazione)
In_Out: lettura e scrittura (per gli aggiornamenti)

Inoltre, le dipendenze tra variabili possono essere espresse con Depends:

procedure Transfer
  (From, To : in out Account_Type)
  with Global => (Input => Exchange_Rate),
       Depends => (From =>+ (From, Exchange_Rate),
                   To   =>+ (To, Exchange_Rate));

=>+ significa «dipende dal valore precedente più questi input aggiuntivi».

Vantaggi dei contratti di flusso dati:
  1. «Cosa tocca questa funzione?» si vede a colpo d'occhio
  2. Gli effetti collaterali non intenzionali vengono rilevati in compilazione
  3. Alimentano l'analisi del flusso di informazioni delle variabili
  4. Aiutano a visualizzare il flusso dati nei sistemi di grandi dimensioni

9. Livelli di dimostrazione ── Adozione graduale da Stone a Platinum

SPARK definisce il concetto di livelli di dimostrazione (Proof Levels).

Cercare di dimostrare completamente tutto il codice in una volta porta spesso alla frustrazione. SPARK offre quindi una strategia per aumentare gradualmente il rigore della dimostrazione.

Stone (livello 0):
  Solo verifica della sintassi dei contratti e della coerenza dei tipi
  Il primo livello da raggiungere

Bronze (livello 1):
  Stone + dimostrazione dell'assenza di letture di variabili non inizializzate
  Garanzia di correttezza di base

Silver (livello 2):
  Bronze + dimostrazione dell'assenza di errori a runtime (fuori limiti,
  overflow, divisione per zero)
  L'obiettivo più pragmatico

Gold (livello 3):
  Silver + dimostrazione delle condizioni Pre/Post
  Garanzia di correttezza funzionale completa

Platinum (livello 4):
  Gold + dimostrazione della non interferenza dei dati e del flusso
  di informazioni
  Per sistemi orientati alla sicurezza

Una strategia di adozione pratica:

Fase 1: portare l'intero progetto al livello Stone
  → Individuare errori di scrittura nei contratti

Fase 2: portare i moduli critici al livello Silver
  → Eliminare overflow e accessi fuori limite
  → La maggior parte dei bug reali viene evitata qui

Fase 3: dimostrare la logica centrale al livello Gold
  → Garantire matematicamente la correttezza funzionale
  → Dimostrare la correttezza degli algoritmi

Fase 4: passare a Platinum se ci sono requisiti di sicurezza
  → Individuare percorsi di fuga di informazioni

10. Un flusso di lavoro pratico per la dimostrazione ── Ridurre i ripensamenti

Ecco un flusso di lavoro per usare GNATprove quotidianamente:

1. Progettare tipi e specifiche
   Decidere i vincoli di intervallo e gli invarianti di tipo

2. Scrivere i contratti (Pre/Post)
   Esprimere la specifica come contratto prima dell'implementazione

3. Far compilare il codice
   Risolvere gli errori di compilazione con GNAT

4. Eseguire GNATprove al livello Stone
   gnatprove -P proj.gpr --level=0

5. Esaminare gli avvisi e affinare i contratti se necessario
   Prestare particolare attenzione ai problemi di inizializzazione

6. Puntare al livello Silver
   gnatprove -P proj.gpr --level=2
   Eliminare tutti gli errori a runtime

7. Aggiungere invarianti di ciclo dove necessario
   Se una dimostrazione fallisce, verificare se mancano invarianti

8. Dimostrare la correttezza funzionale al livello Gold
   gnatprove -P proj.gpr --level=3

Casi comuni di «impossibile dimostrare» e come gestirli:

Caso 1: «medium: postcondition might fail»
  → Post troppo forte, oppure Pre troppo debole
  → Oppure invarianti di ciclo insufficienti

Caso 2: «medium: overflow check might fail»
  → Restringere gli intervalli di valori in Pre
  → Oppure restringere l'intervallo del tipo stesso

Caso 3: «medium: array index check might fail»
  → Usare un invariante di ciclo per mostrare che l'intervallo del ciclo
    rientra nei limiti dell'array
  → Usare for I in Arr'Range per aiutare il riconoscimento automatico
    dei limiti da parte di SPARK

Caso 4: «prover timeout»
  → Il dimostratore ha esaurito il tempo; suddividere con invarianti
    graduali
  → Suddividere le funzioni grandi in funzioni più piccole

11. Usare insieme SPARK e il testing ── Comprendere la relazione di complementarità

La verifica formale e il testing non sono avversari; si completano a vicenda.

Dimostrazioni SPARK:
  Dimostrano proprietà per tutti gli input possibili
  Coprono solo le proprietà scritte nei contratti
  I casi non dimostrabili vengono affidati alla revisione manuale o al testing

Testing:
  Verifica il comportamento reale per gli input selezionati
  Può scoprire assunzioni implicite non scritte nei contratti
  Può verificare l'interazione con l'ambiente di esecuzione

Schemi di utilizzo combinato:

1. Garantire l'assenza di errori a runtime (livello Silver) con SPARK
2. Verificare la correttezza concreta di input/output con test unitari
3. Dimostrare la logica centrale al livello Gold
4. Concentrare i test sulle parti non dimostrabili

Ada dispone del framework di test unitari AUnit. Una combinazione pratica consiste nel consolidare tipi e contratti con SPARK, per poi testare il comportamento con AUnit.

12. Leggere i risultati di GNATprove ── Interpretare i messaggi

L’output di GNATprove ha tre livelli di gravità:

info:   dimostrazione riuscita
medium: dimostrazione fallita (avviso). Serve una revisione manuale
high:   dimostrazione fallita (errore). Probabile violazione del contratto

Messaggi comuni e il loro significato:

«postcondition proved»          la condizione Post è stata dimostrata
«range check proved»            il controllo di intervallo è stato dimostrato
«overflow check proved»         è stata dimostrata l'assenza di overflow
«index check proved»            sono stati dimostrati i limiti dell'indice dell'array
«divide by zero check proved»   è stata dimostrata l'assenza di divisione per zero

«might fail»                    non è stato possibile dimostrarlo
«cannot prove»                  il dimostratore non è riuscito a completare la dimostrazione
«prover timeout»                la dimostrazione non si è conclusa entro il limite di tempo

Procedura da seguire quando compare might fail:

1. Leggere il codice e valutare se può realmente fallire
2. Se può fallire, correggere il codice
3. Se in teoria non dovrebbe fallire, rafforzare il contratto (Pre / invariante)
4. Se ancora non si riesce a dimostrare, dichiararlo come assunzione con
   pragma Assume (attenzione: Assume è un'assunzione non dimostrata, va
   usata con cautela)

13. Integrazione in progetti reali

Ecco un approccio realistico per introdurre SPARK in un progetto esistente:

1. Iniziare dal codice nuovo
   Non cercare di convertire tutto il codice esistente in SPARK in una volta
   Attivare SPARK_Mode sui moduli scritti da zero

2. Puntare a Silver
   Gold (dimostrazione funzionale completa) è l'ideale, ma si inizia con
   Silver (nessun errore a runtime)
   Anche solo prevenire l'overflow ha un valore pratico enorme

3. Scrivere i contratti partendo dalle interfacce
   Scrivere i contratti nella specifica del pacchetto (.ads) prima
   dell'implementazione
   Con una specifica solida, chiunque implementi può scrivere codice
   che soddisfa i contratti

4. Integrare in CI/CD
   Aggiungere gnatprove alla pipeline di CI
   Interrompere la build (o almeno avvisare) in caso di fallimento della
   dimostrazione

5. Accumulare report di dimostrazione
   Generare report con gnatprove --report=all
   Monitorare nel tempo l'andamento degli elementi non dimostrati

Per progetti con codice misto C/C++ e Ada, è efficace un approccio graduale:

1. Scrivere i nuovi moduli in Ada/SPARK
2. Interfacciarsi con C/C++ tramite Interfaces.C
3. Migrare a SPARK le strutture dati critiche e la logica di verifica
4. Espandere gradualmente la copertura SPARK

14. Limiti e avvertenze di SPARK

Anche SPARK non è una soluzione universale. Comprendere onestamente i suoi limiti porta a un’applicazione corretta.

Ciò che SPARK può dimostrare:
  SPARK dimostra solo le proprietà scritte nei contratti
  Le proprietà omesse (dimenticate in fase di scrittura) non vengono dimostrate
  Esempio: dimostrare in Post che il risultato è ordinato non garantisce
  che gli elementi originali siano preservati, a meno di scriverlo anche esso

Limiti dei dimostratori:
  Alcune proprietà complesse superano le capacità dei dimostratori automatici
  In quei casi serve la dimostrazione interattiva (ad esempio con Coq)
  Detto ciò, la dimostrazione automatica è sufficiente per la maggior
  parte dei casi pratici

Restrizioni del linguaggio:
  Il codice che fa largo uso di puntatori non può essere convertito in SPARK
  La dimostrazione dell'allocazione dinamica di memoria è limitata
  La dimostrazione di strutture dati ricorsive è difficile

Competenza degli sviluppatori:
  Scrivere contratti richiede pratica
  Progettare invarianti di ciclo è particolarmente lungo da apprendere
  Un piano di crescita delle competenze a livello di team è indispensabile

15. Conclusione ── Rendere la dimostrazione parte dello sviluppo quotidiano

Abbiamo ripercorso la pratica della verifica formale con SPARK.

SPARK è un sottoinsieme di Ada, ristretto alle funzionalità verificabili
I contratti (Pre/Post) sono l'input delle dimostrazioni. I contratti di
Ada 2012 funzionano direttamente
GNATprove esegue dimostrazioni automatiche e riporta i risultati a
livello di codice sorgente
Gli invarianti di ciclo dimostrano le proprietà dei cicli
Global/Depends rendono esplicito il flusso dati e gestiscono gli effetti
collaterali
I livelli di dimostrazione (da Stone a Platinum) permettono di aumentare
il rigore per gradi
Puntare prima al livello Silver (nessun errore a runtime) è la
raccomandazione pratica
Testing e dimostrazione non sono opposti: si completano a vicenda

Si potrebbe avere l’idea preconcetta che «la verifica formale sia troppo difficile e riservata a progetti particolari».

Ma la combinazione odierna di SPARK e GNATprove ha raggiunto il seguente livello:

1. Scrivere un contratto. È fondamentalmente la stessa attività
   progettuale dello scrivere tipi o test
2. Eseguire gnatprove. Dà la sensazione di una compilazione
3. Guardare i risultati e correggere il codice o il contratto

Questo ciclo non è diverso dal flusso di sviluppo quotidiano in cui si corregge il codice leggendo i messaggi di errore del compilatore.

La differenza è questa: mentre un compilatore garantisce che «la sintassi è corretta», GNATprove garantisce «la correttezza per tutti gli input».

Lo slogan di Ada presentato nell’articolo precedente — «i bug non si trovano; i tipi e i contratti li rendono impossibili da scrivere» — con SPARK avanza al livello successivo:

L’assenza di bug è garantita dalla dimostrazione.

Iniziate aggiungendo SPARK_Mode e un Post a una piccola funzione, quindi eseguite gnatprove.

Quando vedrete il messaggio verde postcondition proved, il vostro modo di vedere la garanzia della qualità del software cambierà.

Riferimenti

Articoli correlati

Articoli recenti con gli stessi tag per approfondire argomenti vicini.

Argomenti correlati

Queste pagine collocano l’argomento in un contesto più ampio di servizi e decisioni.

Domande frequenti

Domande che ricorrono nelle consulenze sull’argomento dell’articolo.

Cos'è SPARK e che rapporto ha con Ada?
SPARK è un sottoinsieme di Ada deliberatamente ristretto, progettato affinché le proprietà di un programma possano essere dimostrate matematicamente. Limita funzionalità difficili da verificare — uso libero dei puntatori, gestione illimitata delle eccezioni, strutture dati ricorsive e tasking senza restrizioni — in cambio della dimostrabilità. Il codice SPARK è codice Ada con l'aggiunta di annotazioni contrattuali, quindi rappresenta un'estensione naturale dello sviluppo Ada quotidiano e non un linguaggio diverso; lo strumento GNATprove traduce i contratti nel linguaggio intermedio Why3 e tenta le dimostrazioni con dimostratori automatici come Z3, CVC4 e Alt-Ergo.
In cosa differisce la verifica formale con SPARK dal testing?
Il testing verifica che il programma si comporti correttamente per gli input selezionati; la verifica formale dimostra matematicamente che una proprietà vale per tutti gli input possibili. Le due pratiche sono complementari, non contrapposte: SPARK dimostra solo le proprietà scritte nei contratti, mentre il testing può scoprire assunzioni implicite mai formalizzate e verificare l'interazione con l'ambiente di esecuzione. Una combinazione pratica consiste nel garantire l'assenza di errori a runtime con SPARK, verificare comportamenti concreti di input/output con test unitari e concentrare i test sulle parti che non si riescono a dimostrare.
Quali sono i livelli di dimostrazione di SPARK, e quale conviene puntare per primo?
SPARK definisce cinque livelli di rigore crescente: Stone (sintassi dei contratti e coerenza dei tipi), Bronze (aggiunge la dimostrazione dell'assenza di letture di variabili non inizializzate), Silver (aggiunge la dimostrazione dell'assenza di errori a runtime come overflow, violazioni dei limiti e divisione per zero), Gold (aggiunge la dimostrazione della correttezza funzionale tramite Pre/Post) e Platinum (aggiunge la non interferenza dei dati e il flusso di informazioni). Silver è l'obiettivo iniziale più pragmatico — la maggior parte dei bug reali viene eliminata già eliminando gli errori a runtime — mentre Gold vale la pena perseguirlo per la logica centrale la cui correttezza deve essere garantita.
Cos'è un invariante di ciclo, e perché le dimostrazioni SPARK ne hanno bisogno?
Un invariante di ciclo è una proprietà vera all'inizio di ogni iterazione, scritta con pragma Loop_Invariant. I cicli si eseguono un numero arbitrario di volte, quindi il dimostratore ha bisogno dell'invariante per ragionare su tutte le iterazioni contemporaneamente: esprime come formula il calcolo parziale svolto fino a quel punto, e dopo l'ultima iterazione deve implicare la postcondizione desiderata. Progettare invarianti è l'abilità più delicata nelle dimostrazioni sui cicli: un invariante troppo forte non si riesce a dimostrare, uno troppo debole non implica la postcondizione.

Profilo dell’autore

Pagina di presentazione dell’autore dell’articolo.

Go Komura

Rappresentante di KomuraSoft LLC

Specializzato nello sviluppo di software Windows, nella consulenza tecnica e nell’analisi dei malfunzionamenti, soprattutto nei progetti con sistemi esistenti e guasti difficili da riprodurre.

Contattaci
Torna al blog