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