Aniello Murano » 10.Esercitazione sulle semantiche operazionale e denotazionale di IMP

Esercizio 1

• Scrivere la semantica operazionale del seguente comando:

while b₁ do c exit b₂

• con la seguente semantica intuitiva:
  “la semantica standard del costrutto while di IMP viene arricchita controllando alla fine di ogni iterazione di c se la condizione b₂ è soddisfatta. Se b₂ è soddisfatta, il ciclo viene interrotto”.

Esercizio 1 – Soluzione

• Sia w ´ while b₁ do c exit b₂

• Vogliamo definire la semantica operazionale (regole di derivazione) di w rispetto ad ogni stato σ 2 Σ<w,σ>).
• Per definire le regole di derivazione di <w,σ>, dobbiamo distinguere i seguenti casi

1. b1 è valutata “false” in σ, secondo le regole della semantica operazionale di IMP. Allora il comando c non viene eseguito e il ciclo viene interrotto. Dunque, viene derivata in σ.
2. b1 è valutata “true” in σ, secondo le regole della semantica operazionale di IMP. Allora il comando c viene eseguito. Sia σ’ lo stato raggiunto dopo l’esecuzione di c, dato dalle valutazione di , secondo le regole della semantica operazionale di IMP. Allora dobbiamo distinguere i seguenti due casi:

1. b₂ è valutata “true” in σ, secondo le regole della semantica operazionale di IMP. Allora il ciclo viene interrotto dopo l’esecuzione di c. Dunque, viene derivata in σ’.
2. b₂ è valutata “false” in σ, secondo le regole della semantica operazionale di IMP. Allora viene eseguito nuovamente il ciclo a partire dallo stato σ. Dunque, la valutazione di w, in σ dipende dalla valutazione di w in σ’

Esercizio 1 – Regole

Esercizio 2

Esercizio 2 – Soluzione

• Per dimostrare l’equivalenza di w ´ while b do c exit b con if ´ if b then c else skip, in qualsiasi stato σ, occorre distinguere i seguenti casi:
• b è valutata “false” in σ. In questo caso w e if sono valutati σ.
• b è valutata “true” in σ. Allora occorre eseguire c nello stato attuale σ. Sia σ’ lo stato raggiunto dopo l’esecuzione di c in σ. A questo punto bisogna distinguere le seguenti possibilità:
  • b è valutata “true” in σ’. Allora il ciclo viene interrotto dopo l’esecuzione di c. Dunque, viene derivata in σ’. Si noti che nel comando if, comunque sia valutato b in σ’, esso viene interrotto dopo l’esecuzione di c e dunque in questo caso <w,σ> è valutato σ’ sse è valutato σ’.
  • b è valutata “false” in σ’. Allora dopo il comando c viene eseguito nuovamente il comando w nello stato σ’. Ma adesso già sappiamo che b è valutata “false” in σ’, e dunque il ciclo while viene interrotto senza eseguire ulteriormente c, proprio come nel comando if. Dunque, anche in questo caso è valutato <if,σ>’ sse è valutato σ’.

Esercizio 3

Esercizio 3 – Soluzione

Esercizio 4

Esercizio 4 – Soluzione (Sem.op.)

Esercizio 4 – Soluzione (Regole)

Esercizio 4 – Soluzione (Sem.den.)

Esercizio 4 – Soluzione (Sem.den.)

Esercizio 5