Metodi Formali dell'Informatica

• Prof: Ugo De’ Liguoro
• PDF Version
• Testo:
  • Programming Language Foundation in Agda

Teoria

I linguaggi sono definibili come sistemi formali, composti di

• alfabeto di simboli
• espressioni ben formate
• regole di inferenza

Metodi Formali

Derivano dalla logica-matematica

• Chompsky - Teoria delle Grammatiche
  • paralleli con gli automi
• Linguaggi di programmazione - Linguaggi formali
  • metodo che permette di verificare - Metodi Formale
    • descrizioni formali del comportamento dei programmi

In computer science formal methods are a particular kind of mathematically based techniques for the specification, development and verification of software and hardware systems - Wikipedia

• Componenti dei metodi formali
  • calcoli logici
  • sistemi di riscrittura
    • semplificazioni
  • linguaggi formali
  • teoria degli automi
  • sistemi di transizione
  • algebra dei dati
  • algebra dei processi
    • esecuzione concorrente
  • algebra relazionale
    • basi di dati
  • semantica dei linguaggi di programmazione
  • teoria dei tipi
  • analisi statica
    • Data Flow
    • Control Flow
    • Abstract Interpretation

L’utilitá é l’analisi matematica che dimostri la robustezza e la correttezza della progettazione hardware e software

• Tool:
  • Infer
  • Key
  • Viper

Il Problema della Verifica

• In:
  • descrizione di un sistema
  • specifica del suo comportamento o sua proprietá
• Out:
  • evidenza del fatto che il sistema soddisfa la specifica
  • controesempio che non funziona

1. Semantica Operazionale Definisce il significato di un programma come il suo comportamento che, quando termina, trasforma uno stato in un altro

2. Semantica Logica Pre e Post condizioni che un programma soddisfa

   • Floyd
     • metodo delle asserzioni - 1967
       • controllo del flusso di grafi che descrivono le aspettative sullo stato della memoria
   • Hoare
     • formalizza le idee di Floyd
     • Logica di Hoare
       • $‘\{\phi \}P\{\psi \}‘$
         • in P out

3. Verifica Statica Il programma non viene eseguito - statico Il testing é fatto sull’esecuzione - dinamico

   • l’importante é la scelta degli esempi di testing
     • G.J.Myers, The Art of Software Testing
   • essendo i test infiniti il superamento di qualsiasi test non verifica il programma
     • é un metodo di ricerca degli errori, non di verifica Processo:
   1. Contratto
   2. Invariante di Loop
      • esistono euristiche per trovarlo ma non algoritmi
   3. Asserzioni Intermedie
      • conducono alla dimostrazione di ció che voglio

4. Logica di Hoare HL Usiamo logica debole, non dimostriamo la terminazione. Se il programma termina allora é il risultato sará corretto.

   • Rules:
     • skip
     • assignments
     • sequencing
     • conditionals
     • while loops
     • consequence

   1. Correttezza di HL Teorema: Se la tripla é derivabile in HL, allora é valida

   2. Limiti teorici La logica del primo ordine é corretta e completa ma é indecidibile

      • Teorema di Church
      • non esiste un algoritmo che verifichi che formula logica sia corretta HL é corretta, ma completa solo in senso debole; include FOL dunque é indecidibile

      Allora si utilizzano Truth Assistant, il teorema di Rice ci dimostra che i Verificatori non possono esistere.

      • Isabelle
      • Coq
      • Agda
        • un linguaggio di programmazione funzionale
      • VeriFast
        • ProofAssistant dedicato a Separation Logic in C e Java

5. Separation Logic Per trattare linguaggi imperativi con puntatori, gestione dinamica della memoria

   • si utilizza per modularizzare

   • si guarda una funzione per volta

     • poi si uniscono i risultati per dimostrare la correttezza totale Si estendono le asserzioni con:

   • $‘s,h\models \text{emp}‘$

     • empty heap

   • $‘s,h\models a\to a^{\prime }‘$

     • singleton heap

   • $‘s,h\models P\star Q‘$

     • separating conjunction
     • $‘h_1\uplus h_2‘$ Le triple $‘(c,s,h)‘$ sono dette safe se $‘(c,s,h)/{\to }_{\ast }\text{error}‘$

   1. Frame Rule

      $$\frac{\{P\}c\{Q\}}{\{P\star R\}c\{Q\star R\}}$$

      • pre-condizione $‘P‘$

      • post-condizione $‘Q‘$

      • contesto $‘R‘$ Se vale questo allora posso spezzare in moduli il codice e verificare questi sottoinsiemi Lemmi:

      • monotonicitá

        • $‘(c,s,h)\text{safe}⟹\forall h^{\prime }\perp h:(c,s,h\uplus h^{\prime })\text{safe}‘$
        • $$\begin{gathered} ‘(c,s,h_0){\to }^{\ast }(\text{skip},s^{\prime },h_0^{\prime })⟹ \\ \forall h_1\perp h_0:(c,s,h_0\uplus h_1){\to }^{\ast }(\text{skip},s^{\prime },h_0^{\prime }\uplus h_1^{\prime })‘ \end{gathered}$$
        • $‘(c,s,h_0)‘$ riduce all’infinito $‘⟹\forall h_1\perp h_0:(c,s,h_0\uplus h_1)‘$ riduce all’infinito

      • frame property

        • $$\begin{gathered} ‘(c,s,h_0)\text{safe}\wedge (c,s,h_0\uplus h_1){\to }^{\ast }(\text{skip},s^{\prime },h^{\prime })⟹ \\ \exists h_0^{\prime }\perp h_1:(c,s,h_0){\to }^{\ast }(\text{skip},s^{\prime },h_0^{\prime })\wedge h^{\prime }=h_0^{\prime }\uplus h_1‘ \end{gathered}$$

   2. Heap Simbolici $‘H::=\exists \vec{x}:(P_1\wedge \cdots \wedge P_n)\wedge (S_1\star \cdots \star S_m)‘$

      • $‘\vec{x}={⋓}_{i}fv(P_i)\cup {⋓}_{j}fv(S_j)‘$
      • puro e spaziale Dai comandi atomici, definiti conseguentemente alle rispettive regole della logica. Si eseguono poi sequenze atomiche
      $$\{H\}{A}_1;\cdots ;A_n\{H^{\prime }\}$$ $$\frac{\{H\}{A}_1\{H^{\prime \prime }\}\{H^{\prime \prime }\}{A}_2\{H^{\prime }\}}{\{H\}{A}_1;A_2\{H^{\prime }\}}$$ $$\frac{H,A_1⟹H^{\prime }}{H,A_1;A_2⟹H^{\prime },A_2}$$

Grammatiche

Concrete

Descrivo Grammatiche Senza Contesti con le Regole di Inferenza

$$\frac{}{n\in Aexp}$$ $$\frac{}{x\in Aexp}$$ $$\frac{a_1\in Aexp{a}_2\in Aexp}{a_1+a_2\in Aexp}$$

Astratte

1. Backus Normal Form Utiliziamo la notazione carrificata

   vname ::== String
   aexp ::== N n | V x | Plus aexp aexp | Times aexp aexp

Semantica

Agda

Set, insieme o Tipo

data aexp: Set nohere
N: N -> aexp
V: String -> aexp
Plus: aexp -> aexp -> aexp
 
depth: aexp -> N
  depth (Nn) = 0
  depth (Vx) = 0
  depth (Plus a b) = 1 + max (depth a) (depth b)

Dim. per induzione strutturale:

depth (Plus a b) <= size (Plus a b)

La semantica di $‘a\in aexp‘$ é un numero $‘n\in N‘$ Per def il valore di $‘Vx‘$ usiamo gli stati

• $‘s\in state=vname\to val‘$

aval: aexp -> state -> val
  aval (N n) s = n
  aval (V x) s = sx
  aval (Plus a_1 a_2) s = (aval a_1 s) + (aval a_2 s)

$‘FVa‘$: l’insieme delle variabili libere in $‘a\in aexp‘$

FV (N n) = nil
FV (V x) = { n }
FV (Plus a_1 a_2) = (FVa_1) U (FVa_2)

1. Lemma FVa Se per ogni $‘x\in FVa‘$ gli stati $‘s,s^{{}^{\prime }}\mid sx=s^{{}^{\prime }}x‘$ allora $‘avalas=avala{s}^{{}^{\prime }}‘$

   • dim su ind. strutturale su $‘a‘$

Sostituzione

$‘a[a^{{}^{\prime }}/x]‘$ intendiama la sostituzione di x con a’ in a

(N n)[a'/x] = N n
(V x)[a'/x] = a'
(V y)[a'/x] = V y
(Plus a_1 a_2)[a'/x] = Plus a_1[a'/x] a_2[a'/x]

Modifica delle variabili Se $‘s\in state,x\in vname,n\in val\mid s[x\to n]\in state‘$

1. Lemma di Sostituzione $$aval(a[a^{{}^{\prime }}/x])s=avalas[x\to aval{a}^{{}^{\prime }}s]$$

Booleani

bexp ::= B bval
      | Not bexp | And bexp bexp
      | Less aexp aexp -- a < a'
 
bval ::= tt | ff

Comandi

Espressioni generate dalla grammatica (BNF)

Sintassi

com ::= SKIP                      -- noop
     |  vname := aexp             -- assegnazione
     |  com ; com                 -- composizione sequenziale
     |  IF bexp THEN com ELSE com -- selezione
     |  WHILE bexp DO com         -- iterazione

Con queste caratteristiche il nostro linguaggio IMP é Touring completo:

• Arbib, A programming approach to computability

Semantica di com

cval : com -> state -> state

Se questa funzione esiste deve essere parziale

• definita solo in alcuni casi

cval (WHILE b DO c) s = ??
cval (WHILE b DO c) s = s  -- bval b s = ff
cval (WHILE b DO c) s =    -- bval b s = tt
    = cval (c; WHILE b DO c) s
    = cval (WHILE b DO c) (cval c s)

In questo caso la definizione é circolare

Semantica Naturale - Big-step

Usiamo la relazione $‘(c,s)⟹t‘$ su $‘com\times state\times state‘$ $‘⟺‘$ l’esecuzione di $‘c‘$ in $‘s‘$ termina in $‘t‘$

$‘(c,s,t)\to (c,s)⟹t\in bool‘$

• true se in un stato finale, false altrimenti
• questa funzione é definibile in Agda

Sistema formale:

$$\frac{(c_1,s_1)⟹t_1\cdots (c_n,s_n)⟹t_n}{(c_{n+1},s_{n+1})⟹t_{n+1}}$$

1. Regole

   • Skip $$\frac{}{(SKIP,s)⟹s}$$
   • Ass \frac{aval \: a \: s = n}{(n:= a,s)\implies s[x\rightarrow n]
   • Comp $$frac(c_1,s)⟹s^{\prime }(c_2,s^{\prime })⟹t(c_1;c_2,s)⟹t$$

   IF b THEN c_1 ELSE c_2

   • $$\frac{bvalbs=tt(c_1,s)⟹t}{(IFbTHEN{c}_{1}ELSE{c}_2,s)}$$
   • $$\frac{bvalbs=ff(c_2,s)⟹t}{(IFbTHEN{c}_{1}ELSE{c}_2,s)}$$

   WHILE

   • $$\frac{bvalbs=ff}{(WHILEbDOc,s)⟹s}$$
   • $$\frac{bvalbs=tt(c,s)⟹s^{{}^{\prime }}(W,s^{{}^{\prime }})⟹t}{(WHILEbDOc,s)⟹t}$$
     • $‘W‘$ abbrevia $‘(WHILEbDOc,s)⟹t‘$ Con queste si studia la convergenza

   1. Proposizione SKIP $‘\forall s,t⊬(WHILEtrueDOSKIP,s)\Rightarrow t‘$ Dim

      • per assurdo sia $‘D‘$ una dimostrazione (derivazione chiusa) t.c. la sua conclusione sia $‘(WHILEtrueDOSKIP,s)\Rightarrow t‘$
      • poiché bval true s = tt per ogni s, D deve terminare con:
        • $‘\frac{(SKIP,s)\Rightarrow s^{{}^{\prime }}(W,s^{{}^{\prime }})\Rightarrow t}{(W,s)\Rightarrow t}‘$
        • ma s'=s per SKIP, dunque la des. D' ha la stessa forma di D, essendo propriamente inclusa in D, cioé é infinita
      • dunque D non é una dimostrazione

   2. Equivalenza di Programmi I comandi $‘c_1,c_2‘$ sono equivalenti [$c₁ ∼ c₂$]

      • $‘\forall s,t\in state.(c_1,s)\Rightarrow t⟺(c_2,s)\Rightarrow t‘$ Lemma WHILE b DO c ~ IF b THEN (c;WHILE b DO c) ELSE SKIP

   3. Determinismo della semantica naturale Teorema:

      • Per ogni $‘c\in com‘$ , per ogni $‘st,,t^{\prime }\in state‘$
      • $‘(c,s)\Rightarrow t\wedge (c,s)\Rightarrow t^{{}^{\prime }}⟹t=t^{{}^{\prime }}‘$

   4. Funzione parziale $‘[[\cdot ]]:com\to state\rightharpoonup state‘$ $‘[[c]]s=\{\begin{array}{ll}t& \text{mbox}se⊢(c,s)\Rightarrow t\\ \perp & \text{mbox}altrimenti\end{array}‘$

Semantica SOS - Small Step

Singolo passo di calcolo $‘(c,s)\to (c^{{}^{\prime }},s^{{}^{\prime }})‘$

• Lemma - determinismo
  • $‘(c,s)\to (c^{{}^{\prime }},s^{{}^{\prime }})\wedge (c,s)\to (c^{{}^{\prime \prime }},s^{{}^{\prime \prime }})⟹c^{{}^{\prime }}=c^{{}^{\prime \prime }}\wedge s^{{}^{\prime }}=s^{{}^{\prime \prime }}‘$
• Corollario
  • $‘(c,s)‘$ termina se $‘\exists t\mid (c,s){\to }^{\ast }(\text{textsc}skip,t)‘$, cicla se esiste una sequenza infinita
• Assegnazione
  • $‘(x:=a,s)\to (\text{textsc}skip,s[x\mapsto avalas])‘$
• SKIP
  • $‘(\text{textsc}skip;c,s)\to (c,s)‘$

• IF

  $$\frac{bvalbs=tt}{(\text{textsc}ifb\text{textsc}then{c}_1\text{textsc}else{c}_2,s)\to (c_1,s)}$$
  • $‘ff‘$ speculare
• WHILE
  • $(while\ b\ do\ c,s) →

(if\ b\ then\ (c;\ while\ b\ do\ c)\ else\ skip, s$

$‘[[c]{]}_{\text{textsc}sos}s=\{\begin{array}{ll}t& \text{mbox}se⊢(c,s){\to }^{\ast }(\text{textsc}skip,t)\\ \perp & \text{mbox}se(c,s)\text{mbox}cicla\end{array}‘$

• Teorema di equivalenza delle Semantiche

$‘\forall c\in \text{mbox}com\forall s,t\in \text{mbox}state\mid [[c]{]}_{\text{textsc}nat}s=[[c]{]}_{\text{textsc}sos}s‘$

Teoria dei Tipi

file Agda

Il quantificatore universale si traduce, nella teoria dei tipi dipendenti, in

$$\frac{A:\text{Set}x:A⊢B[x]:\text{Set}}{\pi [x:A]B[x]:\text{Set}}$$

dove

$‘\pi [x:A]B[x]\equiv B[a_1]\times B[a_2]\times \cdots ‘$ per $‘a_i\in A‘$ corrisponde a $‘\forall x.B[x]⟺B[a_1]\wedge B[a_2]\wedge \cdots ‘$

Il $‘\pi ‘$ sta per il concetto di indicizzazione:

• forma famiglie secondo i suoi indici

$‘\forall (\lambda x\to Bx):\text{Set}‘$

• il quantificatore é un operatore che viene applicata al lambda

Logica Classica e Intuizionistica

• Wadler

In Gilbert and Sullivan’s The Gondoliers, Casilda is told that as an infant she was married to the heir of the King of Batavia, but that due to a mix-up no one knows which of two individuals, Marco or Giuseppe, is the heir. Alarmed, she wails “Then do you mean to say that I am married to one of two gondoliers, but it is impossible to say which?” To which the response is “Without any doubt of any kind whatever.”

Logic comes in many varieties, and one distinction is between classical and intuitionistic. Intuitionists, concerned by assumptions made by some logicians about the nature of infinity, insist upon a constructionist notion of truth. In particular, they insist that a proof of A ⊎ B must show which of A or B holds, and hence they would reject the claim that Casilda is married to Marco or Giuseppe until one of the two was identified as her husband. Perhaps Gilbert and Sullivan anticipated intuitionism, for their story’s outcome is that the heir turns out to be a third individual, Luiz, with whom Casilda is, conveniently, already in love.

Intuitionists also reject the law of the excluded middle, which asserts A ⊎ ¬ A for every A, since the law gives no clue as to which of A or ¬ A holds. Heyting formalised a variant of Hilbert’s classical logic that captures the intuitionistic notion of provability. In particular, the law of the excluded middle is provable in Hilbert’s logic, but not in Heyting’s. Further, if the law of the excluded middle is added as an axiom to Heyting’s logic, then it becomes equivalent to Hilbert’s. Kolmogorov showed the two logics were closely related: he gave a double-negation translation, such that a formula is provable in classical logic if and only if its translation is provable in intuitionistic logic.

Propositions as Types was first formulated for intuitionistic logic. It is a perfect fit, because in the intuitionist interpretation the formula A ⊎ B is provable exactly when one exhibits either a proof of A or a proof of B, so the type corresponding to disjunction is a disjoint sum.

(Parts of the above are adopted from “Propositions as Types”, Philip Wadler, Communications of the ACM, December 2015.) ~ Philip Wadler cit

• Propositions as Types è un paradigma che pone le proposizioni e tipi come equivalenti.
  • in Type Theory
  • una proposizione è identificata come il tipo (collezione) delle sue prove
  • un tipo è identificato come la proposizione che contiene i suoi termini

Semantica di Heyting

$$\frac{B[t]}{\exists x.B[x]}$$ $$⟨t,M⟩:\exists x.B[x]$$

dove

$$M:B[t]$$

IMP

Definizione in Agda

Estensione Puntatori

com ::= ... | x := cons(a_1,...,a_2) allocation | n := [a] lookup | [a] := a' mutation | dispose(a) deallocation

la notazione [a] richiama il concetto di heap come array, dove a ne é l’indice

1. Semantica store = var_name -> Val heap = loc -> Val

   Per $‘h\in \text{heap},n\ge 0‘$

   • $‘h=\{l_1\to v_1\cdots l_n\to v_n\}‘$
   • $‘\text{dom}(h|l_1\cdots l_n)‘$
     • le locazioni allocate Viene aggiunta alla semantica SOS lo heap h
   1. Indipendenza dello Heap $‘h_1\perp h_2⟺\text{dom}(h_1)\cap \text{dom}(h_2)=\varnothing ‘$

Semantica Operazionale

File Agda

StackMachine

Basato su ~/Code/Agda/C-List.agda

• Source

Compilatore

Nipkow, cap. 8

Linguaggio IMP $‘⟶‘$ istruzioni di una macchina astratta

• c : com $‘\mapsto ‘$ p : prog
  • $‘(c,s)\Rightarrow t‘$
    • correttezza $‘\Rightarrow ‘$
    • completezza $‘\Leftarrow ‘$
  • $‘p⊢(0,s,[]){\to }^{\ast }(\text{size }p,t,[])‘$
    • program counter
    • memoria
    • stack

instr

• LOADI int
• LOAD vname
• ADD
• STORE vname
• JMP int
• JMPLESS int
• JMPGE int

Si definisce lookup i P dove $‘0\le i<\text{size}P‘$

• in Agda le funzioni parziali non sono ammesse e quindi questo va adattato

$$\frac{0\le i<\text{size }P\text{iexec }(\text{lookup }iP)(i,s,stk)\equiv (i^{\prime },s^{\prime },st{k}^{\prime })}{P⊢(i,s,stk)\to (i^{\prime },s^{\prime },st{k}^{\prime })}$$

Un singolo passo di esecuzione (programma $‘P‘$ esegue dalla configurazione $‘c‘$ a $‘c^{\prime }‘$) $‘P⊢c\to c^{\prime }‘$

1. bcomp $‘bcomp::bexp\Rightarrow bool\Rightarrow int\Rightarrow prog‘$

   Lemma 8.8 Si definisce il program counter sui salti condizionali:

   • $‘\text{pc’}=\text{size }(\text{bcomp }bfn)+(\text{ if }f=\text{ bval }bs\text{ then }n\text{ else }0)‘$