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 » 7.Semantica denotazionale di IMP


Introduzione alla VII lezione

  • Nella prima parte del corso abbiamo introdotto il linguaggio imperativo IMP.
  • Per questo linguaggio, abbiamo introdotto una semantica operazionale e abbiamo mostrato che questa semantica si basa su regole di derivazione. In particolare:
    • è legata alla sintassi;
    • interpreta i programmi come relazioni di transizione.
  • Sebbene relativamente semplice e molto efficiente per valutare certe proprietà di un linguaggio quali il determinismo, l’utilizzo di tali regole comporta alcune limitazioni:
    • mostra soltanto come possono essere utilizzati gli elementi di un linguaggio, ma non il oro significato intrinseco.
    • La dipendenza dalla sintassi rende difficile il confronto di programmi scritti in linguaggi di programmazione differenti.

Esempio


Un po’ di storia

  • Negli anni sessanta, Christopher Strachey e Dana Scott riuscirono a superare le limitazioni della semantica operazionale introducendo una semantica più astratta basata sull’utilizzo di funzioni semantiche (chiamate denotazioni) come modelli matematici di rappresentazione (del significato) dei programmi.
  • L’idea di base utilizzata in questa semantica (denotazionale) può essere mostrata con un esempio:
  • In IMP, due comandi c0 e c1 sono equivalenti (c0 » c1) se
      • 8σ,σ’ . <c0 σ’> ! σ’ , <c1 σ’> ! σ’
  • In modo equivalente, possiamo dire che c0 » c1 sse
      • {(σ,σ’ ) | <c0 σ’> ! σ’ } = {(σ,σ’ ) | <c1 σ’> ! σ’ }
  • Cioè sse c0 e c1 definiscono la stessa funzione parziale sugli stati. Dunque una valutazione di equivalenza tra linguaggi viene rimandata alla valutazione di equivalenza tra oggetti matematici.

Semantica denotazionale

  • L’obiettivo della semantica denotazionale è quello di esprimere il significato di un programma in termini di funzioni semantiche (funzioni matematiche ).
  • In pratica, ad ogni frase del linguaggio viene associata una denotazione (significato) come funzione delle denotazioni delle sue sottofrasi.
  • La semantica denotazionale cerca di catturare il significato interno di un programma piuttosto che la strategia di implementazione. Per questo motivo è più astratta di quella operazionale ed è indipendente dalla macchina su cui si lavora.

Semantica denotazionale di IMP

  • In generale, per definire la semantica di un oggetto di un linguaggio definito da una certa sintassi utilizzeremo la notazione « ¬ nel seguente modo:
      • «<sintassi> ¬ = denotazione di <sintassi>
  • dove le parentesi « ¬ sono chiamate parentesi semantiche e «<sintassi>¬ va letto come la “denotazione di <sintassi>”.
  • Sostanzialmente le parentesi « ¬ sono una funzione matematica.

Semantica operazionale di Aexp

  • Ricordiamo la sintassi delle espressioni aritmetiche Aexp di IMP
      • a ::= n | X | a0 + a1 | a0 – a1 | a0 – a1
  • La semantica denotazionale per a 2 Aexp è una funzione
      • A«a¬ : ∑ ! N o equivalentemente A : Aexp ! ∑ ! N
  • vedi figura
  • Si noti che le funzioni “∑ ! N ” sono rappresentate (in modo equivalente) in termini di insiemi di coppie “stato, numero” e che i simboli “+”, “-” e “*” nella parte sinistra delle uguaglianze sono simboli sintattici e nella parte destra sono operatori.

Esempi di valutazione di Aexp

  • Per qualsiasi stato σ, la semantica denotazionale di “3+5″ è:
      • A«3 + 5¬σ = A«3¬σ + A«5¬σ = 3+5 =8
  • dove A«a¬σ semplifica A«a¬(σ).
  • Sia σ lo stato in cui la locazione X vale “2″. La semantica denotazionale di “X*3″ è
      • A«X*3¬σ = A«X¬σ * A«3¬σ = σ(X)*3 =6
  • E se avessimo avuto anche la divisione (a0/a1) in Aexp, come può essere definita la semantica denotazionale per a0/a1 ?
  • Bisogna tener presente quando il denominatore è zero:
    • A«a0/a1¬σ è indefinito se A«a1¬σ = 0.
    • Altrimenti è il quoziente intero della divisione tra A«a0¬σ e A«a1¬σ

λ-calculus

  • Un modo alternativo di rappresentare funzioni è dato dalla notazione λ
  • In pratica, la notazione λx.e denota la funzione che mappa x in e.
  • Per esempio la funzione successione può esser scritta come
        • λx.x+1
  • Utilizzando questa notazione, è possibile riscrivere la semantica delle espressioni aritmetiche di IMP nel seguente modo:
    • A«n¬ = λσ.n
    • A«X¬ = λσ.σ(X)
    • A«a0 + a1¬ = {(σ, n) | σ 2 ∑ Æ n = A«a0¬σ + A«a1¬σ}
    • A«a0 – a1¬ = {(σ, n) | σ 2 ∑ Æ n = A«a0¬σ – A«a1¬σ}
    • A«a0 * a1¬ = {(σ, n) | σ 2 ∑ Æ n = A«a0¬σ * A«a1¬σ}

Intermezzo: Background del λ-calculus

  • Developed in 1930’s by Alonzo Church.
  • Subsequently studied (and still studied) by many people in logic and computer science.
  • Considered the “testbed” for procedural and functional languages.
    • Simple.
    • Powerful.
    • Easy to extend with features of interest.
  • “Whatever the next 700 languages turn out to be, they will surely be variants of lambda calculus.” (Landin ‘66)

Intermezzo: Alonzo Church

  • PhD from Princeton University, 1927
    • Advisor was Oswald Veblen who also advised R. L. Moore of UT Austin
  • Studied with David Hilbert, Paul Bernays & L.E.J. Brouwer in Germany
  • Many of his PhD students are “founding fathers” of theoretical computer science:
    • Stephen Kleene, 1934 (recursive function theory);
    • J. Barkley Rosser, 1934 (Church-Rosser theorem);
    • Alan Turing, 1938 (computational logic & computability);
    • Martin Davis, 1950 (logic & computability theory);
    • J. Hartley Rogers, 1952 (recursive function theory);
    • Michael Rabin, 1956 (probabilistic algorithms – Turing award);
    • Dana Scott, 1958 (prob. algorithms, domain theory – Turing award);
    • Raymond Smullyan, 1959 (logic, tableau proof, formal systems).

Intermezzo The λ-calculus in Computer Science

  • A formal notation, theory, and model of computation.
  • Church’s thesis: λ-calculus & Turing Machines describe the same set of objects, i.e., effectively computable functions:
    • equivalence was proved by Stephen Kleene.
  • Foundation for the functional style of programming:
    • Lisp, Scheme, ISWIM, ML, Miranda™, Haskell, …
  • Notation for Scott-Strachey denotational semantics.
  • It can be used to abstractly represent numbers, booleans, predicates, functions, variables, block scopes, expressions, ordered pairs, lists, records & recursion, ecc.

Denotazione di Bexp

  • Ricordiamo la sintassi delle espressioni booleane Bexp di IMP
      • b ::= true | false | a0=a1 | a0 · a1 | : b| b0 Æ b1 | b0 Ç b1
  • La semantica denotazionale per b 2 Bexp è una funzione
  • B«b¬ : ∑ ! {true, false}
  • La funzione semantica per le espressioni booleane è definita in termini delle operazioni logiche di congiunzione (Æ), disgiunzione (Ç) e negazione (:)
  • La denotazione di b 2 Bexp (semantica denotazionale A«b¬ per b) è una relazione tra stati e valori di verità, definita per induzione sulla struttura dell’espressione booleane nel modo seguente:

Denotazione di Bexp


Esempi di valutazione di Bexp

  • Per ogni stato σ, la semantica denotazionale di “true Ç false” è
  • B«true Ç false ¬λ = B«true¬λ Ç B«false¬λ = true Ç false = true
  • dove B«b¬λ semplifica B«b¬(λ).
  • Sia λ lo stato in cui la locazione X vale “2″ e Y vale “3″. La semantica denotazionale di “X+3 = Y+2″ è:
      • B«X+3 = Y+2 ¬λ = true perché A«X+3¬λ = 5 = A«Y+2¬λ

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


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}
  • Come si vede, il termine w compare in entrambi i lati dell’uguaglianza e dunque C«w¬ non ha una soluzione immediata.
  • Risolvere questa funzione equivale a calcolare un punto fisso.

Idea di valutazione con fixpoint

  • Si consideri la concatenazione del comando X:=0 e del comando w = while X· 10 do X:=X+1.
  • La denotazione di x:=0; w è C«x:=0; w¬σ = C«w¬σ ± C«x:=0¬σ.
  • Sappiamo che C«x:=0¬σ = {(σ, σ[0/X])}.
  • Per C«w¬σ occorrono 12 valutazioni di X·10 e 11 esecuzioni di X:=X+1.
  • Dopo la prima valutazione di X·10 (ed esecuzione di X:=X+1), la denotazione di w è quella di w valutato solo 10 volte, in combinazione con C«X:=X+1¬σ = {(σ, σ[σ(X)+1/X])}. Questo combinato con C«x:=0¬σ = {(σ, σ[0/X])} restituisce la denotazione di C«x:=0; w¬σ.
  • Iterando, C«x:=0; w¬σ è anche equivalente alla denotazione del while valutato 9 volte combinato alla funzione {(σ, σ[σ(X)+1/X])}, combinato a {(σ, σ[σ(X)+1/X])} e infine combinato a {(σ, σ[0/X])}.
  • Questo termina quando non dobbiamo più valutare X · 10, o meglio, quando ulteriori valutazioni non cambiano il risultato.
  • Dunque, C«x:=0; w¬σ = {(σ, σ[11/X])}. Generalizziamo questa idea.

Valutazione di while con fixpoint

  • 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

  • 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 σ e il comando c viene valutato {(σ,σ’)}, e b valutato “false” in σ’, cioè il while termina in una iterazione, allora possiamo raffinare C1«w¬ con C2«w¬ : ∑ → ∑, che oltre ad essere una funzione identità dove C1«w¬ è definita, associa a C2«w¬σ la funzione {(σ,σ’)}. Chiaramente C1«w¬ · C2«w¬.
  • Iterando il processo, per ogni k si può definire una funzione parziale Ck«w¬ : ∑ → ∑, definita su tutti gli stati su cui il while termina in al più k valutazioni di b (cioè k – 1 esecuzioni di c).
  • Dunque abbiamo una ω-catena C0«w¬ · C1«w¬ · … · Ck«w¬ · … e un odine parziale completo con ? = C0«w¬

Valutazione di while con fixpoint


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 true partendo da _, e false dopo k volte. 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.

Semantica Assiomatica

  • Per motivi di tempo, in questo corso si è deciso di non trattare la semantica assiomatica.
  • Axiomatic Semantics is an approach based on matematical logic to prove the correctness of computer programs.
  • An axiomatic semantics consists of:
    • a language for making assertions about programs.
    • Rules for establishing the assertions.
  • Some typical kinds of assertions:
    • this program terminates.
    • The variables x and y have the same value throughout the execution of the program whenever z is 0.
    • All array accesses are within array bounds.
  • Some typical languages of assertions:
    • first-order logic.
    • Other logics (e.g., temporal logic).

Applications of axiomatic semantics

  • Some application
    • Guidance in design and coding.
    • Proving the correctness of algorithms and hardware description (or finding bugs).
    • Documentation of programs and interfaces.
  • The project of defining and proving everything formally has not succeeded (at least not yet).
  • Dijkstra said: ” Program testing can be used to show the presence of bugs, but never to show their absence “.
  • Hoare said: “Thus the practice of proving programs would seem to lead to solution of three of the most pressing problems in software and programming, namely, reliability, documentation, and compatibility. However, program proving, certainly at present, will be difficult even for programmers of high caliber; and may be applicable only to quite simple program designs”.
  • 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