Aniello Murano » 4.Esercitazione sulla semantica operazionale di IMP e sulle tecniche di prova

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.

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 a₀^a₁ dove a0 e a1 sono elementi di Aexp. Dunque per Aexp avremo:
a ::= n | X | a₀ + a₁ | a₀ – a₁ | a₀x a₁ | a₀^ a₁.
Valutazione del nuovo operatore: vedi figura
dove n è uguale a n₀ elevato a n₁.

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 m₀ e conclusione <(y + y), σ> ! m=m₀+m₀. 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 m₀= m₀+m₀=m
- “←” L’inverso del discorso precedente.

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