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 » 12.Esercitazione in aula (sulla prima metà del corso)


Esercizio

Scrivere la semantica operazionale e denotazionale del seguente comando da aggiungere al linguaggio IMP:

Do b1 → c1, b2 → c2

dove b1 e b2 sono espressioni booleane e c1 e c2 sono comandi e con la seguente semantica intuitiva:
“ad ogni terazione del costrutto i comandi c_1 e c_2 vengono eseguiti (sequenzialmente) se le espressioni booleane associate valutano a vero. L’iterazione ed il singolo ciclo terminano non appena viene incontratta una espressione booleana che valuta a falso”

Equivalenza delle semantiche

  • Dimostriamo che per il comando dato vale la proprietà P(c)

(σ, σ’) 2 C«Do¬ , < Do, σ > ! σ’

  • Iniziamo con il verso “( ” e per questo verso usiamo una induzione sulle derivazioni.

Equivalenza del comando: “(“


Equivalenza del comando: “)”


Equivalenza per Com: while per “)”


Esercizio 1 – Soluzione


Esercizio 1 – Regole


Esercizio 4

Scrivere la semantica operazionale e denotazionale del seguente costrutto iterativo che viene aggiunto nel linguaggio IMP:

DO c1 check b1; c2 check b2 OD

con b1, b2 espressioni booleane e c1, c2 comandi.

  • Intuitivamente, ad ogni iterazione del costrutto i comandi c1 check b1 e c2 check b2 vengono eseguiti in modo sequenziale.
  • Il commando ci check bi ha il seguente effetto: sullo stato corrente viene eseguito il comando ci e la condizione bi viene valutata sullo stato ottenuto dall’esecuzione di ci; se la valutazione della condizione è “false”, l’effetto dell’esecuzione di ci viene annullato (abort di c1 check b1).
  • Se entrambi i comandi ci check bi provocano una azione di abort il ciclo viene interrotto.

Esercizio 4 – Soluzione (Sem.op.)

  • Sia C ´ DO c1 check b1; c2 check b2 OD.
  • Vogliamo definire la semantica operazionale (regole di derivazione) di C rispetto ad ogni stato σ 2 Σ (<C,σ>).
  • Per definire le regole di derivazione di , dobbiamo distinguere i seguenti casi
  • b1 e b2 sono valutate entrambe “false” dopo l’esecuzione di c1 e c2, rispettivamente. In questo caso, il ciclo si interrompe, vengono annullati entrambi i comandi c1 e c2 e la valutazione del comando C equivale a quella di uno “skip”
  1. Almeno una tra b1 e b2 è valutata “true”, dopo l’esecuzione di c1 e c2. In questo caso, il ciclo non si interrompe, e sarà eventualmente annullato il comando ci corrispondente a bi valutata “false”.
  2. La valutazione di C è data dalla valutazione del comando sullo stato derivato dall’esecuzione di uno dei comandi c1 e c2 (o eventualmente entrambi) .

Esercizio 4 – Soluzione (Regole)

Regole di derivazione per D ´ DO c1 check b1; c2 check b2 OD:


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