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
 
I corsi di Scienze Matematiche Fisiche e Naturali
 
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