CS101.3 Programing Language Semantics

CS101.3Programing LanguageSemanticsLecture 1January 9, 2004CS101.3: Programing Language SemanticsLecture 1January 9, 2004 – p. 1/11

Quick InformationTime:Place:Instructors:Office Hours:Units:Course Home Page:Admin email:Mailing list:F 14:00 – 15:00Jorgensen 74Jason Hickey and Aleksey NoginJorgensen 60; TBA, and by appt4 (1 0 3), pass/fail or letter gcs101-class@metaprl.orgTextbook:Glynn Winskel. The Formal Semanticsof Programming Languages. An Introduction.CS101.3: Programing Language SemanticsLecture 1January 9, 2004 – p. 2/11

Assigning Meaning toProgramsHow the program executes — operational semanticsWhat the program as a whole means — denotationalsemanticsWhat properties does a program have — axiomaticsemanticsCS101.3: Programing Language SemanticsLecture 1January 9, 2004 – p. 3/11

Assigning Meaning toPrograms — Examplelet fact i if i 1 then 1 else fact (i-1) * iHow the program executes (operational semantics): “tocompute fact, first compare input to 1, if equals, thenreturn 1, else . . .”;What the program as a whole means (denotationalsemantics): “fact computes the factorial function”;What properties does a program have (axiomaticssemantics): “when input is a positive integer, fact wouldterminate”.CS101.3: Programing Language SemanticsLecture 1January 9, 2004 – p. 4/11

IMP—a Simple ImperativeLanguageNumbers (N): m, nLocations (Loc): X , YArithmetical expressions (Aexp):a :: n X a1 a2 a1 a2 a1 a2Boolean expressions (Bexp):b :: true false a1 a2 a1 a2 b b1 b2 b1 b2Commands (Com):c :: skip X : a c1 ; c2 if b then c1 else c2 while b do cCS101.3: Programing Language SemanticsLecture 1January 9, 2004 – p. 5/11

Evaluation: StateA state σ maps locations to numbers. Σ Loc N — set allall states. σ(X) — contents of location X in state σ .For σ Σ and a Aexp we will define a relation hσ, ai n:hσ, ni nhσ, Xi σ(X)hσ, a1 i n1 hσ, a2 i n2hσ, a1 a2 i , where n n1 n2 .hσ, a1 a2 i nhσ, a i n hσ, a2 i n2hσ, a11 a2 i 1 , where n n1 n2 .hσ, a1 a2 i netcCS101.3: Programing Language SemanticsLecture 1January 9, 2004 – p. 6/11

Evaluation ExampleIn σ0 that maps all locations to 0, evaluate (I 1) (4 2)hσ0 , Ii 0hσ0 , 1i 1hσ0 , I 1i 1hσ0 , 4i 4hσ0 , 2i 2hσ0 , 4 2i 2hσ0 , (I 1) (4 2)i 2CS101.3: Programing Language SemanticsLecture 1January 9, 2004 – p. 7/11

Evaluation of Booleanshσ, truei true and hσ, falsei falsehσ, a1 i n1 hσ, a2 i n2, if n1 and n2 are equal;hσ, a1 a2 i truehσ, a1 i n1 hσ, a2 i n2, if n1 and n2 are unequal;hσ, a1 a2 i falsehσ, bi truehσ, bi falseandhσ, bi falsehσ, bi trueetcCS101.3: Programing Language SemanticsLecture 1January 9, 2004 – p. 8/11

Equivalence ofExpressionsTwo expressions are equivalent if they evaluate to the samething in any state:a1 a2 iff σ Σ. n N. hσ, a1 i n hσ, a2 i nSimilarly, for booleans:b1 b2 iff σ Σ. t {true, false}. hσ, b1 i t hσ, b2 i tExample. Whenever b1 true, b1 b2 true (for anyb2 Bexp).CS101.3: Programing Language SemanticsLecture 1January 9, 2004 – p. 9/11

Evaluation of Commandshσ, skipi σhσ, ai nhσ, X : ai σ[n/X]hσ, c1 i σ 0 σ 0 , c2 σ 00hσ, c1 ; c2 i σ 00hσ, bi true hσ, c1 i σ 0hσ, if b then c1 else c2 i σ 0hσ, bi false hσ, c2 i σ 0hσ, if b then c1 else c2 i σ 0hσ, bi falsehσ, while b do ci σhσ, bi true hσ, ci σ 0 σ 0 , while b do c σ 00hσ, while b do ci σ 00CS101.3: Programing Language SemanticsLecture 1January 9, 2004 – p. 10/11

TheoremLet w : while b do c. Thenw if b then c; w else skipCS101.3: Programing Language SemanticsLecture 1January 9, 2004 – p. 11/11

The Formal Semantics of Programming Languages. An Introduction. CS101.3:Programing Language Semantics Lecture 1 January