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 » 8.Semantica denotazionale del comando while di IMP


Denotazione di Com

  • Ricordiamo la sintassi dei comandi Com di IMP

c ::= skip | X:=a | c0;c1 | if b then c0 else c1 | while b do c

  • La semantica denotazionale per c 2 Com è una funzione

C«c¬ : ∑ → ∑

  • La denotazione di c 2 Com (semantica denotazionale C«c¬ per c) è una relazione tra stati, definita per induzione sulla struttura dei comandi.
  • Si noti che la funzione di valutazione è parziale C«c¬ : ∑ → ∑ in quanto su alcuni comandi la funzione può non essere definita (per esempio sui loop infiniti)

Denotazione di Com II

  • C«skip¬ = {(σ, σ) | σ 2 ∑}
  • C«X:=a ¬ = {(σ, σ[n/X]) | σ 2 ∑ & A«a0¬σ = n }
  • C«c0;c1¬ = C«c1¬ ± C«c0¬ (si noti l’inversione in accordo alla regola di composizione)
  • C«if b then c0 else c1¬ = {(σ, σ’) | B«b¬σ = true & (σ, σ’) 2 C«c0¬} [
    {(σ, σ’) | B«b¬σ = false & (σ, σ’) 2 C«c1¬}
  • Particolarmente difficile è invece la valutazione del comando while per il quale è necessario utilizzare i concetti matematici del punto fisso introdotti nella lezione precedente.

Denotazione del while

  • Dalla semantica operazionale (II lezione) abbiamo osservato che esiste la seguente equivalenza:
  • Sia w ´ while b do c allora: w » if b then c;w else skip
  • Possiamo allora scriver la semantica del comando while utilizzando le regole precedenti nel seguente modo:
  • C«w¬ = C«if b then c;w else skip¬ =

{(σ, σ’) | B«b¬σ = true & (σ, σ’) 2 C«w¬ ± C«c¬} [
{(σ, σ’) | B«b¬σ = false} =
{(σ, σ’) | 9 σ”. B«b¬σ = true & (σ, σ”) 2 C«c¬ & (σ”, σ’) 2 C«w¬} [
{(σ, σ’) | B«b¬σ = false}

  • Come si vede, il termine w compare in entrambi i lati dell’uguaglianza (equazione ricorsiva). Dunque C«w¬ non ha una soluzione immediata.
  • Risolvere questa funzione equivale a calcolare un punto fisso di una funzione C«w¬=f(C«w¬).

Alcune osservazioni su f(C[w])

  • C«w¬ = C«if b then c;w else skip¬ =
    {(σ, σ’) | 9 σ”. B«b¬σ = true & (σ, σ”) 2 C«c¬ & (σ”, σ’) 2 C«w¬}
    [ {(σ, σ) | B«b¬σ = false}
  • Risolvere questa equazione equivale a calcolare un punto fisso di una funzione C«w¬=f(C«w¬).
  • C«w¬ è una unzione parziale C«w¬: ∑ → ∑.
  • C«c¬ è una unzione parziale C«c¬: ∑ → ∑.
  • Dunque, f è ottenuta eseguendo prima C«c¬ e poi C«w¬. Per cui, f è una funzione f: (∑ → ∑) ! (∑ → ∑). Questa osservazione chiarirà il formalismo utilizzato nelle prossime diapositive.

Idea di valutazione con fixpoint


Valutazione di while con fixpoint II

  • Nella lezione precedente abbiamo parlato di ordinamento parziale tra funzioni:
  • date due funzioni parziali I,J : ∑ → ∑, con I · J indichiamo che J raffina I o che J estende I
  • Tornando alla funzione parziale di while, si potrebbe pensare che ad ogni iterazione di un while si può raffinare la conoscenza della sua valutazione
  • Caso base: prima che b sia valutata, la conoscenza su C«w¬ è
  • C0«w¬ := ? : ∑ → ∑, che denota la funzione non definita in nessun stato. Quindi C0«w¬ corrisponde a nessuna informazione.

Valutazione di while con fixpoint III

  • Si supponga adesso di valutare b “false” in uno stato σ. Dunque la denotazione del while ritorna {(σ,σ)},
  • Questo ci permette di raffinare la nostra conoscenza del while da C0«w¬ ad una nuova funzione parziale C1«w¬ : ∑ → ∑, che è una funzione identità sugli stati σ in cui b è valutata “false”
  • Se invece b è valutato “true” in σ, il comando c viene valutato in σ. Supponendo che la sua valutazione sia {(σ,σ’)}, il risultato del while è rimandato alla valutazione del while stesso su σ’.
  • Se conosciamo anche la valutazione di b in σ’ possiamo raffinare la nostra conoscenza sul valore del while in C2«w ¬. In pratica se b è valutato “false” in σ’, il while termina, altrimenti si valuta c in σ’ e si itera con la valutazione del while. Chiaramente C1«w¬ · C2«w¬.
  • Iterando il processo, abbiamo una σ-catena C0«w¬ · C1«w¬ · … · Ck«w¬ · … di raffinamenti e un ordine parziale dove ? = C0«w¬

Valutazione di while con fixpoint IV


Osservazioni sulla definizione di f

  • Osserviamo ancora come la definizione di f tramite le regole
      • ; ! (σ,σ) if B«b¬σ = false
      • (σ”,σ’) ! (σ,σ’) if B«b¬σ = true & C«c¬σ = σ”
    • permette di valutare ricorsivamente il comando iterativo w in σ.
  • Consideriamo i seguenti scenari di denotazione di b:
  • b denotata false in σ, allora la denotazione di w è (σ,σ)
  • b vale true in σ, e false in σ”. Siccome al secondo ciclo si utilizza la prima regola di f, risulta (σ”,σ’) = (C«c¬σ, C«c¬σ). Dunque la denotazione di w è (σ, C«c¬σ), e corrisponde ad f applicata ad f al passo ricorsivo precedente cioè su: b valutata false in C«c¬σ”.
  • b vale k volte “true” partendo da σ, e false la k+1-ma volta. Allora si applica k volte la seconda regola di f e poi una sola volta la prima. Dunque la valutazione di w in questo caso è data dalla funzione f applicata su f al passo ricorsivo precedente cioè su: b valutata k-1 true partendo da σ, e poi false dopo k-1 volte.

Ultima osservazione su f

Nel libro di testo, la funzione f è riferita come “operatore ⌈”. In seguito anche noi utilizzeremo indistintamente f e ⌈, riferendoci allo stesso operatore definito in questa lezione.

Denotazione del comando while


Fixpoint per C[w]

  • La denotazione di w è data dalla soluzione della funzione ricorsiva f(C«w¬) = C«w¬. Questo equivale a calcolare il suo fixpoint
  • Siano f0(?) = ? = C0«w¬ e f1(?) = f(f0(?)) = C1«w¬, allora possiamo definire induttivamente
  • fk(?) = f(fk-1(?)) = Ck«w¬ come il risultato di k composizioni di f.
  • La funzione f è continua e dunque, esiste il fixpoint di f è corrisponde al “least upper bound” della catena.
  • Un modo alternativo per legare la valutazione del while “least upper bound” della catena fi(?) è dato dal theorema di Tarski

Teorema di Tarski


Ricapitolando

  • Se ho un comando iterativo la cui denotazione è data una funzione ricorsiva di cui non so a priori il numero delle iterazioni, definisco un operatore di punto fisso, cioè una funzione (ricorsiva) il cui punto fisso è proprio la denotazione del comando.
  • Provo dunque a definire l’operatore tramite un insieme di regole
  • Se queste regole hanno premesse finite e positive, allora posso applicare il teorema di Tarski e concludere che la semantica del comando è il l.u.b. della catena ottenuta applicando iterativa-mente le regole che definiscono l’operatore.

Esercizio 1 – prima parte


Esercizio 1 – seconda parte


Esercizio per casa

Definire la semantica denotazionale di

while x > 0 do y = y*2; x:=x-1

con la semantica intuitiva di calcolare y*2x per x ¸ 0.

  • 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