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 » 10.Esercitazione sulle semantiche operazionale e denotazionale di IMP


Esercizio 1

  • Scrivere la semantica operazionale del seguente comando:

while b1 do c exit b2

  • 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 b2 è soddisfatta. Se b2 è soddisfatta, il ciclo viene interrotto”.

Esercizio 1 – Soluzione

  • Sia w ´ while b1 do c exit b2
  • 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. b2 è 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. b2 è 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


  • 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