Vai alla Home Page About me Courseware Federica Living Library Federica Federica Podstudio Virtual Campus 3D Le Miniguide all'orientamento Gli eBook di Federica La Corte in Rete
 
I corsi di Scienze Matematiche Fisiche e Naturali
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

Aniello Murano » 2.Semantica Operazionale del linguaggio imperativo IMP


Introduzione

  • Il linguaggio IMP è detto imperativo perché l’esecuzione di un programma comporta l’esecuzione esplicito di comandi che modificano lo stato.
  • IMP è descritto da regole che specificano come valutare le sue espressioni e come eseguire i suoi comandi.
  • Tali regole forniscono una semantica operazionale di IMP.
  • Sintassi di IMP


    Grammatica BNF (Bakus-Naur Form)

    a ::= n | X | a0 + a1| a0 – a1| a0 x a1

    • La BNF altro non e’ che un insieme di regole per costruire un linguaggio dove:
      • “::=” significa “puo’ essere”
      • “|” significa “oppure”
      • “a” e’ una metavariabile
  • Un linguiaggio e’ chiaramente un insieme di espressioni:
    • Aexp e’ l’insieme delle espressioni aritmetiche
    • Chiaramente la BNF e’ una semplificazione…

    Regole di costruzione

    • Si consideri la regola

    R = if ao є Aexp and a1  є Aexp then a0 + a1 є Aexp

    • La regola R può essere scritta in modo rigoroso tramite un regola di inferenza nel modo indicato in figura.

    Due livelli


    Regole per generare espressioni


    Tutto questo è sufficiente?

    • Gli assiomi con le regole di inferenza generano l’insieme Aexp.
      • L’insieme cioè più piccolo chiuso rispetto all’applicazione di tutte le regole.
  • L’insieme è infinito.
    • È ben definito o genera paradossi?
    • Per esempio, si possono avere insiemi che contengono se stessi?
    • La risposta a queste domande per Aexp è semplice, come anche per Bexp.
    • Per Com occorrono argomentazioni complesse come vedremo in seguito.
    • Cominciamo con un esempio….

    Albero di derivazione

    Mostriamo adesso come derivare un’espressione tramite un albero di derivazione (che rappresenta una forma di prova).


    Semantica operazionale

    • Come si può definire la semantica di un programma?
      Si consideri per esempio il seguente frammento di codice:

    while x ≠ y do
    if x < y then
    y:=y-x
    else
    x:=x-y

    • Informalmente
      • Se conosciamo il valore di tutte le variabili (locazioni) si possono sicuramente valutare le espressioni di Aexp e Bexp.
      • I comandi possono portare a cambiamenti nelle variabili (tramite l’operatore assegnazione := ) oppure direzionare il flusso di controllo (tramite per esempio il comando if).
    • Formalizziamo tutto questo….

    Stati

    • Uno stato altro non è che una funzione da locazioni a valori naturali:
      • σ : Σ= Loc -> N
      • σ(X) rappresenta il valore della locazione nello stato σ.
    • Noi consideriamo solo stati finiti
    • Esempio:
      • Loc = {x,y,z,…}
      • σ = {(x,2), (y,3)}
    • Dunque:
      • σ(x) =2
      • σ(y) =3
      • σ(z) = indefinita

    Valutazione delle espressioni

    • Aexp si valuta in interi, rispetto ad un dato stato.
    • Con <a, σ> denotiamo una espressione aritmetica a che deve essere valutata nello stato σ.
      • La coppia <a, σ> è una configurazione
    • Per dire che l’espressione a valutata nello stato σ si riduce a n usiamo:

    <a, σ> → n

    Il simbolo “” è una relazione di transizione.

    • Specifica il comportamento di una macchina astratta:
      • quando forniamo in input alla macchina una coppia espressione (a) stato (σ), la macchina da in output il valore n.
      • Questo può essere pensato come una transizione da una configurazione a un valore finale.

    Terminologia

    • Il simbolo è una relazione, sottoinsieme di

    Aexp×Σ×N

    • Si ricordi che x R y significa (x,y) є R.
    • La scelta del simbolo è arbitraria, infatti in alcuni testi è possibile trovare simboli differenti.
    • Relazione tra sintassi e semantica
      • Aexp è un dominio sintattico, N invece è un dominio semantico
    • Nelle prossime slide vediamo la definizione di questa relazione per ogni singolo elemento di Aexp che ricordiamo essere definito dalla seguente sintassi:

    a ::= n | X | a0 + a1| a0 – a1| a0 x a1


    Semantica operazionale di Aexp I

    • Numeri
      • <n, σ> → n
    • Esempi
      • <2, Ø> 2
      • <2, σ > 2   dove σ = {(x,5)}
      • <2, σ > 2 per qualsiasi σ

    Semantica operazionale di Aexp II

    • Locazioni
      • <X, σ> σ(X)
    • Esempi
      • <x, {(x,3)}> 3
      • <y, {(x,3), (x,4)}> 4
      • <z, {…(z,n)…}> n
    • Cosa succede nel caso < x,  Ø>
      • la relazione non contiene nessuna tripla della forma < x,  Ø, n>

    Semantica operazionale di Aexp III

    • Addizione
    • dove n è la somma di n1 e n2
    • Esempio:
      • <4 + x, {(x,3)}}> 7
      • Questo perché: <4, {(x,3)}}> 4  e  <x, {(x,3)}}> 3

    Semantica operazionale di Aexp IV


    Interpretazione delle regole

    • Ogni regola di valutazione ha una premessa (scritta sopra la linea) e una conclusione (scritta sotto la linea).
    • Siccome le regole specificano il significato delle espressioni in modo operazionale, si dice che esse definiscono una semantica operazionale di tali espressioni.
    • Alcune regole non hanno premesse. Queste regole, vengono anche chiamate assiomi come la regola indicata in figura.


    Albero di derivazione

    • Sia a ≡ (Init + 5 ) + (7 + 9) nello stato σ0
    • Init una locazione tale che σ0(init)=0

    • Tale struttura (indicata in figura) viene detta albero di derivazione.
    • La conclusione della derivazione si chiama derivata.
    • Si noti come le regole forniscono anche un algoritmo per la valutazione di espressioni aritmetiche basato sulla ricerca di un albero di derivazione.


    Equivalenza in Aexp

    • Date due espressioni di Aexp a1 e a2. Diciamo che a1 ~ a2 se e solo se a2 e a2 si valutano nello stesso valore in qualsiasi stato.

    Formalmente, a1 ~ a2 se e solo se (vedi figura)


    Intermissione

    • Riassumendo
      • Abbiamo definito la valutazione di espressioni aritmetiche di Aexp.
      • Abbiamo definito una relazione di transizione che lega la sintassi astratta di espressioni di Aexp a valori naturali.
    • Adesso estendiamo questi concetti a Bexp
      • Si ricordi che Bexp è definita dalla seguenti regole (vedi figura).


    Semantica operazionale di Bexp I

    • true e false
      • <true, σ> true
      • <false, σ> false

    • Si noti che il true sulla sinistra delle regole di derivazioni è sintattico mentre quello sulla destra è semantico e denota l’elemento T dell’insieme dei valori di verità.

    Semantica operazionale di Bexp II

    • Confronto (vedi figura)

    dove t è vero se n1 è uguale a n2 e false altrimenti.

    • Lo stesso ragionamento si estende facilmente ad “a1 ≤ a2” dove si possono usare le stesse premesse usate per l’uguaglianza.
      • Di fatti, <a1 ≤ a2, σ>  t, dove t è true se n1 è minore o uguale a n2 e false altrimenti.

    Semantica operazionale di Bexp III

    Negazione

    Negazione


    Semantica operazionale di Bexp IV

    • Caso AND (OR è speculare)
    • Ci sono solo tre casi. Come mai?
      • Risposta: Nel primo caso, una volta valutato b0 come false, non è più necessario valutare b1.
      • Si ricordi che, nelle regole di inferenza, una espressione non valutata si considera in modo che possa assumere qualsiasi valore.


    Intermissione

    • Riassumendo:
    • Abbiamo definito la valutazione di espressioni aritmetiche e booleane tramite relazioni di transizioni che legano la sintassi astratta delle espressioni al loro significato.
    • In totale, abbiamo bisogno di tre differenti relazioni di transizioni (vedi figura).
    • Ma noi le utilizziamo senza la sottoscrittura in quanto l’insieme sintattico a cui la relazione si riferisce sarà chiaro dal contesto.
    • Vediamo adesso la valutazione dei comandi….


    Comandi

    • Valutazione: Il ruolo dei programmi (e quindi dei comandi) è quello di essere eseguiti per cambiare lo stato.
    • Quando si esegue un programma IMP, sia assume che lo stato (iniziale σ0) associ valore 0 ad ogni locazione (“variabile”). In pratica σ0(X)=0. Successivamente l’esecuzione può terminare in uno stato finale oppure divergere.
    • <c, σ> denota una configurazione di comando e denota la possibilità di eseguire il comando c a partire dallo stato σ.

    • La valutazione di un comando è formalmente definita da una funzione da un comando e uno stato ad un nuovo stato.

    <c, σ> → σ’


    Semantica Operazionale di Com I

    • Skip (vedi figura 1)
    • Assegnamento (vedi figura 2)
      • dove ¾’ è ¾ aggiornato ponendo X uguale a n.
    • Per esempio, < X:=5, σ > → σ’, indica che lo stato σ’ si ottiene dallo stato σ, aggiornandolo in modo che la locazione X contenga il valore 5.
    • Per meglio esprimere la semantica di questo comando conviene usare una notazione per l’aggiornamento delle variabili.
    Figura 1

    Figura 1

    Figura 2

    Figura 2


    Semantica Operazionale di Com II

    • Scriveremo allora che σ ‘ è σ aggiornato σ ‘ è σ aggiornato con X che assume il valore n nel seguente modo
      • σ ‘ = σ [n/X]
    • In generale, la nuova notazione funziona come indicato in figura 1.
    • Con questa nuova notazione, la regola per l’assegnamento si può scrivere nel modo indicato in figura 2.
    • Per esempio, <X:=5, σ > → σ  [5/X].
    Figura 1

    Figura 1

    Figura 2

    Figura 2


    Osservazione

    • Cosa possiamo osservare dalla regola di assegnamento appena introdotta (vedi figura)
      • a è valutata prima che l’assegnamento venga realizzato.
      • Non ci sono effetti collaterali: l’unica cosa che cambia in memoria è il valore di X dopo che a è stata valutata e il suo valore è assegnato a X.
      • Non è possibile memorizzare valori booleani nelle variabili

    Semantica Operazonale di Com III

    • Sequenza (vedi figura 1)
    • L’ordine di valutazione è definito dall’uso della memoria (vedi figura 2)
    Figura 1

    Figura 1

    Figura 2

    Figura 2


    Semantica Operazionale di Com IV

    • Condizionale (vedi figura 1)
    • La valutazione dell’espressione booleana determina quale diramazione del comando if verrà eseguita.

    Semantica Operazonale di Com V

    • Ciclo while (vedi figura 1)
    • La valutazione è dunque definita in termini di se stessa. In questo caso è necessario assicurare che questo abbia senso!

    Equivalenza in Com

    • Dati due comandi c1 e c2 di Com. Diciamo che c1 ~ c2 se e solo se la valutazione di c1 e c2 porta allo stesso stato quando sono valutati in un medesimo stato

    Formalmente, c1 ~ c2 se e solo se (vedi figura).


    Esercizio

    • Si mostri che w ~w’  dove
      • w ≡ while b do c
      • w’ ≡ if b then c; w else skip

    Nota: ≡ sta per sintatticamente equivalente
    Più formalmente, si provi quanto indicato in figura.


    • Contenuti protetti da Creative Commons
    • Feed RSS
    • Condividi su FriendFeed
    • Condividi su Facebook
    • Segnala su Twitter
    • Condividi su LinkedIn
    Progetto "Campus Virtuale" dell'Università degli Studi di Napoli Federico II, realizzato con il cofinanziamento dell'Unione europea. Asse V - Società dell'informazione - Obiettivo Operativo 5.1 e-Government ed e-Inclusion