Semantik von Programmiersprachen

Semantik = Bedeutung

statisch (kann zur Übersetzungszeit geprüft werden)
Beispiele:
- Typ-Korrektheit von Ausdrücken,
- Bedeutung (Bindung) von Bezeichnern
Hilfsmittel: Attributgrammatiken
dynamisch (beschreibt Ausführung des Programms)
operational, axiomatisch, denotational

Attribut: Annotation an Knoten des Syntaxbaums.
A : Knotenmenge→Attributwerte (Bsp: $\mathbb {N}$ )
Attributgrammatik besteht aus:
- kontextfreier Grammatik G (Bsp: {S→e | mSS} )
- für jeden Knotentyp (Terminal + Regel)
  eine Menge (Relation) von erlaubten Attribut-Tupeln (A(X₀), A(X₁),…, A(X_n))
  für Knoten X₀ mit Kindern [X₁,…, X_n]
  
  S→mSS , A(X₀) + A(X₃) = A(X₂) ;
  S→e , A(X₀) = A(X₁) ;
  Terminale: A(e) = 1, A(m) = 0

ein Ableitungsbaum mit Annotationen ist
korrekt bezüglich einer Attributgrammatik, wenn

zur zugrundeliegenden CF-Grammatik paßt
in jedem Knoten das Attribut-Tupel (von Knoten und Kindern) zur erlaubten Tupelmenge gehört

Plan:

Baum beschreibt Syntax, Attribute beschreiben Semantik

Ursprung: Donald Knuth: Semantics of Context-Free Languages, (Math. Systems Theory 2, 1968)

technische Schwierigkeit: Attributwerte effizient bestimmen. (beachte: (zirkuläre) Abhängigkeiten)

The Art Of Computer Programming (1968, ...)
(Band 3: Sortieren und Suchen)
TEX, Metafont, Literate Programming (1983, ...)
(Leslie Lamport: L^ATEX)
Attribut-Grammatiken
die Bezeichnung „NP-vollständig``
...

http://www-cs-faculty.stanford.edu/~uno/

synthetisiert:
hängt nur von Attributwerten in Kindknoten ab
ererbt (inherited)
hängt nur von Attributwerten in Elternknoten und (linken) Geschwisterknoten ab

Wenn Abhängigkeiten bekannt sind, kann man Attributwerte durch Werkzeuge bestimmen lassen.

Auswertung arithmetischer Ausdrücke (dynamisch)
Bestimmung des abstrakten Syntaxbaumes
Typprüfung (statisch)
Kompilation (für Kellermaschine) (statisch)

konkreter Syntaxbaum = der Ableitungsbaum
abstrakter Syntaxbaum = wesentliche Teile des konkreten Baumes

unwesentlich sind z. B. die Knoten, die zu Hilfsvariablen der Grammatik gehören.

abstrakter Syntaxbaum kann als synthetisiertes Attribut konstruiert werden.

E -> E + P  ;  E.abs = new Plus(E.abs, P.abs)
E -> P      ;  E.abs = P.abs

...bei geschachtelten Funktionsaufrufen

Funktion f hat Typ A→B
Ausdruck X hat Typ A
dann hat Ausdruck f (X) den Typ B

Beispiel

String x = "foo"; String y = "bar";

Boolean.toString (x.length() < y.length()));

(Curry-Howard-Isomorphie)

SableCC: http://sablecc.org/
SableCC is a parser generator for building compilers, interpreters ..., strictly-typed abstract syntax trees and tree walkers

Syntax einer Regel

linke-seite { -> attribut-typ } 
   = { zweig-name } rechte-seite { ->  attribut-wert }

Quelltexte: git clone git://dfa.imn.htwk-leipzig.de/ws13-code/pps.git
Benutzung: cd pps/rechner ; make ; make test ; make clean
(dafür muß sablecc gefunden werden, also /usr/local/waldmann/bin im PATH sein)
Struktur:
- rechner.grammar enthält Attributgrammatik, diese beschreibt die Konstruktion des abstrakten Syntaxbaumes (AST) aus dem Ableitungsbaum (konkreten Syntaxbaum)
- Eval.java enthält Besucherobjekt, dieses beschreibt die Attributierung der AST-Knoten durch Zahlen
- Hauptprogramm in Interpreter.java
- bauen, testen, aufräumen: siehe Makefile
- generierte Dateien in rechner/*
Aufgaben:
Multiplikation, Subtraktion, Klammern, Potenzen

Kommentar: in Java fehlen: algebraische Datentypen, Pattern Matching, Funktionen höherer Ordnung. Deswegen muß SableCC das simulieren -- das sieht nicht schön aus. Die „richtige`` Lösung sehen Sie später im Compilerbau.

Abstrakter Syntaxbaum, Interpreter: http://www.imn.htwk-leipzig.de/~waldmann/edu/ws11/cb/folien/main/node12.html, Kombinator-Parser: http://www.imn.htwk-leipzig.de/~waldmann/edu/ws11/cb/folien/main/node70.html

operational:
beschreibt Wirkung von Anweisungen durch Änderung des Programmzustandes
denotational:
ordnet jedem (Teil-)Programm einen Wert zu, Bsp: eine Funktion (höherer Ordnung).
Beweis von Programmeigenschaften durch Term-Umformungen
axiomatisch (Bsp: Hoare-Kalkül):
enthält Schlußregeln, um Aussagen über Programme zu beweisen

arithmetischer Ausdruck ⇒ Programm für Kellermaschine

3*x + 1 ⇒ push 3, push x, mal, push 1, plus

Code für Konstante/Variable c : push c;
Code für Ausdruck xoy : code(x); code(y); o;
Ausführung eines binären Operators o :
x <- pop; y <- pop; push (x o y);

Der erzeugte Code ist synthetisiertes Attribut!

Beispiele: Java-Bytecode (javac, javap),
CIL (gmcs, monodis)

Bemerkung: soweit scheint alles trivial--interessant wird es bei Teilausdrücken mit Nebenwirkungen, Bsp. x++ - --x;

Schleife

while (B) A

wird übersetzt in Sprungbefehle

   if (B) ...

(vervollständige!)

Aufgabe: übersetze for(A; B; C) D in while!

Beispiele

jedes (nebenwirkungsfreie) Unterprogramm ist eine Funktion von Argument nach Resultat
jede Anweisung ist eine Funktion von Speicherzustand nach Speicherzustand

Vorteile denotationaler Semantik:

Bedeutung eines Programmes = mathematisches Objekt
durch Term beschreiben, durch äquivalente Umformungen verarbeiten (equational reasoning)

Vorteil deklarativer Programierung:

Programmiersprache ist Beschreibungssprache

jeder arithmetische Ausdruck (aus Konstanten und Operatoren)
beschreibt eine Zahl
jeder aussagenlogische Ausdruck (aus Variablen und Operatoren)
beschreibt eine Funktion (von Variablenbelegung nach Wahrheitswert)
jeder reguläre Ausdruck
beschreibt eine formale Sprache
jedes rekursive definierte Unterprogramm
beschreibt eine Funktion (?)

Unterprogramme definiert durch Gleichungssysteme.

Sind diese immer lösbar? (überhaupt? eindeutig?)

Geben Sie geschlossenen arithmetischen Ausdruck für:

f (x) = if x > 52 
        then x - 11 
        else f (f (x + 12))

t (x, y, z) = 
  if x <= y then z + 1 
  else t ( t (x-1, y, z) 
         , t (y-1, z, x) 
         , t (z-1, x, y) )

Notation für Aussagen über Programmzustände:

{ V } A { N }

für jeden Zustand s , in dem Vorbedingung V gilt:
wenn Anweisung A ausgeführt wird,
und Zustand t erreicht wird, dann gilt dort Nachbedingung N

Beispiel:

{ x >= 5 } y := x + 3 { y >= 7 }

Gültigkeit solcher Aussagen kann man

beweisen (mit Hoare-Kalkül)
prüfen (testen)

Bertrand Meyer, http://www.eiffel.com/

class Stack [G]     feature 
    count : INTEGER
    item : G is require not empty do ... end
    empty : BOOLEAN is do .. end
    full  : BOOLEAN is do .. end
    put (x: G) is
       require not full do ...
       ensure not empty
              item = x
              count = old count + 1

Beispiel sinngemäß aus: B. Meyer: Object Oriented Software Construction, Prentice Hall 1997

Kalkül: für jede Anweisung ein Axiom, das die schwächste Vorbedingung (weakest precondition) beschreibt.

Beispiele

{ N[x/E] } x := E { N }

    { V und     B } C { N }  
und { V und not B } D { N }
=>  { V } if (B) then C else D { N }

Schleife ...benötigt Invariante

wenn  { I and B } A { I },
dann  { I } while (B) do A { I and not B }

Beispiel:

Eingabe int p, q; 
// p = P und q = Q
int c = 0;
// inv: p * q + c = P * Q 
while (q > 0) { 
   ???
}
// c = P * Q

Moral: erst Schleifeninvariante (Spezifikation), dann Implementierung.

Schreiben Sie eine Java-Methode, deren Kompilation genau diesen Bytecode erzeugt: a)

  public static int h(int, int);
    Code:
       0: iconst_3      
       1: iload_0       
       2: iadd          
       3: iload_1       
       4: iconst_4      
       5: isub          
       6: imul          
       7: ireturn

  public static int g(int, int);
    Code:
       0: iload_0       
       1: istore_2      
       2: iload_1       
       3: ifle          17
       6: iload_2       
       7: iload_0       
       8: imul          
       9: istore_2      
      10: iload_1       
      11: iconst_1      
      12: isub          
      13: istore_1      
      14: goto          2
      17: iload_2       
      18: ireturn

Ergänze das Programm:

Eingabe: natürliche Zahlen a, b;
// a = A und b = B
int p = 1; int c = ???;
// Invariante:  c^b * p = A^B
while (b > 0) {
    ???
    b = abrunden (b/2);
}
Ausgabe: p; // p = A^B

2015-08-17