From fdbbf102e677fbb0c450eb3255cdc81c2f422ce2 Mon Sep 17 00:00:00 2001
From: Marco Aceti <marco.aceti@studenti.unimi.it>
Date: Tue, 6 Jun 2023 14:53:37 +0200
Subject: [PATCH] Add 'Lezione 12'

---
 ...2022-11-23-testing-e-processi-di-review.md | 492 +-----------------
 src/12_analisi-statica/00_index.md            |  16 +
 src/12_analisi-statica/01_compilatori.md      |  54 ++
 .../02_data-flow/00_index.md                  |  65 +++
 .../02_data-flow/01_regole.md                 | 152 ++++++
 .../02_data-flow/02_sequenze.md               | 124 +++++
 src/12_analisi-statica/03_testing.md          |  23 +
 src/12_analisi-statica/04_criteri/00_index.md |   5 +
 .../04_criteri/01_definizioni.md              |  98 ++++
 src/12_analisi-statica/04_criteri/02_usi.md   | 146 ++++++
 .../04_criteri/03_cammini-du.md               |  14 +
 src/12_analisi-statica/05_oltre-variabili.md  |  69 +++
 src/SUMMARY.md                                |  12 +-
 13 files changed, 785 insertions(+), 485 deletions(-)
 create mode 100644 src/12_analisi-statica/00_index.md
 create mode 100644 src/12_analisi-statica/01_compilatori.md
 create mode 100644 src/12_analisi-statica/02_data-flow/00_index.md
 create mode 100644 src/12_analisi-statica/02_data-flow/01_regole.md
 create mode 100644 src/12_analisi-statica/02_data-flow/02_sequenze.md
 create mode 100644 src/12_analisi-statica/03_testing.md
 create mode 100644 src/12_analisi-statica/04_criteri/00_index.md
 create mode 100644 src/12_analisi-statica/04_criteri/01_definizioni.md
 create mode 100644 src/12_analisi-statica/04_criteri/02_usi.md
 create mode 100644 src/12_analisi-statica/04_criteri/03_cammini-du.md
 create mode 100644 src/12_analisi-statica/05_oltre-variabili.md

diff --git a/_posts/2022-11-23-testing-e-processi-di-review.md b/_posts/2022-11-23-testing-e-processi-di-review.md
index 67e8a8b..8623e3d 100644
--- a/_posts/2022-11-23-testing-e-processi-di-review.md
+++ b/_posts/2022-11-23-testing-e-processi-di-review.md
@@ -5,504 +5,28 @@ date: 2022-11-23 14:40:00 +0200
 toc: true
 ---
 
-# Analisi statica
 
-Come abbiamo detto nella lezione precedente, il testing dell'esecuzione del programma non è però l'unica cosa che possiamo fare per aumentare la fiducia nostra e del cliente nella correttezza del programma.
-Un'altra importante iniziativa in tal senso è l'ispezione tramite varie tecniche del _codice_ del programma, attività che prende il nome di __analisi statica__.
 
-L'analisi statica si basa cioè sull'esame di un __insieme finito di elementi__ (_le istruzioni del programma_), contrariamente all'analisi dinamica che invece considera un insieme infinito (_gli stati delle esecuzioni_).
-È un'attività perciò __meno costosa del testing__, poiché non soffre del problema dell'_"esplosione dello spazio degli stati"_.
-
-Considerando solamente il codice "statico" del programma, questa tecnica non ha la capacità di rilevare anomalie dipendenti da particolari valori assunti dalle variabili a runtime.
-Si tratta nondimeno di un'attività estremamente utile, che può aiutare a individuare numerosi errori e inaccortezze.
-
-## Compilatori
-
-Prima di trasformare il codice sorgente in eseguibile, i compilatori fanno un'attività di analisi statica per identificare errori sintattici (o presunti tali) all'interno del codice.
-
-Il lavoro dei compilatori si può dividere solitamente in __quattro tipi di analisi__ (gli esempi sono presi dal compilatore di Rust, caratteristico per la quantità e qualità di analisi svolta durante la compilazione):
-
-- __analisi lessicale__: identifica i token appartenenti o meno al linguaggio, permettendo di individuare possibili errori di battitura;
-
-  ```txt
-  error: expected one of `!`, `.`, `::`, `;`, `?`, `{`, `}`, or an operator, found `ciao`
-  --> src/main.rs:2:9
-    |
-  2 |     BRO ciao = "mondo";
-    |           ^^^^ expected one of 8 possible tokens
-  ```
-
-- __analisi sintattica__: controlla che i token identificati siano in relazioni _sensate_ tra di loro in base alla grammatica del linguaggio, scovando così possibili errori di incomprensione del linguaggio;
-
-  ```txt
-  error: expected `{`, found keyword `for`
-  --> src/main.rs:2:14
-    |
-  2 |     if !expr for;
-    |              ^^^ expected `{`
-    |
-  ```
-
-- __controllo dei tipi__: nei linguaggi tipizzati, individua violazioni di regole d'uso dei tipi ed eventuali incompatibilità tra tipi di dati;
-
-  ```txt
-  error[E0308]: mismatched types
-  --> src/main.rs:2:24
-    |
-  2 |     let name: String = 42;
-    |               ------   ^^- help: try using a conversion method: `.to_string()`
-    |               |        |
-    |               |        expected struct `String`, found integer
-    |               expected due to this
-
-  For more information about this error, try `rustc --explain E0308`.
-  ```
-
-- __analisi flusso dei dati__: si cercano di rilevare problemi relativi all'_evoluzione dei valori_ associati alle variabili, come per esempio porzioni di codice non raggiungibili.
-
-  ```txt
-  error: equal expressions as operands to `!=`
-  --> src/main.rs:2:8
-    |
-  2 |     if 1 != 1 {
-    |        ^^^^^^
-    |
-  ```
-
-Se i primi tre tipi di analisi sono abbastanza facili da comprendere, l'ultimo merita una maggiore attenzione, motivo per cui gli dedichiamo il prossimo paragrafo.
+#
 
 ## Analisi Data Flow
 
-Nata nell'ambito dell'__ottimizzazione dei compilatori__, che per migliorare le proprie performance ricercavano porzioni di codice non raggiungibile da non compilare, l'__analisi del flusso di dati__ è stata più avanti imbracciata dall'ingegneria del software per ricercare e prevenire le cause di errori simili. \\
-Parlando di flusso dei dati si potrebbe pensare a un'analisi prettamente dinamica come il testing, ma l'insieme dei controlli statici che si possono fare sul codice per comprendere come vengono _utilizzati_ i valori presenti nel programma è invece particolarmente significativo.
-
-È possibile infatti analizzare staticamente il tipo delle operazioni eseguite su una variabile e l'__insieme dei legami di compatibilità__ tra di esse per determinare se il valore in questione viene usato in maniera _semanticamente sensata_ all'interno del codice. \\
-Nello specifico, le operazioni che possono essere eseguite su un __dato__ sono solamente di tre tipi:
-
-<!-- KaTeX op macro definitions -->
-<div style="display: none; margin: 0;">
-$$
-\require{color}
-% Regular operations
-\def\op#1{
-  \fcolorbox{black}{white}{$\vphantom{d} \sf{#1}$}
-}
-\def\d{\op{d} \\,}
-\def\a{\op{a} \\,}
-\def\u{\op{u} \\,}
-% Erroneous operations
-\def\opR#1{
-  \fcolorbox{black}{orangered}{$\vphantom{d} \color{white}{\sf{#1}}$}
-}
-\def\dR{\opR{d} \\,}
-\def\aR{\opR{a} \\,}
-\def\uR{\opR{u} \\,}
-% Subscript operations
-\def\Op#1#2{
-  \fcolorbox{black}{white}{$\vphantom{d_6} \sf{#1}_{#2}$}
-}
-\def\D#1{\Op{d}{#1} \\,}
-\def\A#1{\Op{a}{#1} \\,}
-\def\U#1{\Op{u}{#1} \\,}
-% Warning subscript operations
-\def\OpW#1#2{
-  \fcolorbox{black}{orange}{$\vphantom{d_6} \sf{#1}_{#2}$}
-}
-% Green subscript operations
-\def\OpG#1#2{
-  \fcolorbox{black}{lightgreen}{$\vphantom{d_6} \sf{#1}_{#2}$}
-}
-\def\DG#1{\OpG{d}{#1} \\,}
-\def\AG#1{\OpG{a}{#1} \\,}
-\def\UG#1{\OpG{u}{#1} \\,}
-% Error
-\def\Err{
-  \color{red}{\sf{ERROR}}
-}
-\def\err{
-  \\, \Err
-}
-$$
-</div>
-
-- \\(\op{d}\\) (__definizione__): il comando __assegna un valore__ alla variabile; anche il passaggio del dato come parametro ad una funzione che lo modifica è considerata un'operazione di (ri)definizione;
-
-- \\(\op{u}\\) (__uso__): il comando __legge il contenuto__ di una variabile, come per esempio l'espressione sul lato destro di un assegnamento;
-
-- \\(\op{a}\\) (__annullamento__): al termine dell'esecuzione del comando il valore della variabile __non è significativo/affidabile__.
-  Per esempio, dopo la _dichiarazione senza inizializzazione_ di una variabile e al termine del suo _scope_ il valore è da considerarsi inaffidabile.
-
-Dal punto di vista di ciascuna variabile è possibile ridurre una qualsiasi sequenza d'istruzioni (_ovvero un cammino sul diagramma di flusso_) a una sequenza di definizioni, usi e annullamenti.
-
-### Regole
-
-Fatta questa semplificazione è allora possibile individuare la presenza di anomalie nell'uso delle variabili definendo alcune __regole di flusso__: alcune di queste devono essere necessariamente rispettate in un programma corretto (1 e 3), mentre altre hanno più a che fare con la semantica dell'uso di un valore (2).
-
-<ol>
-
-<li markdown="1">
-  L'**uso di una variabile** deve essere **sempre preceduto** in ogni sequenza **da una definizione senza annullamenti intermedi**.
-
-  $$
-  \a\u\err
-  $$
-
-</li>
-<li markdown="1">
-  La **definizione di una variabile** deve essere **sempre seguita** da **un uso**, **prima** di un suo **annullamento** o nuova **definizione**.
-
-  $$
-  \d\a\err \\
-  \d\d\err
-  $$
-
-</li>
-  <li markdown="1">
-  L'**annullamento di una variabile** deve essere **sempre seguito** da **una definizione**, **prima** di un **uso** o **altro annullamento**.
-  
-  $$
-  \a\a\err
-  $$
-
-</li>
-</ol>
-
-Riassumendo, \\(\a\op{u}\\), \\(\d\op{a}\\), \\(\d\op{d}\\) e \\(\a\op{a}\\) sono sequenze che identificano __situazioni anomale__, anche se non necessariamente dannose: se per esempio usare una variabile subito dopo averla annullata rende l'esecuzione del programma non controllabile, un annullamento subito dopo una definizione non crea nessun problema a runtime, ma è altresì indice di un possibile errore concettuale.
-
-<table align="center" style="width: 50%">
-<tr>
-  <th></th>
-  <th markdown="1">\\(\a\\)</th>
-  <th markdown="1">\\(\d\\)</th>
-  <th markdown="1">\\(\u\\)</th>
-</tr>
-<tr>
-  <th markdown="1">\\(\a\\)</th>
-  <th markdown="1">\\(\Err\\)</th>
-  <th markdown="1"></th>
-  <th markdown="1">\\(\Err\\)</th>
-</tr>
-<tr>
-  <th markdown="1">\\(\d\\)</th>
-  <th markdown="1">\\(\Err\\)</th>
-  <th markdown="1">\\(\Err\\)</th>
-  <th markdown="1"></th>
-</tr>
-<tr>
-  <th markdown="1">\\(\u\\)</th>
-  <th markdown="1"></th>
-  <th markdown="1"></th>
-  <th markdown="1"></th>
-</tr>
-</table>
-
-#### Esempio
-
-Consideriamo la seguente funzione C con il compito di scambiare il valore di due variabili:
-
-```c
-void swap(int &x1, int &x2) {
-    int x1;
-    x3 = x1;
-    x3 = x2;
-    x2 = x1;
-}
-```
-
-Analizzando il codice, le sequenze per ogni variabile sono le seguenti:
-
-| Variabile | Sequenza | Anomalie |
-|-|-|-|
-| `x1` | \\(\aR\uR\u\a\\) | `x1` viene usata 2 volte senza essere stata prima definita |
-| `x2` | \\(\dots \d\u\op{d} \dots\\) | Nessuna |
-| `x3` | \\(\dots \d\dR\opR{d} \dots\\) | `x3` viene definita più volte senza nel frattempo essere stata usata |
-
-Come si vede, in un codice sintatticamente corretto l'analisi Data Flow ci permette quindi di scovare un errore semantico osservando le sequenze di operazioni sulle sue variabili.
-
-### Sequenze Data Flow
-
-Abbiamo accennato più volte al concetto di "sequenza" di operazioni su una variabile.
-Più formalmente, definiamo __sequenza__ di operazioni per la variabile \\(\mathtt{a}\\) secondo il cammino \\(p\\) la concatenazione della tipologia delle istruzioni che coinvolgono tale variabile, e la indichiamo con \\(\operatorname{P}(p, \\, \mathtt{a})\\).
-
-Considerando per esempio il seguente programma C:
-
-```c
-01  void main() {
-02      float a, b, x, y;
-03      read(x);
-04      read(y);
-05      a = x;
-06      b = y;
-07      while (a != b)
-08          if (a > b)
-09              a = a - b;
-10          else
-11              b = b - a;
-12      write(a);
-13  }
-```
-
-possiamo dire che:
-
-$$
-\begin{align*}
-&\operatorname{P}([1, 2, 3, 4, 5, 6, 7, 8, 9, 7, 12, 13], \\, \mathtt{a}) \\
-&= \A{2} \D{5} \U{7} \U{8} \U{9} \D{9} \U{7} \U{12} \A{13}
-\end{align*}
-$$
-
-Eseguendo questo tipo di operazione su tutte le variabili e per tutti i cammini del programma si potrebbe verificare la presenza eventuali anomalie, ma come sappiamo __i cammini sono potenzialmente infiniti__ quando il programma contiene cicli e decisioni: per scoprire quali percorsi segue effettivamente l'esecuzione del programma dovremmo eseguirlo e quindi uscire dal campo dell'analisi statica.
-
-#### Espressioni regolari
-
-Tuttavia non tutto è perduto: un caso di cammini contenenti __cicli__ e __decisioni__ è possibile rappresentare un insieme di sequenze ottenute dal programma \\(P\\) utilizzando delle __espressioni regolari__.
-Con \\(\operatorname{P}([1 \rightarrow], \\, \mathtt{a})\\) si indica infatti l'espressione regolare che rappresenta __tutti i cammini__ che partono dall'istruzione \\(1\\) per la variabile \\(\mathtt{a}\\).
-
-Questo perché nelle espressioni regolari è possibile inserire, oltre che una serie di parentesi che isolano sotto-sequenze, anche due simboli molto particolari:
-
-- la __pipe__ (\|), che indica che i simboli (o le sotto-sequenze) alla propria destra e alla propria sinistra si _escludono_ a vicenda: _una e una sola_ delle due è presente;
-- l'__asterisco__ (\*), che indica che il simbolo (o la sotto-sequenza) precedente può essere _ripetuto da 0 a \\(n\\) volte_.
-
-Grazie a questi simboli è possibile rappresentare rispettivamente decisioni e cicli.
-Prendendo per esempio il codice precedente, è possibile costruire \\(\operatorname{P}([1 \rightarrow], \\, \mathtt{a})\\) come:
-
-$$
-\begin{align*}
-&\A{2} \D{5} & & &&&  && && & & \\
-&\A{2} \D{5} &\U{7} &\Big( &\phantom{\U8} &&\textit{while body} &&\phantom{\U{7}} &&\Big)* &\quad \quad \U{12} &\A{13} \\
-&\A{2} \D{5} &\U{7} &\Big( &\U{8} &&\textit{if body} &&\phantom{\U{7}} &&\Big)* &\quad \quad \U{12} &\A{13} \\
-&\A{2} \D{5} &\U{7} &\Big( &\U{8} &&\Big(\, \U{9} \D{9} \Big | \: \U{11} \Big) && &&\Big)* &\quad \quad \U{12} &\A{13} \\
-&\A{2} \D{5} &\OpW{u}{7} \\, &\Big( \\, &\U{8} &&\Big(\, \U{9} \D{9} \Big | \: \U{11} \Big)
-  &&\OpW{u}{7} \\,
-&&\Big)* &\quad \quad \U{12} &\A{13}
-\end{align*}
-$$
-
-Osserviamo come \\(\OpW{u}{7}\\) si ripeta due volte: questo può rendere _fastidioso_ ricercare errori, per via della difficoltà di considerare cammini multipli.
-Comunque sia, una volta ottenuta un'espressione regolare è facile verificare l'eventuale presenza di errori applicando le solite regole (nell'esempio non ce n'erano).
-
-Bisogna però fare attenzione a un'aspetto: le espressioni regolari così costruite rappresentano __tutti i cammini__ possibili del programma, ma __non tutti e i soli__!
-Trattandosi di oggetti puramente matematici, infatti, le espressioni regolari sono necessariamente _più generali_ di qualunque programma: esse non tengono infatti conto degli _effetti_ che le istruzioni hanno sui dati e delle relative proprietà che si possono inferire. \\
-Riprendendo a esempio l'espressione regolare di cui sopra, essa contiene la sequenza nella quale il ciclo viene eseguito _infinite volte_, ma osservando il programma è facile indovinare che tale comportamento non sia in realtà possibile: diminuendo progressivamente \\(\mathtt{a}\\) e \\(\mathtt{b}\\) a seconda di chi sia il maggiore si può dimostrare che prima o poi i due convergeranno allo stesso valore permettendo così di uscire dal ciclo.
-
-In effetti, uno stesso programma può essere rappresentato tramite __un numero infinito di espressioni regolari__ valide.
-Si potrebbe addirittura argomentare che l'espressione regolare
-
-$$
-\Big ( \\, \u \Big | \: \d \Big | \: \a \Big)*
-$$
-
-possa rappresentare qualsiasi programma. \\
-Allontanandosi però dai casi estremi, si dimostra essere impossibile scrivere un algoritmo che dato un qualsiasi programma riesca a generare un'espressione regolare che rappresenti __tutti e soli__ i suoi cammini possibili senza osservare i valori delle variabili.
-Bisogna dunque accontentarsi di trovare espressioni regolari che rappresentino __al meglio__ l'esecuzione del programma, ovvero con il minor numero di cammini impossibili rappresentati.
-
-Nell'analisi Data Flow tramite espressioni regolari è quindi necessario tenere conto che il modello generato è un'__astrazione pessimistica__: se viene notificata la presenza di un errore non si può essere certi che esso ci sia veramente, in quanto esso potrebbe derivare da un cammino non percorribile.
-
-## Analisi statica e Testing
-
-Oltre ad essere un processo utile di per sé per il rilevamento di potenziali errori, l'__analisi statica__ può anche contribuire a guidare l'attività di __testing__. \\
-Per capire come, osserviamo che a partire dall'analisi statica è possibile fare le seguenti osservazioni:
-
-- perché si presenti un malfunzionamento dovuto a una anomalia in una _definizione_, deve esserci un _uso_ che si serva del valore assegnato;
-- un ciclo dovrebbe essere ripetuto (di nuovo) se verrà _usato_ un valore _definito_ alla iterazione precedente.
-
-L'analisi statica può quindi aiutare a __selezionare i casi di test__ basandosi sulle _sequenze definizione-uso_ delle variabili, costruendo cioè dei nuovi criteri di copertura.
-
-### Terminologia
-
-Per rendere più scorrevole la spiegazione dei prossimi argomenti introduciamo innanzitutto un po' di terminologia.
 
-Dato un nodo \\(i\\) del diagramma di flusso (_un comando/riga del programma_), chiamiamo \\(\operatorname{def}(i)\\) l'__insieme delle variabili definite in__ \\(\bf{i}\\).
+##
 
-Data invece una variabile \\(x\\) e un nodo \\(i\\), chiamiamo \\(\operatorname{du}(x, \\, i)\\) l'insieme dei nodi \\(j\\) tali che:
+##
 
-- \\(x \in \operatorname{def}(i)\\), ovvero la variabile \\(x\\) è __definita__ in \\(i\\);
-- \\(x\\) è __usata__ nel nodo \\(j\\);
-- __esiste un cammino__ da \\(i\\) a \\(j\\) __libero da definizioni__ di \\(x\\), ovvero che se seguito non sovrascrive il valore di \\(x\\).
-
-Si tratta cioè dell'__insieme di nodi \\(\bf{j}\\) che _potrebbero_ usare il valore di \\(\bf{x}\\) definito in \\(\bf{i}\\)__.
+#
 
 ### Criteri di copertura derivati dall'analisi statica
 
-#### Criterio di copertura delle definizioni
-
-_Un test \\(\ T\\) soddisfa il __criterio di copertura delle definizioni__ se e solo se per ogni nodo \\(i\\) e ogni variabile \\(x \in \operatorname{def}(i)\\), \\(T\\) include un caso di test che esegue un cammino libero da definizioni da \\(i\\) ad __almeno uno__ degli elementi di \\(\operatorname{du}(i, x).\\)_
-
-Ci si vuole cioè assicurare di testare tutte le definizioni, assicurandosi che funzionino osservando almeno un uso del valore da loro assegnato.
-Matematicamente si può dire che:
-
-$$
-\begin{align*}
-T \in C_{def} \Longleftrightarrow& \forall i \in P, \  \forall x \in \operatorname{def}(i), \ \exists j \in \operatorname{du}(i, \\, x) \:, \\
-& \: \exists t \in T \ \text{che esegue un cammino da $i$ a $j$ senza ulteriori definizioni di $x$}.
-\end{align*}
-$$
-
-Riconsideriamo l'esempio già visto in precedenza, considerando la variabile \\(\mathtt{a}\\):
-
-```c
-01  void main() {
-02      float a, b, x, y;
-03      read(x);
-04      read(y);
-05      a = x;
-06      b = y;
-07      while (a != b)
-08          if (a > b)
-09              a = a - b;
-10          else
-11              b = b - a;
-12      write(a);
-13  }
-```
-
-Partiamo definendo gli insiemi dei nodi degli usi \\(\operatorname{du}(i, \\, \mathtt a)\\):
-
-1. \\(\operatorname{du}(5, \\, \mathtt a)\\) = \\(\{7, \\, 8, \\, 9, \\, 11, \\, 12\}\\);
-2. \\(\operatorname{du}(9, \\, \mathtt a)\\) = \\(\{7, \\, 8, \\, 9, \\, 11, \\, 12\}\\).
-
-È solo __un caso__ il fatto che in questo esempio tali insiemi siano uguali. \\
-Comunque sia, l'obiettivo è _per ognuna delle due definizioni_ ottenere un __uso__ di tale definizione:
-
-1. Per la prima definizione la soluzione è banale, a riga 7 la variabile \\(\mathtt a\\) viene letta sempre:
-\\(\D{5}\U{7}\\).
-2. Per la seconda, invece, è necessario scegliere un valore tale per cui il flusso di esecuzione entri almeno una volta nel ciclo ed esegua almeno una volta la riga 9:
-\\(\D{9}\U{7}\\).
-
-Un test che soddisfa totalmente il criterio può essere il seguente:
-
-$$
-T = \{ \langle 8, \\, 4 \rangle \}.
-$$
-
-Come si vede, il criterio di copertura delle definizioni non copre tutti i comandi e di conseguenza __non implica il criterio di copertura dei comandi__.
-
-#### Criterio di copertura degli usi
-
-_Un test \\(\ T\\) soddisfa il __criterio di copertura degli usi__ se e solo se per ogni nodo \\(i\\) e ogni variabile \\(x\\) appartenente a \\(\operatorname{def}(i)\\), \\(T\\) include un caso di test che esegue un cammino libero da definizioni da \\(i\\) ad __ogni elemento__ di \\(\operatorname{du}(i, \\, x).\\)_
-
-Sembra simile al precedente, con la differenza che ora bisogna coprire __tutti__ i potenziali usi di una variabile definita.
-Questo appare ancora più chiaro osservando la formula matematica:
-
-$$
-\begin{align*}
-T \in C_{path} \Longleftrightarrow& \forall i \in P, \  \forall x \in \operatorname{def}(i), \ \forall j \in \operatorname{du}(i, \\, x) \:, \\
-& \: \exists t \in T \ \text{che esegue un cammino da $i$ a $j$ senza ulteriori definizioni di $x$}.
-\end{align*}
-$$
-
-Si noti però che il criterio di copertura degli usi __non implica il criterio di copertura delle definizioni__, perché nel caso in cui non esistano \\(j \in \operatorname{du}(i, \\, x)\\) l'uso del \\(\forall\\) è più _"permissivo"_ del \\(\exists\\) del criterio precedente: quest'ultimo richiedeva infatti che per ogni definizione esistesse almeno un uso, mentre il criterio di copertura degli usi non pone tale clausola (_se non ci sono usi il \\(\forall\\) è sempre vero_).
-Viene quindi da sé che questo criterio non copre neanche il criterio di copertura dei comandi.
-
-Riconsideriamo nuovamente il programma in C visto in precedenza come esempio:
-
-```c
-01  void main() {
-02      float a, b, x, y;
-03      read(x);
-04      read(y);
-05      a = x;
-06      b = y;
-07      while (a != b)
-08          if (a > b)
-09              a = a - b;
-10          else
-11              b = b - a;
-12      write(a);
-13  }
-```
-
-Come prima, consideriamo la variabile \\(\mathtt a\\) e i relativi insieme dei nodi degli usi per ogni sua definizione:
-
-1. \\(\operatorname{du}(5, \\, \mathtt a)\\) = \\(\{7, \\, 8, \\, 9, \\, 11, \\, 12\}\\);
-2. \\(\operatorname{du}(9, \\, \mathtt a)\\) = \\(\{7, \\, 8, \\, 9, \\, 11, \\, 12\}\\).
-
-Per ogni definizione occorre coprire __tutti gli usi__:
-
-<style>
-  #criterio-usi-tabella {
-    text-align: center;
-  }
-  #criterio-usi-tabella p {
-    margin-bottom: 0;
-  }
-</style>
-
-<table id="criterio-usi-tabella" style="text-align: center;">
-<tr>
-  <th style="width: 50%" markdown="1">
-    \\(\operatorname{du}(5, \\, \mathtt a)\\)
-  </th>
-  <th markdown="1">\\(\operatorname{du}(9, \\, \mathtt a)\\)</th>
-</tr>
-<tr>
-  <td markdown="1">\\(\D{5}\UG{7}\UG{8}\UG{11}\U{7}\UG{12}\\)
-  </td>
-  <td markdown="1">\\(\dots \\, \D{9} \UG7 \UG8 \UG9 \dots\\)
-  </td>
-</tr>
-<tr>
-  <td markdown="1">\\(\dots \\, \D5 \U7 \U8 \UG9 \dots\\)
-  </td>
-  <td markdown="1">\\(\dots \\, \D9 \U7 \U8 \UG{12} \dots\\)
-  </td>
-</tr>
-<tr>
-  <td></td>
-  <td markdown="1">\\(\dots \\, \D9 \U7 \U8 \UG{11} \dots\\)
-  </td>
-</tr>
-</table>
-
-Un test che soddisfa totalmente il criterio può essere il seguente:
-
-$$
-T = \{ \langle 4, \\,  8 \rangle, \\, \langle 12, \\, 8 \rangle, \\, \langle 12, \\, 4 \rangle \}.
-$$
-
-Questo esempio permette di notare qualcosa sulla natura dei cicli: dovendo testare ogni percorso al loro interno è necessario fare almeno due iterazioni.
-Può quindi sorgere un dubbio: è meglio che le due iterazioni siano fatte nello stesso caso di test o in casi test separati? Ovvero, è meglio __minimizzare__ i __casi di test__ o le __iterazioni per caso__? \\
-Opinione diffusa è quella secondo cui è preferibile __minimizzare le iterazioni__: partizionando le casistiche in diversi casi di test è possibile rilevare con più precisione gli errori, riducendo il tempo di debug.
-In alcune situazioni però aumentare il numero di iterazioni può diminuire il tempo di esecuzione totale dei test, in quanto dovendo riavviare il programma per ciascun caso di test la somma dei tempi di startup può diventare significativa per software molto massicci.
-
-#### Criterio di copertura dei cammini DU
-
-Nel criterio precedente si richiedeva di testare _un_ cammino da ogni definizione ad ogni suo uso, ma come sappiamo i cammini tra due istruzioni di un programma possono essere molteplici.
-Potrebbe dunque sorgere l'idea di testarli _tutti_: da questa intuizione nasce il __criterio di copertura dei cammini DU__.
-
-$$
-\begin{align*}
-T \in C_{pathDU} \Longleftrightarrow& \forall i \in P, \  \forall x \in \operatorname{def}(i), \ \forall j \in \operatorname{du}(i, \\, x), \\
-&\forall \text{ cammino da $i$ a $j$ senza ulteriori definizioni di $x$} \\
-& \exists t \in T \ \text{che lo esegue}.
-\end{align*}
-$$
-
-Questo criterio può essere __utile da ipotizzare__, ma a causa dell'esplosione combinatoria del numero dei cammini è considerato __impraticabile__ (_"sopra la barra rossa"_).
-
-### Oltre le variabili
-
-L'analisi del flusso dati si può estendere anche su altri _"oggetti"_, non solo variabili. \\
-Per esempio, è possibile prevedere le seguenti operazioni su un __file__:
-
-- \\(\op{a}\\) (__apertura__): specializzata in _per lettura_ o _per scrittura_;
-- \\(\op{c}\\) (__chiusura__);
-- \\(\op{l}\\) (__lettura__);
-- \\(\op{s}\\) (__scrittura__).
-
-Date queste operazioni si possono individuare una serie di regole, come per esempio:
-
-1. \\(\op{l}\\), \\(\op{s}\\) e \\(\op{c}\\) devono essere precedute da \\(\op{a}\\) senza \\(\op{c}\\) intermedie;
-2. \\(\op{a}\\) deve essere seguita da \\(\op{c}\\) prima di un'altra \\(\op{a}\\);
-3. legami tra tipo di apertura (per lettura o per scrittura) e relative operazioni.
+###
 
-È interessante notare il __legame__ tra l'attività di analisi del flusso di dati e i diagrammi UML a stati finiti: un _oggetto_ risponde a una certa _tipologia di eventi_, può essere in diversi _stati_ e in certi _stati_ non sono ammesse alcune _operazioni_.
-Si noti come nessuna delle due discipline entra comunque nel merito del valore delle variabili, relegato ad un'analisi a runtime.
+###
 
-#### Criterio di _copertura del budget_
+###
 
-Molto spesso nei contesti reali l'unico criterio applicato è quello di __copertura del budget__: si continuano a creare casi di test finché non sono finite le risorse (tempo e soldi).
-Questa tecnica ovviamente non fornisce alcuna garanzia sull'efficacia dei test, ed è sicuramente sconsigliata.
+##
 
 # Tecniche di review
 
diff --git a/src/12_analisi-statica/00_index.md b/src/12_analisi-statica/00_index.md
new file mode 100644
index 0000000..99e7a07
--- /dev/null
+++ b/src/12_analisi-statica/00_index.md
@@ -0,0 +1,16 @@
+# Analisi statica
+
+Come abbiamo detto nella lezione precedente, il testing dell'esecuzione del programma non è però l'unica cosa che possiamo fare per aumentare la fiducia nostra e del cliente nella correttezza del programma.
+Un'altra importante iniziativa in tal senso è l'ispezione tramite varie tecniche del _codice_ del programma, attività che prende il nome di __analisi statica__.
+
+L'analisi statica si basa cioè sull'esame di un __insieme finito di elementi__ (_le istruzioni del programma_), contrariamente all'analisi dinamica che invece considera un insieme infinito (_gli stati delle esecuzioni_).
+È un'attività perciò __meno costosa del testing__, poiché non soffre del problema dell'_"esplosione dello spazio degli stati"_.
+
+Considerando solamente il codice "statico" del programma, questa tecnica non ha la capacità di rilevare anomalie dipendenti da particolari valori assunti dalle variabili a runtime.
+Si tratta nondimeno di un'attività estremamente utile, che può aiutare a individuare numerosi errori e inaccortezze.
+
+- [**Compilatori**](./01_compilatori.md)
+- [**Analisi Data Flow**](./02_data-flow/00_index.md)
+- [**Testing**](./03_testing.md)
+- [**Criteri di copertura**](./04_criteri/00_index.md)
+- [**Oltre le variabili**](./05_oltre-variabili.md)
diff --git a/src/12_analisi-statica/01_compilatori.md b/src/12_analisi-statica/01_compilatori.md
new file mode 100644
index 0000000..a7feaa3
--- /dev/null
+++ b/src/12_analisi-statica/01_compilatori.md
@@ -0,0 +1,54 @@
+# Compilatori
+
+Prima di trasformare il codice sorgente in eseguibile, i compilatori fanno un'attività di analisi statica per identificare errori sintattici (o presunti tali) all'interno del codice.
+
+Il lavoro dei compilatori si può dividere solitamente in __quattro tipi di analisi__ (gli esempi sono presi dal compilatore di Rust, caratteristico per la quantità e qualità di analisi svolta durante la compilazione):
+
+- __analisi lessicale__: identifica i token appartenenti o meno al linguaggio, permettendo di individuare possibili errori di battitura;
+
+  ```txt
+  error: expected one of `!`, `.`, `::`, `;`, `?`, `{`, `}`, or an operator, found `ciao`
+  --> src/main.rs:2:9
+    |
+  2 |     BRO ciao = "mondo";
+    |           ^^^^ expected one of 8 possible tokens
+  ```
+
+- __analisi sintattica__: controlla che i token identificati siano in relazioni _sensate_ tra di loro in base alla grammatica del linguaggio, scovando così possibili errori di incomprensione del linguaggio;
+
+  ```txt
+  error: expected `{`, found keyword `for`
+  --> src/main.rs:2:14
+    |
+  2 |     if !expr for;
+    |              ^^^ expected `{`
+    |
+  ```
+
+- __controllo dei tipi__: nei linguaggi tipizzati, individua violazioni di regole d'uso dei tipi ed eventuali incompatibilità tra tipi di dati;
+
+  ```txt
+  error[E0308]: mismatched types
+  --> src/main.rs:2:24
+    |
+  2 |     let name: String = 42;
+    |               ------   ^^- help: try using a conversion method: `.to_string()`
+    |               |        |
+    |               |        expected struct `String`, found integer
+    |               expected due to this
+
+  For more information about this error, try `rustc --explain E0308`.
+  ```
+
+- __analisi flusso dei dati__: si cercano di rilevare problemi relativi all'_evoluzione dei valori_ associati alle variabili, come per esempio porzioni di codice non raggiungibili.
+
+  ```txt
+  error: equal expressions as operands to `!=`
+  --> src/main.rs:2:8
+    |
+  2 |     if 1 != 1 {
+    |        ^^^^^^
+    |
+  ```
+
+Se i primi tre tipi di analisi sono abbastanza facili da comprendere, l'ultimo merita una maggiore attenzione, motivo per cui gli dedichiamo il prossimo paragrafo.
diff --git a/src/12_analisi-statica/02_data-flow/00_index.md b/src/12_analisi-statica/02_data-flow/00_index.md
new file mode 100644
index 0000000..ebfe5aa
--- /dev/null
+++ b/src/12_analisi-statica/02_data-flow/00_index.md
@@ -0,0 +1,65 @@
+<!-- KaTeX op macro definitions -->
+<div style="display: none; margin: 0;">
+$$
+\require{color}
+% Regular operations
+\def\op#1{
+  \fcolorbox{black}{white}{$\vphantom{d} \sf{#1}$}
+}
+\def\d{\op{d} \\,}
+\def\a{\op{a} \\,}
+\def\u{\op{u} \\,}
+% Erroneous operations
+\def\opR#1{
+  \fcolorbox{black}{orangered}{$\vphantom{d} \color{white}{\sf{#1}}$}
+}
+\def\dR{\opR{d} \\,}
+\def\aR{\opR{a} \\,}
+\def\uR{\opR{u} \\,}
+% Subscript operations
+\def\Op#1#2{
+  \fcolorbox{black}{white}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+\def\D#1{\Op{d}{#1} \\,}
+\def\A#1{\Op{a}{#1} \\,}
+\def\U#1{\Op{u}{#1} \\,}
+% Warning subscript operations
+\def\OpW#1#2{
+  \fcolorbox{black}{orange}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+% Green subscript operations
+\def\OpG#1#2{
+  \fcolorbox{black}{lightgreen}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+\def\DG#1{\OpG{d}{#1} \\,}
+\def\AG#1{\OpG{a}{#1} \\,}
+\def\UG#1{\OpG{u}{#1} \\,}
+% Error
+\def\Err{
+  \color{red}{\sf{ERROR}}
+}
+\def\err{
+  \\, \Err
+}
+$$
+</div>
+
+# Analisi Data Flow
+
+Nata nell'ambito dell'__ottimizzazione dei compilatori__, che per migliorare le proprie performance ricercavano porzioni di codice non raggiungibile da non compilare, l'__analisi del flusso di dati__ è stata più avanti imbracciata dall'ingegneria del software per ricercare e prevenire le cause di errori simili. \
+Parlando di flusso dei dati si potrebbe pensare a un'analisi prettamente dinamica come il testing, ma l'insieme dei controlli statici che si possono fare sul codice per comprendere come vengono _utilizzati_ i valori presenti nel programma è invece particolarmente significativo.
+
+È possibile infatti analizzare staticamente il tipo delle operazioni eseguite su una variabile e l'__insieme dei legami di compatibilità__ tra di esse per determinare se il valore in questione viene usato in maniera _semanticamente sensata_ all'interno del codice. \
+Nello specifico, le operazioni che possono essere eseguite su un __dato__ sono solamente di tre tipi:
+
+- \\(\op{d}\\) (__definizione__): il comando __assegna un valore__ alla variabile; anche il passaggio del dato come parametro ad una funzione che lo modifica è considerata un'operazione di (ri)definizione;
+
+- \\(\op{u}\\) (__uso__): il comando __legge il contenuto__ di una variabile, come per esempio l'espressione sul lato destro di un assegnamento;
+
+- \\(\op{a}\\) (__annullamento__): al termine dell'esecuzione del comando il valore della variabile __non è significativo/affidabile__.
+  Per esempio, dopo la _dichiarazione senza inizializzazione_ di una variabile e al termine del suo _scope_ il valore è da considerarsi inaffidabile.
+
+Dal punto di vista di ciascuna variabile è possibile ridurre una qualsiasi sequenza d'istruzioni (_ovvero un cammino sul diagramma di flusso_) a una sequenza di definizioni, usi e annullamenti.
+
+- [**Regole**](./01_regole.md)
+- [**Sequenze**](02_sequenze.md)
diff --git a/src/12_analisi-statica/02_data-flow/01_regole.md b/src/12_analisi-statica/02_data-flow/01_regole.md
new file mode 100644
index 0000000..3f41937
--- /dev/null
+++ b/src/12_analisi-statica/02_data-flow/01_regole.md
@@ -0,0 +1,152 @@
+<!-- KaTeX op macro definitions -->
+<div style="display: none; margin: 0;">
+$$
+\require{color}
+% Regular operations
+\def\op#1{
+  \fcolorbox{black}{white}{$\vphantom{d} \sf{#1}$}
+}
+\def\d{\op{d} \,}
+\def\a{\op{a} \,}
+\def\u{\op{u} \,}
+% Erroneous operations
+\def\opR#1{
+  \fcolorbox{black}{orangered}{$\vphantom{d} \color{white}{\sf{#1}}$}
+}
+\def\dR{\opR{d} \,}
+\def\aR{\opR{a} \,}
+\def\uR{\opR{u} \,}
+% Subscript operations
+\def\Op#1#2{
+  \fcolorbox{black}{white}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+\def\D#1{\Op{d}{#1} \,}
+\def\A#1{\Op{a}{#1} \,}
+\def\U#1{\Op{u}{#1} \,}
+% Warning subscript operations
+\def\OpW#1#2{
+  \fcolorbox{black}{orange}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+% Green subscript operations
+\def\OpG#1#2{
+  \fcolorbox{black}{lightgreen}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+\def\DG#1{\OpG{d}{#1} \,}
+\def\AG#1{\OpG{a}{#1} \,}
+\def\UG#1{\OpG{u}{#1} \,}
+% Error
+\def\Err{
+  \color{red}{\sf{ERROR}}
+}
+\def\err{
+  \, \Err
+}
+$$
+</div>
+
+# Regole
+
+Fatta questa semplificazione è allora possibile individuare la presenza di anomalie nell'uso delle variabili definendo alcune __regole di flusso__: alcune di queste devono essere necessariamente rispettate in un programma corretto (1 e 3), mentre altre hanno più a che fare con la semantica dell'uso di un valore (2).
+
+<ol>
+
+<li>
+
+  L'**uso di una variabile** deve essere **sempre preceduto** in ogni sequenza **da una definizione senza annullamenti intermedi**.
+
+  $$
+  \a\u\err
+  $$
+</li>
+<li>
+
+  La **definizione di una variabile** deve essere **sempre seguita** da **un uso**, **prima** di un suo **annullamento** o nuova **definizione**.
+
+  $$
+  \d\a\err \\\\
+  \d\d\err
+  $$
+
+</li>
+  <li>
+
+  L'**annullamento di una variabile** deve essere **sempre seguito** da **una definizione**, **prima** di un **uso** o **altro annullamento**.
+  
+  $$
+  \a\a\err
+  $$
+
+</li>
+</ol>
+
+Riassumendo, \\(\a\op{u}\\), \\(\d\op{a}\\), \\(\d\op{d}\\) e \\(\a\op{a}\\) sono sequenze che identificano __situazioni anomale__, anche se non necessariamente dannose: se per esempio usare una variabile subito dopo averla annullata rende l'esecuzione del programma non controllabile, un annullamento subito dopo una definizione non crea nessun problema a runtime, ma è altresì indice di un possibile errore concettuale.
+
+<table align="center" style="width: 50%">
+<tr>
+  <th></th>
+  <th>
+  
+  \\(\a\\)</th>
+  <th>
+  
+  \\(\d\\)</th>
+  <th>
+  
+  \\(\u\\)</th>
+</tr>
+<tr>
+  <th>
+  
+  \\(\a\\)</th>
+  <th>
+  
+  \\(\Err\\)</th>
+  <th></th>
+  <th>
+  
+  \\(\Err\\)</th>
+</tr>
+<tr>
+  <th>
+  
+  \\(\d\\)</th>
+  <th>
+  
+  \\(\Err\\)</th>
+  <th>
+  
+  \\(\Err\\)</th>
+  <th></th>
+</tr>
+<tr>
+  <th>
+  
+  \\(\u\\)</th>
+  <th></th>
+  <th></th>
+  <th></th>
+</tr>
+</table>
+
+#### Esempio
+
+Consideriamo la seguente funzione C con il compito di scambiare il valore di due variabili:
+
+```c
+void swap(int &x1, int &x2) {
+    int x1;
+    x3 = x1;
+    x3 = x2;
+    x2 = x1;
+}
+```
+
+Analizzando il codice, le sequenze per ogni variabile sono le seguenti:
+
+| Variabile | Sequenza | Anomalie |
+|-|-|-|
+| `x1` | \\(\aR\uR\u\a\\) | `x1` viene usata 2 volte senza essere stata prima definita |
+| `x2` | \\(\dots \d\u\op{d} \dots\\) | Nessuna |
+| `x3` | \\(\dots \d\dR\opR{d} \dots\\) | `x3` viene definita più volte senza nel frattempo essere stata usata |
+
+Come si vede, in un codice sintatticamente corretto l'analisi Data Flow ci permette quindi di scovare un errore semantico osservando le sequenze di operazioni sulle sue variabili.
diff --git a/src/12_analisi-statica/02_data-flow/02_sequenze.md b/src/12_analisi-statica/02_data-flow/02_sequenze.md
new file mode 100644
index 0000000..2a73ffe
--- /dev/null
+++ b/src/12_analisi-statica/02_data-flow/02_sequenze.md
@@ -0,0 +1,124 @@
+<!-- KaTeX op macro definitions -->
+<div style="display: none; margin: 0;">
+$$
+\require{color}
+% Regular operations
+\def\op#1{
+  \fcolorbox{black}{white}{$\vphantom{d} \sf{#1}$}
+}
+\def\d{\op{d} \,}
+\def\a{\op{a} \,}
+\def\u{\op{u} \,}
+% Erroneous operations
+\def\opR#1{
+  \fcolorbox{black}{orangered}{$\vphantom{d} \color{white}{\sf{#1}}$}
+}
+\def\dR{\opR{d} \,}
+\def\aR{\opR{a} \,}
+\def\uR{\opR{u} \,}
+% Subscript operations
+\def\Op#1#2{
+  \fcolorbox{black}{white}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+\def\D#1{\Op{d}{#1} \,}
+\def\A#1{\Op{a}{#1} \,}
+\def\U#1{\Op{u}{#1} \,}
+% Warning subscript operations
+\def\OpW#1#2{
+  \fcolorbox{black}{orange}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+% Green subscript operations
+\def\OpG#1#2{
+  \fcolorbox{black}{lightgreen}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+\def\DG#1{\OpG{d}{#1} \,}
+\def\AG#1{\OpG{a}{#1} \,}
+\def\UG#1{\OpG{u}{#1} \,}
+% Error
+\def\Err{
+  \color{red}{\sf{ERROR}}
+}
+\def\err{
+  \, \Err
+}
+$$
+</div>
+
+# Sequenze
+
+Abbiamo accennato più volte al concetto di "sequenza" di operazioni su una variabile.
+Più formalmente, definiamo __sequenza__ di operazioni per la variabile \\(\mathtt{a}\\) secondo il cammino \\(p\\) la concatenazione della tipologia delle istruzioni che coinvolgono tale variabile, e la indichiamo con \\(\operatorname{P}(p, \\, \mathtt{a})\\).
+
+Considerando per esempio il seguente programma C:
+
+```c
+01  void main() {
+02      float a, b, x, y;
+03      read(x);
+04      read(y);
+05      a = x;
+06      b = y;
+07      while (a != b)
+08          if (a > b)
+09              a = a - b;
+10          else
+11              b = b - a;
+12      write(a);
+13  }
+```
+
+possiamo dire che:
+
+$$
+\begin{align*}
+&\operatorname{P}([1, 2, 3, 4, 5, 6, 7, 8, 9, 7, 12, 13], \\, \mathtt{a}) \\\\
+&= \A{2} \D{5} \U{7} \U{8} \U{9} \D{9} \U{7} \U{12} \A{13}
+\end{align*}
+$$
+
+Eseguendo questo tipo di operazione su tutte le variabili e per tutti i cammini del programma si potrebbe verificare la presenza eventuali anomalie, ma come sappiamo __i cammini sono potenzialmente infiniti__ quando il programma contiene cicli e decisioni: per scoprire quali percorsi segue effettivamente l'esecuzione del programma dovremmo eseguirlo e quindi uscire dal campo dell'analisi statica.
+
+#### Espressioni regolari
+
+Tuttavia non tutto è perduto: un caso di cammini contenenti __cicli__ e __decisioni__ è possibile rappresentare un insieme di sequenze ottenute dal programma \\(P\\) utilizzando delle __espressioni regolari__.
+Con \\(\operatorname{P}([1 \rightarrow], \\, \mathtt{a})\\) si indica infatti l'espressione regolare che rappresenta __tutti i cammini__ che partono dall'istruzione \\(1\\) per la variabile \\(\mathtt{a}\\).
+
+Questo perché nelle espressioni regolari è possibile inserire, oltre che una serie di parentesi che isolano sotto-sequenze, anche due simboli molto particolari:
+
+- la __pipe__ (\|), che indica che i simboli (o le sotto-sequenze) alla propria destra e alla propria sinistra si _escludono_ a vicenda: _una e una sola_ delle due è presente;
+- l'__asterisco__ (\*), che indica che il simbolo (o la sotto-sequenza) precedente può essere _ripetuto da 0 a \\(n\\) volte_.
+
+Grazie a questi simboli è possibile rappresentare rispettivamente decisioni e cicli.
+Prendendo per esempio il codice precedente, è possibile costruire \\(\operatorname{P}([1 \rightarrow], \\, \mathtt{a})\\) come:
+
+$$
+\begin{align*}
+&\A{2} \D{5} & & &&&  && && & & \\\\
+&\A{2} \D{5} &\U{7} &\Big( &\phantom{\U8} &&\textit{while body} &&\phantom{\U{7}} &&\Big)* &\quad \quad \U{12} &\A{13} \\\\
+&\A{2} \D{5} &\U{7} &\Big( &\U{8} &&\textit{if body} &&\phantom{\U{7}} &&\Big)* &\quad \quad \U{12} &\A{13} \\\\
+&\A{2} \D{5} &\U{7} &\Big( &\U{8} &&\Big(\, \U{9} \D{9} \Big | \: \U{11} \Big) && &&\Big)* &\quad \quad \U{12} &\A{13} \\\\
+&\A{2} \D{5} &\OpW{u}{7} \\, &\Big( \\, &\U{8} &&\Big(\, \U{9} \D{9} \Big | \: \U{11} \Big)
+  &&\OpW{u}{7} \\,
+&&\Big)* &\quad \quad \U{12} &\A{13}
+\end{align*}
+$$
+
+Osserviamo come \\(\OpW{u}{7}\\) si ripeta due volte: questo può rendere _fastidioso_ ricercare errori, per via della difficoltà di considerare cammini multipli.
+Comunque sia, una volta ottenuta un'espressione regolare è facile verificare l'eventuale presenza di errori applicando le solite regole (nell'esempio non ce n'erano).
+
+Bisogna però fare attenzione a un'aspetto: le espressioni regolari così costruite rappresentano __tutti i cammini__ possibili del programma, ma __non tutti e i soli__!
+Trattandosi di oggetti puramente matematici, infatti, le espressioni regolari sono necessariamente _più generali_ di qualunque programma: esse non tengono infatti conto degli _effetti_ che le istruzioni hanno sui dati e delle relative proprietà che si possono inferire. \
+Riprendendo a esempio l'espressione regolare di cui sopra, essa contiene la sequenza nella quale il ciclo viene eseguito _infinite volte_, ma osservando il programma è facile indovinare che tale comportamento non sia in realtà possibile: diminuendo progressivamente \\(\mathtt{a}\\) e \\(\mathtt{b}\\) a seconda di chi sia il maggiore si può dimostrare che prima o poi i due convergeranno allo stesso valore permettendo così di uscire dal ciclo.
+
+In effetti, uno stesso programma può essere rappresentato tramite __un numero infinito di espressioni regolari__ valide.
+Si potrebbe addirittura argomentare che l'espressione regolare
+
+$$
+\Big ( \\, \u \Big | \: \d \Big | \: \a \Big)*
+$$
+
+possa rappresentare qualsiasi programma. \
+Allontanandosi però dai casi estremi, si dimostra essere impossibile scrivere un algoritmo che dato un qualsiasi programma riesca a generare un'espressione regolare che rappresenti __tutti e soli__ i suoi cammini possibili senza osservare i valori delle variabili.
+Bisogna dunque accontentarsi di trovare espressioni regolari che rappresentino __al meglio__ l'esecuzione del programma, ovvero con il minor numero di cammini impossibili rappresentati.
+
+Nell'analisi Data Flow tramite espressioni regolari è quindi necessario tenere conto che il modello generato è un'__astrazione pessimistica__: se viene notificata la presenza di un errore non si può essere certi che esso ci sia veramente, in quanto esso potrebbe derivare da un cammino non percorribile.
\ No newline at end of file
diff --git a/src/12_analisi-statica/03_testing.md b/src/12_analisi-statica/03_testing.md
new file mode 100644
index 0000000..d988a6d
--- /dev/null
+++ b/src/12_analisi-statica/03_testing.md
@@ -0,0 +1,23 @@
+# Testing
+
+Oltre ad essere un processo utile di per sé per il rilevamento di potenziali errori, l'__analisi statica__ può anche contribuire a guidare l'attività di __testing__. \
+Per capire come, osserviamo che a partire dall'analisi statica è possibile fare le seguenti osservazioni:
+
+- perché si presenti un malfunzionamento dovuto a una anomalia in una _definizione_, deve esserci un _uso_ che si serva del valore assegnato;
+- un ciclo dovrebbe essere ripetuto (di nuovo) se verrà _usato_ un valore _definito_ alla iterazione precedente.
+
+L'analisi statica può quindi aiutare a __selezionare i casi di test__ basandosi sulle _sequenze definizione-uso_ delle variabili, costruendo cioè dei nuovi criteri di copertura.
+
+## Terminologia
+
+Per rendere più scorrevole la spiegazione dei prossimi argomenti introduciamo innanzitutto un po' di terminologia.
+
+Dato un nodo \\(i\\) del diagramma di flusso (_un comando/riga del programma_), chiamiamo \\(\operatorname{def}(i)\\) l'__insieme delle variabili definite in__ \\(\bf{i}\\).
+
+Data invece una variabile \\(x\\) e un nodo \\(i\\), chiamiamo \\(\operatorname{du}(x, \\, i)\\) l'insieme dei nodi \\(j\\) tali che:
+
+- \\(x \in \operatorname{def}(i)\\), ovvero la variabile \\(x\\) è __definita__ in \\(i\\);
+- \\(x\\) è __usata__ nel nodo \\(j\\);
+- __esiste un cammino__ da \\(i\\) a \\(j\\) __libero da definizioni__ di \\(x\\), ovvero che se seguito non sovrascrive il valore di \\(x\\).
+
+Si tratta cioè dell'__insieme di nodi \\(\bf{j}\\) che _potrebbero_ usare il valore di \\(\bf{x}\\) definito in \\(\bf{i}\\)__.
diff --git a/src/12_analisi-statica/04_criteri/00_index.md b/src/12_analisi-statica/04_criteri/00_index.md
new file mode 100644
index 0000000..7653015
--- /dev/null
+++ b/src/12_analisi-statica/04_criteri/00_index.md
@@ -0,0 +1,5 @@
+# Criteri di copertura derivati dall'analisi statica
+
+- [**Criterio di copertura delle definizioni**](./01_definizioni.md)
+- [**Criterio di copertura degli usi**](./02_usi.md)
+- [**Criterio di copertura dei cammini DU**](./03_cammini-du.md)
diff --git a/src/12_analisi-statica/04_criteri/01_definizioni.md b/src/12_analisi-statica/04_criteri/01_definizioni.md
new file mode 100644
index 0000000..c54f587
--- /dev/null
+++ b/src/12_analisi-statica/04_criteri/01_definizioni.md
@@ -0,0 +1,98 @@
+<!-- KaTeX op macro definitions -->
+<div style="display: none; margin: 0;">
+$$
+\require{color}
+% Regular operations
+\def\op#1{
+  \fcolorbox{black}{white}{$\vphantom{d} \sf{#1}$}
+}
+\def\d{\op{d} \,}
+\def\a{\op{a} \,}
+\def\u{\op{u} \,}
+% Erroneous operations
+\def\opR#1{
+  \fcolorbox{black}{orangered}{$\vphantom{d} \color{white}{\sf{#1}}$}
+}
+\def\dR{\opR{d} \,}
+\def\aR{\opR{a} \,}
+\def\uR{\opR{u} \,}
+% Subscript operations
+\def\Op#1#2{
+  \fcolorbox{black}{white}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+\def\D#1{\Op{d}{#1} \,}
+\def\A#1{\Op{a}{#1} \,}
+\def\U#1{\Op{u}{#1} \,}
+% Warning subscript operations
+\def\OpW#1#2{
+  \fcolorbox{black}{orange}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+% Green subscript operations
+\def\OpG#1#2{
+  \fcolorbox{black}{lightgreen}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+\def\DG#1{\OpG{d}{#1} \,}
+\def\AG#1{\OpG{a}{#1} \,}
+\def\UG#1{\OpG{u}{#1} \,}
+% Error
+\def\Err{
+  \color{red}{\sf{ERROR}}
+}
+\def\err{
+  \, \Err
+}
+$$
+</div>
+
+# Criterio di copertura delle definizioni
+
+_Un test \\(\ T\\) soddisfa il __criterio di copertura delle definizioni__ se e solo se per ogni nodo \\(i\\) e ogni variabile \\(x \in \operatorname{def}(i)\\), \\(T\\) include un caso di test che esegue un cammino libero da definizioni da \\(i\\) ad __almeno uno__ degli elementi di \\(\operatorname{du}(i, x).\\)_
+
+Ci si vuole cioè assicurare di testare tutte le definizioni, assicurandosi che funzionino osservando almeno un uso del valore da loro assegnato.
+Matematicamente si può dire che:
+
+$$
+\begin{align*}
+T \in C_{def} \Longleftrightarrow& \forall i \in P, \  \forall x \in \operatorname{def}(i), \ \exists j \in \operatorname{du}(i, \\, x), \\\\
+& \exists t \in T \ \text{che esegue un cammino da $i$ a $j$ senza ulteriori definizioni di $x$}.
+\end{align*}
+$$
+
+Riconsideriamo l'esempio già visto in precedenza, considerando la variabile \\(\mathtt{a}\\):
+
+```c
+01  void main() {
+02      float a, b, x, y;
+03      read(x);
+04      read(y);
+05      a = x;
+06      b = y;
+07      while (a != b)
+08          if (a > b)
+09              a = a - b;
+10          else
+11              b = b - a;
+12      write(a);
+13  }
+```
+
+Partiamo definendo gli insiemi dei nodi degli usi \\(\operatorname{du}(i, \\, \mathtt a)\\):
+
+1. \\(\operatorname{du}(5, \\, \mathtt a)\\) = \\(\{7, \\, 8, \\, 9, \\, 11, \\, 12\}\\);
+2. \\(\operatorname{du}(9, \\, \mathtt a)\\) = \\(\{7, \\, 8, \\, 9, \\, 11, \\, 12\}\\).
+
+È solo __un caso__ il fatto che in questo esempio tali insiemi siano uguali. \
+Comunque sia, l'obiettivo è _per ognuna delle due definizioni_ ottenere un __uso__ di tale definizione:
+
+1. Per la prima definizione la soluzione è banale, a riga 7 la variabile \\(\mathtt a\\) viene letta sempre:
+\\(\D{5}\U{7}\\).
+2. Per la seconda, invece, è necessario scegliere un valore tale per cui il flusso di esecuzione entri almeno una volta nel ciclo ed esegua almeno una volta la riga 9:
+\\(\D{9}\U{7}\\).
+
+Un test che soddisfa totalmente il criterio può essere il seguente:
+
+$$
+T = \{ \langle 8, \\, 4 \rangle \}.
+$$
+
+Come si vede, il criterio di copertura delle definizioni non copre tutti i comandi e di conseguenza __non implica il criterio di copertura dei comandi__.
diff --git a/src/12_analisi-statica/04_criteri/02_usi.md b/src/12_analisi-statica/04_criteri/02_usi.md
new file mode 100644
index 0000000..4f8e4f8
--- /dev/null
+++ b/src/12_analisi-statica/04_criteri/02_usi.md
@@ -0,0 +1,146 @@
+<!-- KaTeX op macro definitions -->
+<div style="display: none; margin: 0;">
+$$
+\require{color}
+% Regular operations
+\def\op#1{
+  \fcolorbox{black}{white}{$\vphantom{d} \sf{#1}$}
+}
+\def\d{\op{d} \,}
+\def\a{\op{a} \,}
+\def\u{\op{u} \,}
+% Erroneous operations
+\def\opR#1{
+  \fcolorbox{black}{orangered}{$\vphantom{d} \color{white}{\sf{#1}}$}
+}
+\def\dR{\opR{d} \,}
+\def\aR{\opR{a} \,}
+\def\uR{\opR{u} \,}
+% Subscript operations
+\def\Op#1#2{
+  \fcolorbox{black}{white}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+\def\D#1{\Op{d}{#1} \,}
+\def\A#1{\Op{a}{#1} \,}
+\def\U#1{\Op{u}{#1} \,}
+% Warning subscript operations
+\def\OpW#1#2{
+  \fcolorbox{black}{orange}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+% Green subscript operations
+\def\OpG#1#2{
+  \fcolorbox{black}{lightgreen}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+\def\DG#1{\OpG{d}{#1} \,}
+\def\AG#1{\OpG{a}{#1} \,}
+\def\UG#1{\OpG{u}{#1} \,}
+% Error
+\def\Err{
+  \color{red}{\sf{ERROR}}
+}
+\def\err{
+  \, \Err
+}
+$$
+</div>
+
+# Criterio di copertura degli usi
+
+_Un test \\(\ T\\) soddisfa il __criterio di copertura degli usi__ se e solo se per ogni nodo \\(i\\) e ogni variabile \\(x\\) appartenente a \\(\operatorname{def}(i)\\), \\(T\\) include un caso di test che esegue un cammino libero da definizioni da \\(i\\) ad __ogni elemento__ di \\(\operatorname{du}(i, \\, x).\\)_
+
+Sembra simile al precedente, con la differenza che ora bisogna coprire __tutti__ i potenziali usi di una variabile definita.
+Questo appare ancora più chiaro osservando la formula matematica:
+
+$$
+\begin{align*}
+T \in C_{path} \Longleftrightarrow& \forall i \in P, \  \forall x \in \operatorname{def}(i), \ \forall j \in \operatorname{du}(i, \\, x), \\\\
+& \exists t \in T \ \text{che esegue un cammino da $i$ a $j$ senza ulteriori definizioni di $x$}.
+\end{align*}
+$$
+
+Si noti però che il criterio di copertura degli usi __non implica il criterio di copertura delle definizioni__, perché nel caso in cui non esistano \\(j \in \operatorname{du}(i, \\, x)\\) l'uso del \\(\forall\\) è più _"permissivo"_ del \\(\exists\\) del criterio precedente: quest'ultimo richiedeva infatti che per ogni definizione esistesse almeno un uso, mentre il criterio di copertura degli usi non pone tale clausola (_se non ci sono usi il \\(\forall\\) è sempre vero_).
+Viene quindi da sé che questo criterio non copre neanche il criterio di copertura dei comandi.
+
+Riconsideriamo nuovamente il programma in C visto in precedenza come esempio:
+
+```c
+01  void main() {
+02      float a, b, x, y;
+03      read(x);
+04      read(y);
+05      a = x;
+06      b = y;
+07      while (a != b)
+08          if (a > b)
+09              a = a - b;
+10          else
+11              b = b - a;
+12      write(a);
+13  }
+```
+
+Come prima, consideriamo la variabile \\(\mathtt a\\) e i relativi insieme dei nodi degli usi per ogni sua definizione:
+
+1. \\(\operatorname{du}(5, \\, \mathtt a)\\) = \\(\{7, \\, 8, \\, 9, \\, 11, \\, 12\}\\);
+2. \\(\operatorname{du}(9, \\, \mathtt a)\\) = \\(\{7, \\, 8, \\, 9, \\, 11, \\, 12\}\\).
+
+Per ogni definizione occorre coprire __tutti gli usi__:
+
+<style>
+  #criterio-usi-tabella {
+    text-align: center;
+  }
+  #criterio-usi-tabella p {
+    margin-bottom: 0;
+  }
+</style>
+
+<table id="criterio-usi-tabella" style="text-align: center;">
+<tr>
+  <th style="width: 50%">
+
+\\(\operatorname{du}(5, \\, \mathtt a)\\)
+  </th>
+  <th>
+  
+  \\(\operatorname{du}(9, \\, \mathtt a)\\)</th>
+</tr>
+<tr>
+  <td>
+  
+  \\(\D{5}\UG{7}\UG{8}\UG{11}\U{7}\UG{12}\\)
+  </td>
+  <td>
+  
+  \\(\dots \\, \D{9} \UG7 \UG8 \UG9 \dots\\)
+  </td>
+</tr>
+<tr>
+  <td>
+  
+  \\(\dots \\, \D5 \U7 \U8 \UG9 \dots\\)
+  </td>
+  <td>
+  
+  \\(\dots \\, \D9 \U7 \U8 \UG{12} \dots\\)
+  </td>
+</tr>
+<tr>
+  <td></td>
+  <td>
+  
+  \\(\dots \\, \D9 \U7 \U8 \UG{11} \dots\\)
+  </td>
+</tr>
+</table>
+
+Un test che soddisfa totalmente il criterio può essere il seguente:
+
+$$
+T = \{ \langle 4, \\,  8 \rangle, \\, \langle 12, \\, 8 \rangle, \\, \langle 12, \\, 4 \rangle \}.
+$$
+
+Questo esempio permette di notare qualcosa sulla natura dei cicli: dovendo testare ogni percorso al loro interno è necessario fare almeno due iterazioni.
+Può quindi sorgere un dubbio: è meglio che le due iterazioni siano fatte nello stesso caso di test o in casi test separati? Ovvero, è meglio __minimizzare__ i __casi di test__ o le __iterazioni per caso__? \
+Opinione diffusa è quella secondo cui è preferibile __minimizzare le iterazioni__: partizionando le casistiche in diversi casi di test è possibile rilevare con più precisione gli errori, riducendo il tempo di debug.
+In alcune situazioni però aumentare il numero di iterazioni può diminuire il tempo di esecuzione totale dei test, in quanto dovendo riavviare il programma per ciascun caso di test la somma dei tempi di startup può diventare significativa per software molto massicci.
diff --git a/src/12_analisi-statica/04_criteri/03_cammini-du.md b/src/12_analisi-statica/04_criteri/03_cammini-du.md
new file mode 100644
index 0000000..57d8510
--- /dev/null
+++ b/src/12_analisi-statica/04_criteri/03_cammini-du.md
@@ -0,0 +1,14 @@
+# Criterio di copertura dei cammini DU
+
+Nel criterio precedente si richiedeva di testare _un_ cammino da ogni definizione ad ogni suo uso, ma come sappiamo i cammini tra due istruzioni di un programma possono essere molteplici.
+Potrebbe dunque sorgere l'idea di testarli _tutti_: da questa intuizione nasce il __criterio di copertura dei cammini DU__.
+
+$$
+\begin{align*}
+T \in C_{pathDU} \Longleftrightarrow& \forall i \in P, \  \forall x \in \operatorname{def}(i), \ \forall j \in \operatorname{du}(i, \\, x), \\\\
+&\forall \text{ cammino da $i$ a $j$ senza ulteriori definizioni di $x$} \\\\
+& \exists t \in T \ \text{che lo esegue}.
+\end{align*}
+$$
+
+Questo criterio può essere __utile da ipotizzare__, ma a causa dell'esplosione combinatoria del numero dei cammini è considerato __impraticabile__ (_"sopra la barra rossa"_).
diff --git a/src/12_analisi-statica/05_oltre-variabili.md b/src/12_analisi-statica/05_oltre-variabili.md
new file mode 100644
index 0000000..819d8eb
--- /dev/null
+++ b/src/12_analisi-statica/05_oltre-variabili.md
@@ -0,0 +1,69 @@
+<!-- KaTeX op macro definitions -->
+<div style="display: none; margin: 0;">
+$$
+\require{color}
+% Regular operations
+\def\op#1{
+  \fcolorbox{black}{white}{$\vphantom{d} \sf{#1}$}
+}
+\def\d{\op{d} \,}
+\def\a{\op{a} \,}
+\def\u{\op{u} \,}
+% Erroneous operations
+\def\opR#1{
+  \fcolorbox{black}{orangered}{$\vphantom{d} \color{white}{\sf{#1}}$}
+}
+\def\dR{\opR{d} \,}
+\def\aR{\opR{a} \,}
+\def\uR{\opR{u} \,}
+% Subscript operations
+\def\Op#1#2{
+  \fcolorbox{black}{white}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+\def\D#1{\Op{d}{#1} \,}
+\def\A#1{\Op{a}{#1} \,}
+\def\U#1{\Op{u}{#1} \,}
+% Warning subscript operations
+\def\OpW#1#2{
+  \fcolorbox{black}{orange}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+% Green subscript operations
+\def\OpG#1#2{
+  \fcolorbox{black}{lightgreen}{$\vphantom{d_6} \sf{#1}_{#2}$}
+}
+\def\DG#1{\OpG{d}{#1} \,}
+\def\AG#1{\OpG{a}{#1} \,}
+\def\UG#1{\OpG{u}{#1} \,}
+% Error
+\def\Err{
+  \color{red}{\sf{ERROR}}
+}
+\def\err{
+  \, \Err
+}
+$$
+</div>
+
+# Oltre le variabili
+
+L'analisi del flusso dati si può estendere anche su altri _"oggetti"_, non solo variabili. \
+Per esempio, è possibile prevedere le seguenti operazioni su un __file__:
+
+- \\(\op{a}\\) (__apertura__): specializzata in _per lettura_ o _per scrittura_;
+- \\(\op{c}\\) (__chiusura__);
+- \\(\op{l}\\) (__lettura__);
+- \\(\op{s}\\) (__scrittura__).
+
+Date queste operazioni si possono individuare una serie di regole, come per esempio:
+
+1. \\(\op{l}\\), \\(\op{s}\\) e \\(\op{c}\\) devono essere precedute da \\(\op{a}\\) senza \\(\op{c}\\) intermedie;
+2. \\(\op{a}\\) deve essere seguita da \\(\op{c}\\) prima di un'altra \\(\op{a}\\);
+3. legami tra tipo di apertura (per lettura o per scrittura) e relative operazioni.
+
+È interessante notare il __legame__ tra l'attività di analisi del flusso di dati e i diagrammi UML a stati finiti: un _oggetto_ risponde a una certa _tipologia di eventi_, può essere in diversi _stati_ e in certi _stati_ non sono ammesse alcune _operazioni_.
+Si noti come nessuna delle due discipline entra comunque nel merito del valore delle variabili, relegato ad un'analisi a runtime.
+
+## Criterio di _copertura del budget_
+
+Molto spesso nei contesti reali l'unico criterio applicato è quello di __copertura del budget__: si continuano a creare casi di test finché non sono finite le risorse (tempo e soldi).
+Questa tecnica ovviamente non fornisce alcuna garanzia sull'efficacia dei test, ed è sicuramente sconsigliata.
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index d8d1cce..baa832e 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -132,7 +132,17 @@
         - [Criterio di \\(n\\)-copertura dei cicli](./11_testing/05_altri-criteri/02_cicli.md)
     - [Mappa finale implicazioni tra criteri di copertura](./11_testing/06_mappa.md)
 
-- [Analisi statica]()
+- [Analisi statica](./12_analisi-statica/00_index.md)
+    - [Compilatori](./12_analisi-statica/01_compilatori.md)
+    - [Analisi Data Flow](./12_analisi-statica/02_data-flow/00_index.md)
+        - [Regole](./12_analisi-statica/02_data-flow/01_regole.md)
+        - [Sequenze](./12_analisi-statica/02_data-flow/02_sequenze.md)
+    - [Testing](./12_analisi-statica/03_testing.md)
+    - [Criteri di copertura](./12_analisi-statica/04_criteri/00_index.md)
+        - [Criterio di copertura delle definizioni](./12_analisi-statica/04_criteri/01_definizioni.md)
+        - [Criterio di copertura degli usi](./12_analisi-statica/04_criteri/02_usi.md)
+        - [Criterio di copertura dei cammini DU](./12_analisi-statica/04_criteri/03_cammini-du.md)
+    - [Oltre le variabili](./12_analisi-statica/05_oltre-variabili.md)
 
 - [Processi di review]()
 
-- 
GitLab