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