Semantica Denotazionale
Semantica Denotazionale
Ad ogni costrutto linguistico (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
Tecniche di Analisi di Programmi
2
Il linguaggio while
Tino Cortesi
Tecniche di Analisi di Programmi
3
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
Tecniche di Analisi di Programmi
4
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
Tecniche di Analisi di Programmi
5
Semantica delle Espressioni
Tino Cortesi
Tecniche di Analisi di Programmi
6
Esempio
Consideriamo l’espressione aritmetica (x+1), valutata in uno stato s
tale che s x = 3
Tino Cortesi
Tecniche di Analisi di Programmi
7
Semantica delle espressioni booleane
Tino Cortesi
Tecniche di Analisi di Programmi
8
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
Tecniche di Analisi di Programmi
9
Comando sequenziale
La semantica del comando sequenziale considera il caso In cui una
ddelle due funzioni non sia definita riespetto agli argomenti:
Tino Cortesi
Tecniche di Analisi di Programmi
10
Comando condizionale
Tino Cortesi
Tecniche di Analisi di Programmi
11
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
Tecniche di Analisi di Programmi
12
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
Tecniche di Analisi di Programmi
13
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
Tecniche di Analisi di Programmi
14