Semantica Denotazionale. Tino CortesiTecniche di Analisi di Programmi 2 Semantica Denotazionale Ad...
-
Upload
fillipo-turco -
Category
Documents
-
view
215 -
download
0
Transcript of Semantica Denotazionale. Tino CortesiTecniche di Analisi di Programmi 2 Semantica Denotazionale Ad...
Semantica Denotazionale
Tino Cortesi Tecniche di Analisi di Programmi 2
Semantica DenotazionaleAd 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 Tecniche di Analisi di Programmi 3
Il linguaggio while
Notazione BNF
Elementi sintattici
Tino Cortesi Tecniche di Analisi di Programmi 4
Semantica dei numeraliLa 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 5
Stato ed EspressioniIl 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 6
Semantica delle Espressioni
Tino Cortesi Tecniche di Analisi di Programmi 7
Esempio
Consideriamo l’espressione aritmetica (x+1), valutata in uno stato s tale che s x = 3
Tino Cortesi Tecniche di Analisi di Programmi 8
Semantica delle espressioni booleane
Tino Cortesi Tecniche di Analisi di Programmi 9
Semantica dei comandiUn 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 10
Comando sequenzialeLa 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 11
Comando condizionale
Tino Cortesi Tecniche di Analisi di Programmi 12
Comando whileLa 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 13
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 14
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 terminaC’è un loop interno (c’e’ un comando all’interno di S che non termina)E’ il loop while che non termina
Tino Cortesi Tecniche di Analisi di Programmi 15
EsempioSe è 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 Tecniche di Analisi di Programmi 16
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?