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