Zurich¨Technische HochschuleEidgenossische¨
Swiss Federal Institute of Technology ZurichPolitecnico federale di ZurigoEcole polytechnique federale de Zurich´ ´
Semantik von ProgrammiersprachenTheorie und Anwendungen
(Informatik III, Wintersemester 03/04)
Robert F. Stark
Institut fur Theoretische Informatik
ETH Zurich
http://www.inf.ethz.ch/˜staerk
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 1
Inhalt
Teil 1: Naturliche Semantik von Programmen
Teil 2: ASM Semantik von Programmen
Teil 3: Compilation auf virtuelle Maschine
Teil 4: Denotationelle Semantik
Teil 5: Hoare-Logik
Teil 6: Dynamische Logik
Teil 7: Bytecode Verification
Teil 8: Proof-Carrying Code
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 2
Ubersicht
Aequivalenz
Aequvialenz
ASM−Semantik (small−step)
Korrektheit der Axiome
Virtuelle Maschine Proof−carrying Code
Natürliche Semantik (big−step)
Bytecode Verification
Denotationelle Semantik
Compilation
Hoare−LogikDynamische Logik
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 3
Zusammenfassung
Am Beispiel einer imperativen Programmiersprache mit einfachenDatentypen und rekursiven Prozeduren werden die elementarenKonzepte der Semantik von Programmiersprachen erklart.
Es wird gezeigt, inwiefern die operationelle mit derdenotationellen Semantik ubereinstimmt.
Die denotationelle Semantik bildet die Grundlage fur korrekteAxiome und Beweisregeln (sogenannte axiomatische Semantikoder Hoare Logik).
Die operationelle Semantik wird benutzt fur die beweisbarkorrekte Compilation auf eine einfache virtuelle Maschine.
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 4
Folien mit Stern ∗
Folien, die rechts oben mit einem Stern markiert sind, enthalten Beweisevon Satzen und weiterfuhrendes Material.
Beim ersten Durcharbeiten konnen Stern-Folien ubergangen werden.
Der Inhalt der Stern-Folien ist nicht Prufungsstoff.
Beachte:
Auch wenn die Beweise nicht als Prufungsstoff gelten, sind sietrotzdem wichtig.
Fur das Verstandnis der Semantik von Programmiersprachen sind siegenauso wichtig wie die Beispiele.
Beweise sind eine Form der Kommunikation von abstraktenKonzepten und mathematischen Ideen unter Menschen.
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 5
Literatur
Hanne Riis Nielson, Flemming NielsonSemantics with Applications: A Formal IntroductionWiley, 1992.http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html
Betrand MeyerIntroduction to the Theory of Programming LanuagesPrentice Hall, 1990
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 6
Weiterfuhrende Literatur
Glynn WinskelThe Formal Semantics of Programming Languages: an IntroductionThe MIT Press, 1993
Carl A. GunterSemantics of Programming LanguagesThe MIT Press, 1992
John C. MitchellFoundations of Programming LanguagesThe MIT Press, 1996
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 7
Weiterfuhrende Literatur
Krzysztof R. Apt, Ernst-Rudiger OlderogVerification of Sequential and Concurrent ProgramsSpringer-Verlag, 2nd ed., 1997
David Harel, Dexter Kozen, Jerzy TiurynDynamic LogicThe MIT Press, 2000
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 8
Semantik von Programmiersprachen
Was ist die Bedeutung eines Programms?
Programmiersprache
↗ Syntax
→ Statische Semantik
↘ Dynamische Semantik
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 9
Syntax
Die Syntax wird durch eine Grammatik angegeben.
Folge von Zeichen (Source File)
↓ lexikalische Analyse
Folge von Tokens
↓ Parser
abstrakter Syntaxbaum
Die Grammatik definiert eine Relation zwischen Zeichenfolgen undabstrakten Syntaxbaumen.
[Siehe Vorlesung Compilerbau.]
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 10
Semantik (statisch vs. dynamisch)
Statische Semantik (Was muss zur Compilezeit uberpruft werden?)
Typregeln, Typuberprufung
statische Analyse (z.B. Definite Assignment)
Auflosung von Namen
Auflosung von Methoden (fur uberladene Methoden)
Resultat: annotierter abstrakter Syntaxbaum
Dynamische Semantik (Was geschieht zur Laufzeit?)
Ausfuhrung des Programms (program execution)
Was definiert den Zustand eines Programms?
Was ist der Effekt eines Programms auf den Zustand?
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 11
Dynamische Semantik
Denotationelle Semantik (Programme = mathematische Objekte)
Ein Programm wird betrachtet als (partielle) Funktion in einemmathematischen Raum.
Gut fur deklarative Sprachen (funktionale Programmierung).
Zu kompliziert fur objekt-orientierte Sprachen mit Vererbung,Exception Handling, Threads.
Operationelle Semantik
Varianten:
Naturliche Semantik (Big-Step Semantics)
SOS (Structural Operational Semantics)
ASMs (Gurevich Abstract State Machines)
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 12
Anwendungen der Semantik
Warum eine formale Spezifikation der Semantikeiner Programmiersprache?
nutzlich fur Implementation(korrekte Compilation,Platform-Unabhangigkeit)
Grundlage fur formale Methoden(erweiterte statische Analyse, Verifikation,Korrektheit von Axiomen und Beweisregeln)
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 13
Eine einfache imperative Programmiersprache
While-Programme
Nur zwei Typen: boolean, integer
Boolesche Ausdrucke
Arithmetische Ausdrucke
Alle Variablen werden initialisiert
Rekursive Prozeduren
Werte- und Variablenparameter
Keine Funktionen
Keine Ausdrucke mit Seiteneffekten
Reihenfolge der Auswertung der Argumente beliebig
Keine globalen Variablen
Kein “zufalliges” Verhalten wegen uninitialisierten Variablen
Vermeidung von Alias-Problemen
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 14
Mitteilungszeichen (Metavariablen)
Mitteilungszeichen:
x , y , z . . . . . . . . fur Variablen (Var)
e, e1, e2 . . . . . . . fur arithmetische Ausdrucke (Aexp)
b, b1, b2 . . . . . . . fur Boolesche Ausdrucke (Bexp)
s , s ′, s1, s2 . . . . . fur Anweisungen (Stm)
p . . . . . . . . . . . . . fur Namen von Prozeduren
Vektornotation:
~x = x1, x2, . . . , xm
~e = e1, e2, . . . , en
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 15
Bedeutung der Anweisungen (informale Semantik)
skip Mache nichts (leere Anweisung).
x := e Weise x den Wert von e zu.
s1 ; s2 Fuhre zuerst s1 aus, danach s2.
if b then s1 else s2 end Falls b wahr ist, fuhre s1 aus, sonst s2.
while b do s end Solange b wahr ist, fuhre s aus.
var x := e in s end Erzeuge eine neue lokale Variable x mitdem Wert von e und fuhre s aus.
p(~e;~z) Rufe die Prozedur p mit den Wertenvon ~e und den Variablen ~z auf.
Bedingung: Die Variablen in ~z mussen paarweise verschieden sein.
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 16
Bedeutung der Ausdrucke (informale Semantik)
Arithmetische Ausdrucke:
x Zugriff auf Variable
i Konstante (Literal)
e1 op e2 Arithmetische Operation, op ∈ {+, -, *, /}
Boolesche Ausdrucke:
e1 op e2 Relation, op ∈ {=, #, <, <=, >, >=}
not b Negation (nicht)
b1 and b2 Konjunktion (und)
b1 or b2 Disjunktion (oder)
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 17
Prozedurdeklarationen
Prozedurdeklaration:
procedure p(~x;~y) begin s end
Formale Parameter:
Die Variablen ~x sind Werteparameter (call-by-value)
Die Variablen ~y sind Variablenparameter (call-by-name)
Syntaktische Bedingungen:
Die Variablen in ~x und ~y mussen paarweise verschieden sein.
Jede freie Variable von s muss in ~x oder ~y vorkommen(keine globalen Variablen).
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 18
Grammatik der Programmiersprache
EBNF (extended Backus-Naur Formalism)
‘Terminalsymbol’NichtterminalsymbolAlternative | Alternative{Wiederholung}[Optional]
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 19
Grammatik (Zeichen und Tokens)
Zeichen:
Letter = ‘A’ . . ‘Z’ | ‘a’ . . ‘z’.
Digit = ‘0’ | ‘1’ | ‘2’ | ‘3’ | ‘4’ | ‘5’ | ‘6’ | ‘7’ | ‘8’ | ‘9’.
Tokens:
Ident = Letter {Letter | Digit}.
Integer = Digit {Digit}.
Var = Ident.
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 20
Grammatik (Anweisungen)
Stm = ‘skip’
| Var ‘:=’ Aexp
| ‘if’ Bexp ‘then’ StmSeq ‘else’ StmSeq ‘end’
| ‘while’ Bexp ‘do’ StmSeq ‘end’
| ‘var’ Var ‘:=’ Aexp ‘in’ StmSeq ‘end’
| Ident ‘(’ [AexpList] [‘;’ VarList] ‘)’.
StmSeq = Stm {‘;’ Stm}.
AexpList = Aexp {‘,’ Aexp}.
VarList = Var {‘,’ Var}.
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 21
Grammatik (Arithmetische Ausdrucke)
Aexp = Term {AddOp Term}.
Term = Factor {MulOp Factor}.
Factor = Var | Integer | ‘(’ Aexp ‘)’.
AddOp = ‘+’ | ‘-’.
MulOp = ‘*’ | ‘/’ | ‘div’ | ‘mod’.
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 22
Grammatik (Boolesche Ausdrucke)
Bexp = OrExp {‘or’ OrExp}.
OrExp = PrimExp {‘and’ PrimExp}.
PrimExp = ‘not’ PrimExp | ‘(’ Bexp ‘)’ | Aexp RelOp Aexp.
RelOp = ‘=’ | ‘#’ | ‘<’ | ‘<=’ | ‘>’ | ‘>=’.
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 23
Grammatik (Programme)
Program = {Procedure}.
Procedure = Head ‘begin’ StmSeq ‘end’.
Head = ‘procedure’ Ident ‘(’ [VarList] [‘;’ VarList] ‘)’.
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 24
Bereiche der Variablen
var x := e in . . . . . . . . .︸ ︷︷ ︸Bereich von x
end
procedure p(~x;~y) begin . . . . . . . . . . . . . . .︸ ︷︷ ︸Bereich von ~x und ~y
end
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 25
Freie Variablen in Ausdrucken
Arithmetische Ausdrucke:
FV(x ) = {x}
FV(i) = ∅ (i ein Integer)
FV(e1 op e2) = FV(e1) ∪ FV(e2) (op ∈ AddOp ∪MulOp)
Boolesche Ausdrucke:
FV(e1 op e2) = FV(e1) ∪ FV(e2) (op ∈ RelOp)
FV(not b) = FV(b)
FV(b1 and b2) = FV(b1 or b2) = FV(b1) ∪ FV(b2)
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 26
Freie Variablen in Anweisungen
FV(skip) = ∅
FV(x := e) = {x} ∪ FV(e)
FV(s1 ; s2) = FV(s1) ∪ FV(s2)
FV(if b then s1 else s1 end) = FV(b) ∪ FV(s1) ∪ FV(s2)
FV(while b do s end) = FV(b) ∪ FV(s)
FV(var x := e in s end) = FV(e) ∪ (FV(s) \ {x})
FV(p(~e;~z)) = FV(~e) ∪ {~z}
Vektoren: Fur ~e = e1, . . . , en ist FV(~e) = FV(e1) ∪ . . . ∪ FV(en)
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 27
Syntaktische Abkurzungen
if b then s end if b then s else skip end
repeat s until b s; while not b do s end
for x := e1 to e2 do s end x := e1;
var y := e2 in
while x <= y do
s; x := x + 1
end
end
if b1 then s1elsif b2 then s2else s3 end
if b1 then s1 elseif b2 then s2 else s3 end
end
Bedingung fur For-Schleife: x /∈ FV(e2), y /∈ FV(s).
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 28
Liste der Folien
Inhalt . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
Ubersicht . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
Zusammenfassung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
Folien mit Stern . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
Literatur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
Weiterfuhrende Literatur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
Weiterfuhrende Literatur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
Semantik von Programmiersprachen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
Semantik (statisch vs. dynamisch) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
Dynamische Semantik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
Anwendungen der Semantik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
Eine einfache imperative Programmiersprache . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
Mitteilungszeichen (Metavariablen) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
Bedeutung der Anweisungen (informale Semantik) . . . . . . . . . . . . . . . . . . . . . . . . . . 16
Bedeutung der Ausdrucke (informale Semantik) . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
Prozedurdeklarationen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 29
Grammatik der Programmiersprache . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
Grammatik (Zeichen und Tokens) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
Grammatik (Anweisungen) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
Grammatik (Arithmetische Ausdrucke) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
Grammatik (Boolesche Ausdrucke) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
Grammatik (Programme) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
Bereiche der Variablen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
Freie Variablen in Ausdrucken . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
Freie Variablen in Anweisungen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
Syntaktische Abkurzungen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Copyright c© 2004 Robert F. Stark, Computer Science Department, ETH Zurich, Switzerland. 30