Semantiche dei linguaggi di programmazione

Tino Cortesi Analisi e Verifica di Programmi 2

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 3

Metodi per specificare la semantica

Semantica Operazionale:[[ program ]] = programma per una macchina astrattaSemplice da implementareDifficile ragionarci sopra

Semantica Denotazionale:[[ program ]] = denotazione matematica (una funzione)Facilita il ragionarci sopraNon sempre e’ facile trovare domini semantici appropriati

Tino Cortesi Analisi e Verifica di Programmi 4

Metodi per specificare la semantica

Semantica Assiomatica:[[ programma ]] = insieme di proprieta’ Utile per provare teoremi sui programmiDistante dalla implementazione

Structured Operational Semantics:[[ programma ]] = transition system (regole di inferenza)Utile per concorrenza e non determinismoDifficile ragionare sull’equivalenza

Tino Cortesi Analisi e Verifica di Programmi 5

Metodi per specificare la semantica

Semantica DenotazionaleDefinisce un modello, una astrazione, una interpretazione

for the language designers

Semantica AssiomaticaCostruisce una teoria logica

for the programmers

Semantica OperazionaleCostruisce un interprete o una rappresentazione finita

for the language implementors

Tino Cortesi Analisi e Verifica di Programmi 6

Esempio di semantica operazionale

Il comando C for ( expr1; expr2; expr3 ){ • • • }

viene espresso come:

Basata su linguaggi di livello inferiore, non su matematica o logica

expr1;loop: if expr2 = 0 goto out • • • exp3; goto loopout: • • •

Tino Cortesi Analisi e Verifica di Programmi 7

Esempio di semantica assiomatica

Notazione: {P} S {Q}P preconditonS comandoQ postcondition

EsempioTrova 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 8

Esempio: Comando di assegnamento

Sia x=E un generico comando di assegnamentoIn 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-3Questo diventa: a+b-3>10, ovvero b>13-aQuindi, Q x E e’ { b>13-a }

Tino Cortesi Analisi e Verifica di Programmi 9

Esempio: comando di selezioneConsideriamo il comando if-then-else La regola di inferenza e’

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 }

{ B and P } S1 { Q }, { (not B) and P } S2 { Q}{ P } if B then S1 else S2 { Q }

Semantica Denotazionale

Tino Cortesi Analisi e Verifica di Programmi 11

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 Analisi e Verifica di Programmi 12

Il linguaggio while

Notazione BNF

Elementi sintattici

Tino Cortesi Analisi e Verifica di Programmi 13

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 Analisi e Verifica di Programmi 14

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 Analisi e Verifica di Programmi 15

Semantica delle Espressioni

Tino Cortesi Analisi e Verifica di Programmi 16

Esempio

Consideriamo l’espressione aritmetica (x+1), valutata in uno stato s tale che s x = 3

Tino Cortesi Analisi e Verifica di Programmi 17

Semantica delle espressioni booleane

Tino Cortesi Analisi e Verifica di Programmi 18

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 Analisi e Verifica di Programmi 19

Comando sequenzialeLa 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 20

Comando condizionale

Tino Cortesi Analisi e Verifica di Programmi 21

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 Analisi e Verifica di Programmi 22

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 23

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 Analisi e Verifica di Programmi 24

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 Analisi e Verifica di Programmi 25

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?