Aniello Murano » 2.Semantica Operazionale del linguaggio imperativo IMP

Regole di costruzione

• Si consideri la regola

R = if a_o є Aexp and a1  є Aexp then a₀ + a₁ є Aexp

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

Albero di derivazione

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

Semantica operazionale di Aexp III

• Addizione

• dove n è la somma di n₁ e n₂

• Esempio:
  • <4 + x, {(x,3)}}> → 7
  • Questo perché: <4, {(x,3)}}> → 4  e  <x, {(x,3)}}> → 3

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 σ₀
• Init una locazione tale che σ₀(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 a₁ e a₂. Diciamo che a₁ ~ a₂ se e solo se a₂ e a₂ si valutano nello stesso valore in qualsiasi stato.

Formalmente, a₁ ~ a₂ 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 II

• Confronto (vedi figura)
  

dove t è vero se n₁ è uguale a n₂ e false altrimenti.

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

Semantica operazionale di Bexp IV

• Caso AND (OR è speculare)

• Ci sono solo tre casi. Come mai?
  • Risposta: Nel primo caso, una volta valutato b₀ come false, non è più necessario valutare b₁.
  • 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 σ₀) associ valore 0 ad ogni locazione (“variabile”). In pratica σ₀(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.

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

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)

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 c₁ e c₂ di Com. Diciamo che c₁ ~ c₂ se e solo se la valutazione di c1 e c2 porta allo stesso stato quando sono valutati in un medesimo stato

Formalmente, c₁ ~ c₂ 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.