ZurichÈ Technische Hochschule Semantik von ... · F¨ur das Verst ¨andnis der Semantik von...

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


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


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.


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.


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


http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html

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


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


Semantik von Programmiersprachen

Was ist die Bedeutung eines Programms?

Programmiersprache

↗ Syntax

→ Statische Semantik

↘ Dynamische Semantik


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.]


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?


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)


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)


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


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


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.


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)


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).


Grammatik der Programmiersprache

EBNF (extended Backus-Naur Formalism)

‘Terminalsymbol’NichtterminalsymbolAlternative | Alternative{Wiederholung}[Optional]


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.


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}.


Grammatik (Arithmetische Ausdrucke)

Aexp = Term {AddOp Term}.

Term = Factor {MulOp Factor}.

Factor = Var | Integer | ‘(’ Aexp ‘)’.

AddOp = ‘+’ | ‘-’.

MulOp = ‘*’ | ‘/’ | ‘div’ | ‘mod’.


Grammatik (Boolesche Ausdrucke)

Bexp = OrExp {‘or’ OrExp}.

OrExp = PrimExp {‘and’ PrimExp}.

PrimExp = ‘not’ PrimExp | ‘(’ Bexp ‘)’ | Aexp RelOp Aexp.

RelOp = ‘=’ | ‘#’ | ‘<’ | ‘<=’ | ‘>’ | ‘>=’.


Grammatik (Programme)

Program = {Procedure}.

Procedure = Head ‘begin’ StmSeq ‘end’.

Head = ‘procedure’ Ident ‘(’ [VarList] [‘;’ VarList] ‘)’.


Bereiche der Variablen

var x := e in . . . . . . . . .︸︷︷︸Bereich von x

end

procedure p(~x;~y) begin . . . . . . . . . . . . . . .︸︷︷︸Bereich von ~x und ~y

end


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)


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)


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).


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


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


ZurichÈ Technische Hochschule Semantik von ... · F¨ur das Verst ¨andnis der Semantik von...

Documents

Transcript of ZurichÈ Technische Hochschule Semantik von ... · F¨ur das Verst ¨andnis der Semantik von...