Semantiche dei linguaggi di
programmazione
A cosa serve la semantica di un linguaggio?
1.
Uno standard preciso per l’implementazione del linguaggio
(generazione di compilatori):
Come puo’ essere implementato il linguaggio in diverse
macchine?
2.
Documentazione per l’utente:
Qual’e’ il significato di un programma, data una particolare
combinazione dei costrutti linguistici supportati?
3.
Uno strumento per la progettazione e l’analisi:
Come puo essere sintonizzata la definizione del linguaggio
in modo che possa essere implementata in modo
efficiente?
Tino Cortesi
Analisi e Verifica di Programmi
2
Metodi per specificare la semantica
Semantica Operazionale:
[[ program ]] = programma per una macchina astratta
Semplice da implementare
Difficile ragionarci sopra
Semantica Denotazionale:
[[ program ]] = denotazione matematica (una funzione)
Facilita il ragionarci sopra
Non sempre e’ facile trovare domini semantici appropriati
Tino Cortesi
Analisi e Verifica di Programmi
3
Metodi per specificare la semantica
Semantica Assiomatica:
[[ programma ]] = insieme di proprieta’
Utile per provare teoremi sui programmi
Distante dalla implementazione
Structured Operational Semantics:
[[ programma ]] = transition system (regole di inferenza)
Utile per concorrenza e non determinismo
Difficile ragionare sull’equivalenza
Tino Cortesi
Analisi e Verifica di Programmi
4
Metodi per specificare la semantica
Semantica Denotazionale
Definisce un modello, una astrazione, una interpretazione

for the language designers
Semantica Assiomatica
Costruisce una teoria logica

for the programmers
Semantica Operazionale
Costruisce un interprete o una rappresentazione finita

Tino Cortesi
for the language implementors
Analisi e Verifica di Programmi
5
Esempio di semantica operazionale
Il comando C
viene espresso come:
for ( expr1; expr2; expr3 ){ • • • }
expr1;
loop: if expr2 = 0 goto out
•••
exp3;
goto loop
out: • • •
Basata su linguaggi di livello inferiore, non su matematica o logica
Tino Cortesi
Analisi e Verifica di Programmi
6
Esempio di semantica assiomatica
Notazione: {P} S {Q}
P preconditon
S comando
Q postcondition
Esempio
Trova la weakest precondition P per: {P} a = b + 1 {a > 1}
Una possibile precondition: {b > 10}
Weakest precondition:
{b > 0}
Tino Cortesi
Analisi e Verifica di Programmi
7
Esempio: Comando di assegnamento
Sia x=E un generico comando di assegnamento
In questo caso la semantcia dell’assegnamento e` data da un unico
assioma:
{Q
x  E}
x = E {Q}
La weakest precondition P viene data da Q x  E
In altre parole, P si ottiene dalla proprieta` Q sostituendo tutte le
occorrenze di x con l’espressione E
Ad esempio, {?} a = a + b – 3 {a > 10}
Sostuituisce tutte le occorrenze di a in {a >10} con a+b-3
Questo diventa: a+b-3>10, ovvero b>13-a
Quindi, Q x  E e’ { b>13-a }
Tino Cortesi
Analisi e Verifica di Programmi
8
Esempio: comando di selezione
Consideriamo il comando if-then-else
La regola di inferenza e’
{ B and P } S1 { Q }, { (not B) and P } S2 { Q}
{ P } if B then S1 else S2 { Q }
Esempio
{?} if ( x > 0 ) then y = y - 5 else y = y + 3 { y > 0 }
Le precondizioni per S2 sono { x <= 0 } e {y > -3 }
Le precodizioni per S1 sono { x > 0 } e {y > 5 }
Chi e’ allora P ?
Nota che { y > 5 } => { y > -3 }
Quindi la precondizione P e’ { y > 5 }
Tino Cortesi
Analisi e Verifica di Programmi
9
Semantica Denotazionale
Semantica Denotazionale
Ad ogni costrutto sintattico (parte del programma) P viene
associata la sua denotazione [| P |], un oggetto matematico
che rappresenta il contributo di P al significato di un qualsiasi
programma che contenga P.
Composizionalità: la denotazione di un costrutto linguistico
(parte del programma) dipende unicamente dalla denotazione
delle sue sotto-componenti
Tino Cortesi
Analisi e Verifica di Programmi
11
Il linguaggio while
Elementi
sintattici
Notazione
BNF
Tino Cortesi
Analisi e Verifica di Programmi
12
Semantica dei numerali
La funzione semantica associa
ad ogni numerale (in forma
binaria) il suo significato (un
elemento dell’insieme dei
numeri interi Z)
Ad esempio,
Tino Cortesi
Analisi e Verifica di Programmi
13
Stato ed Espressioni
Il significato dei una espressione aritmetica dipende dallo stato delle
variabili che vi appaiono.
Uno stato è una funzione che associa ad un insieme di variabili un
corrispondente insieme di valori
Data un’espressione aritmetica ed uno stato possiamo determinare il
valore di questa espressione
Tino Cortesi
Analisi e Verifica di Programmi
14
Semantica delle Espressioni
Tino Cortesi
Analisi e Verifica di Programmi
15
Esempio
Consideriamo l’espressione aritmetica (x+1), valutata in uno stato s
tale che s x = 3
Tino Cortesi
Analisi e Verifica di Programmi
16
Semantica delle espressioni booleane
Tino Cortesi
Analisi e Verifica di Programmi
17
Semantica dei comandi
Un comando è un costrutto che può modificare lo stato della
memoria: è quindi una funzione parziale tra stati
La semantica dell’assegnamento
assicura che se
allora
Tino Cortesi
Analisi e Verifica di Programmi
18
Comando sequenziale
La semantica del comando sequenziale considera il caso In cui una
ddelle due funzioni non sia definita riespetto agli argomenti:
Tino Cortesi
Analisi e Verifica di Programmi
19
Comando condizionale
Tino Cortesi
Analisi e Verifica di Programmi
20
Comando while
La semantica del comando
deve essere la stessa di
Quindi la semantica di
deve essere il punto fisso del funzionale F definito da
Tino Cortesi
Analisi e Verifica di Programmi
21
Comando while
La semantica del comando while è quindi:
dove l’operatore di punto fisso FIX è del tipo:
ma cosa ci assicura che il punto fisso esista?
Tino Cortesi
Analisi e Verifica di Programmi
22
C’è un minimo punto fisso?
Operazionalmente possono verificarsi tre casi nell’esecuzione del
comando while b do S a partire da uno stato s0 :
Il comando termina
C’è un loop interno (c’e’ un comando all’interno di S che non
termina)
E’ il loop while che non termina
Tino Cortesi
Analisi e Verifica di Programmi
23
Esempio
Se è lo stato in cui x vale 5, ecco un esempio per ognuno dei tre
casi precedenti:
while x>0 do x:=x-1
while x>0 do
if (x=1) then (while true do skip)
else x:= x-1
While true do skip
Tino Cortesi
Analisi e Verifica di Programmi
24
Problema…
Per garantire l’esistenza di soluzioni a questa equazione di punto
fisso sono necessarie condizioni:
Sul dominio: un ordine parziale? un CPO? un reticolo
completo?
Sul funzionale: monotono? continuo?
Tino Cortesi
Analisi e Verifica di Programmi
25