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 » 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