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 » 4.Esercitazione sulla semantica operazionale di IMP e sulle tecniche di prova


Argomenti di Esercitazione

  • Seconda lezione: Sintassi e semantica operazionale del linguaggio imperativo IMP.
    • Utile per definire sintassi e semantica di nuovi operatori di un linguaggio.
    • Utile per provare l’equivalenza semantica di due elementi di un linguaggio.
  • Terza lezione: Tecniche di prova per induzione.
    • Utile per provare delle proprietà semantiche degli elementi di un linguaggio.

1. Definizione di un nuovo operatore

  • Supponiamo di voler estendere le espressioni aritmetiche di IMP includendo un nuovo operatore “^” con il significato di elevamento a potenza.
  • La sintassi di Aexp di IMP verrà estesa includendo anche a0^a1 dove a0 e a1 sono elementi di Aexp. Dunque per Aexp avremo:
  • a ::= n | X | a0 + a1 | a0 – a1 | a0 x a1 | a0^ a1.
  • Valutazione del nuovo operatore: vedi figura
  • dove n è uguale a n0 elevato a n1.

2. Equivalenza semantica di due espressioni

  • Utilizzando le regole di valutazione introdotte per le espressioni aritmetiche è possibile mostrare l’equivalenza di due espressioni.
  • Per esempio, è possibile mostrare formalmente che
  • ” y + y ” equivale all’espressione ” y * 2 “, cioè (y + y) » (y * 2)
  • Formalmente, si vuole provare che
    • <(y + y),σ> ! m iff <(y * 2),σ> ! m, per qualsiasi σ e m
    • “→” se <(y + y), σ> ! m allora deve esistere un albero di derivazione con y valutato m0 e conclusione <(y + y), σ> ! m=m0+m0. Dunque m è due volte la valutazione di y. Allora possiamo definire un albero di derivazione per <(y * 2), σ> con conclusione <(y * 2), σ> ! m’=2 x m0= m0+m0=m
    • “←” L’inverso del discorso precedente.

2. Equivalenza semantica di due comandi


3. →Bexp è deterministica


Esercizio

  • Provare che →Bexp è totale utilizzando il metodo di induzione strutturale
  • Definire la semantica denotazionale del seguente comandi:
  • Do c while b (con il significato classico in linguaggio C)
  • Do c while b after c’ (con la variante al caso precedente che b viene valutato dopo aver eseguito c’ sullo stato ottenuto dall’esecuzione di c. Si noti che c’ viene eseguito solo per valutare b, ma nell’itgerazione c’ non ha effetto.)
  • save (con il significato di fare un mirror di tutte le variavibli: per ogni variabile x, si usa x’ e si esegue x’:=x.
  • restore (con il significato di eseguire per ogni variabile x il comando x = x’)
  • Provare la seguente equivalenza: 

do c1 while b after c2
equiv.
c1; save; c2; (while b do (restore; c1; save; c2)); restore

  • 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