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