# Modelli Della Concorrenza

## Dimostrazioni di correttezza

**Logica proposizionale:**
- Preposizioni atomiche: $PA = \{p_1, p_2, \dots, p_i, \dots\}$.
- Constanti logiche: $\top, \bot$.
- Connettivi: $\lnot, \lor, \land, \rightarrow, \leftrightarrow$.
- Delimitatori: $(,)$

Definiamo induttivamente $F_p$: insieme delle formule ben formate:
- $\top, \bot \in F_p$.
- $\forall p_i \in PA, pi \in F_p$
- se $A$ e $B \in F_p$ allora $(\lnot A), (A \land B), (A \lor B), \dots \in F_p$

**Semantica:** funzione di valutazione $V:PA \rightarrow \{0, 1\}$
Estendiamo $V$ a $F_p$:
$I_V:F_p \rightarrow \{0, 1\}$ interpretazione.
- $I_V(\bot) = 0, I_V(\top) = 1$
- $\forall p_i \in PA$ $I_V(p_i) = V(P_i)$
- $I_V(\lnot A) = 1 - I_V(A)$
- $I_V(A \land B) = 1 \iff I_V(A) = 1 \land I_V(B) = 1$
- $I_V(A \lor B) = 1 \iff I_V(A) = 1 \lor I_V(B) = 1$
- $I_V(A \rightarrow B) = 1 \iff I_V(A) = 0 \lor I_V(B) = 1$

Diciamo inoltre che:
- $A$ risulta soddisfatta da $I_V$ se $I_V(A)=1$.
- $A$ risulta soddisfacibile se esiste $I_V$ tale che $I_V(A)=1$.
- $A$ è una tautologia se $I_V(A)=1$ per ogni $I_V$.
- $A$ è contraddittoria se $I_V(A)=0$ per ogni $I_V$.

**Modello** $M \subseteq PA$, $I_M:Fp \rightarrow \{0, 1\}$, $I_M(p_i) = 1 \iff p_i \in M$.

$M \models A$: $A$ è soddisfatta in $M$.

**Apparato deduttivo**.
- $\frac{A_1, A_2}{A_1 \land A_2}$, $\frac{A_1 \land A_2}{A_1}$, $\frac{A_1 \land A_2}{A_2}$
- Modus Ponens: $\frac{A, A \rightarrow B}{B}$
- Modus Tollens: $\frac{\lnot B, A \rightarrow B}{\lnot A}$

**Dimostrazione**: Catena di applicazioni di regole di inferenza.
**Validità, correttezza**: Se $A_1, \dots, A_N \vdash B$ allora $A_1, \dots, A_N \models B$.
**Completezza**: Se $A_1, \dots, A_N \models B$ allora $A_1, \dots, A_N \vdash B$.

**Logica per ragionare sui programmi**: Aggiungo uno stato della memoria:
$V$ insieme delle variabili del programma. $\sigma : V \rightarrow Z$. $\sigma \models \alpha$: "$\alpha$ è vera in $\sigma$"
**Tripla di Hoare**: $\{\alpha\}C\{\beta\}$: se il comando $C$ viene eseguito a partire da uno stato della memoria nel quale vale $\alpha$, allora l'esecuzione termina, e nello stato finale $\beta$ risulta vera.


Valgono:
- **Correttezza**: $\vdash \rightarrow \models$: Se posso ottenere una certe tripla tramite derivazioni allora risulta vera rispetto all'interpretazione.
- **Completezza(relativa, incompletezza dell'aritmetica)**: $\models \rightarrow \vdash$: Se tale tripla risulta vera rispetto all'interpretazione allora posso derivarla.

**Precondizione più debole**:
- $V$ insieme delle variabili di $C$.
- $\Sigma = \{\sigma | \sigma: V \rightarrow Z\}$ insieme degli stati.
- $\Pi$ insieme delle formule su $V$.
- $\models \subseteq \Sigma \times \Pi$
- $t(\sigma) = \{p \in \Pi | \sigma \models p\}$ insieme delle formule vere in $\sigma$.
- $m(p) = \{\sigma | \sigma \models p \}$ insieme degli stati in cui vale $p$.
- $S \subseteq \Sigma$ sottoinsieme di stati, $F \subseteq \Pi$ sottoinsieme di formule.
- $t(S) = \{p \in \Pi | \forall s \in S, s \models p\}$
- $m(F) = \{\sigma \in \Sigma | \forall p \in F, \sigma \models p\}$
- **precondizione più debole**: cerchiamo $p$ tale che $\models \{p\} C \{q\}$ e $p$ sia più debole possibile. $p$ rappresenta il più grande insieme di stati a partire dai quali l'esecuzione di $C$ porta ad uno stato in $m(Q)$.
- $wp(W, q) = (\lnot B \land q) \lor (B, wp(C;W, q))$