Formal SemanticsFormal Semanticsldots Formal Semantics --- Modula-2Formal Semantics --- PL/IMethodsContextual ConstraintsOperational SemanticsOperational Semanticsldots Operational Sem. --- Peano ArithmeticOperational Sem. --- Peano ArithmeticOperational Sem. --- Simpleldots Operational Sem. --- Simpleldots Operational Sem. --- Simpleldots Denotational SemanticsDenotational Semanticsldots Denotational Sem. --- Peano ArithmeticDenotational Sem. --- SimpleDenotational Sem. --- Simpleldots Denotational Sem. --- Simpleldots Concrete Syntax of WrenWrenConcrete SyntaxConcrete Syntaxldots Concrete Syntaxldots Wren --- ExampleReadings and ReferencesAcknowledgments520—Spring 2005—50CSc 520Principles of ProgrammingLanguages50: Semantics — IntroductionChristian [email protected] of Computer ScienceUniversity of ArizonaCopyrightc 2005 Christian Collberg[1]520—Spring 2005—50Formal SemanticsIn order for1. compiler writers to know exactly how to implement alanguage, and2. language users to know exactly what (combinationsof) language constructs mean,themeaning of a language needs to be defined.Most definitions of real languages are in a stylized, butinformal, English.It is also possible to give formal semantic languagedefinitions.[2]520—Spring 2005—50Formal Semantics...In practice, most languages are not defined in a formal,precise, mathematical way.There have been some attempts, for exampleModula-2, Algol 68, and PL/I.“Simple” languages such as Scheme and Haskell arecomparatively easy to define formally, compared to C,C++, Java, etc.[3]520—Spring 2005—50Formal Semantics — Modula-2The Modula-2 specification was written in VDM-SL(Vienna Development Method - SpecificationLanguage), a formalism for giving a precise definition ofa programming language in a denotational style.It was over 500 pages long, and didn’t includespecifications of the standard libraries.Wirth’s original Modula-2 report was 28 pages.For a history of this disastrous standardization effort,seehttp://www.scifac.ru.ac.za/cspt/sc22wg13.htm.Note also that Modula-2 is a very simple languagecompared to Ada, C++, Java, etc.[4]520—Spring 2005—50Formal Semantics — PL/IVDL (Vienna Definition Language) was used to specifyPL/I.A specification has two parts:1. Atranslator that specified a translation into anabstract syntax tree,2. aninterpreter of the abstract syntax tree.VDL is a kind of operational semantics.PL/I is large and complex.The resulting (large) document was called theVienna Telephone Directory. It was impossible tocomprehend.[5]520—Spring 2005—50MethodsIn this class we will consider two methods for defining thesemantics of programming languages:Operational semantics define a computation by givingstep-by-step transformations on a abstract machine thatsimulate the execution of the program.Denotational semantics constructs a mathematicalobject (typically a function) which is the meaning of theprogram.[6]520—Spring 2005—50Contextual ConstraintsA compiler performs syntactic and semantic analysis.There really isn’t a sharp distinction between the two.Is String x; · · ·; print x/2 a syntactic orsemantic error?Some would say that it violates thestatic semantic rules of the language, and hence is asemantic (not a syntactic) error.Others would say it violates context-sensitive syntaxrules of the language. I.e., they’d consider the programas a whole to determine if it iswell-formed or not.We will use the term contextual constraints for thoserules that restricts the programs which are consideredwell-formed.[7]520—Spring 2005—50Operational SemanticsOperational Semantics specifies a language throughthe steps by which each program is executed.This is often done informally. For example, thestatementwhile E do C is specified as1. EvaluateE to a truthvalue B;2. If B = true then execute C, then repeat from 1).3. IfB = false, terminate.The emphasis is on specifying the steps needed toexecute the program. This makes the specificationuseful for language implementers.[8]520—Spring 2005—50Operational Semantics...We need two things:1. an abstract syntax, and2. an interpreter.The abstract syntax defines the structure of eachconstruct in the language, for example, that anif-statement consists of three parts: the teste, thethen-partc1and the else-part c2:if ::= e:bool expr c1:statement c2:statementNote that no syntactic information is given.The interpreter generates a sequence of machineconfigurations that define the program’s semantics. Theinterpreter is defined by rewriting rules.[9]520—Spring 2005—50Operational Sem. — Peano ArithmeticAbstract Syntax (N ∈ Nat, the Natural Numbers):N ::= 0 | S(N) | (N + N) | ( N × N)Interpreter:I : N → NI [[(n + 0)]] ⇒ nI [[(m + S(n))]] ⇒ S(I [[(m + n)]])I [[(n × 0)]] ⇒ 0I [[(m × S(n))]] ⇒ I [[((m × n) + m)]]where m, n ∈ Nat[10]520—Spring 2005—50Operational Sem. — Peano ArithmeticThe rewrite rules are used to turn an expression intostandard form, containing only S (succ) and 0.S(S(S(S(0)))) = 4.[11]520—Spring 2005—50Operational Sem. — Simple...Simple is a language with if-statements,while-statements, assignment-statements, and integerarithmetic.The semantic function I interprets commands.The semantic function ν interprets expressions.The store σ maps variables to their values.Assignments update the store.The result of the interpretation (the semantics of theprogram) is the resulting store.[12]520—Spring 2005—50Operational Sem. — Simple...Interpreter:I : C × Σ → Σν : E × Σ → T ∪ ZSemantic Equations:I(skip, σ) = σI(V := E, σ) = σ[V 7→ ν(E, σ)]I(C1; C2, σ) = E(C2, E(C1, σ))I(if E then C1else C2end, σ) = I(C1, σ) if ν(E, σ) = trueI(C2, σ) if ν(E, σ) = false[13]520—Spring 2005—50Operational Sem. — Simple...Interpreter:while E do C end =if E then (C; while Edo C end) else skipν(V, σ) = σ[V ]ν(N, σ) = Nν(E1+ E2, σ) = ν(E1, σ) + ν(E2, σ)ν(E1= E2, σ) = true if ν(E, σ) = ν(E, σ)= false if ν(E, σ) 6= ν(E, σ)[14]520—Spring 2005—50Denotational SemanticsWe think of each program as implementing amathematical function.An imperative program is a function from inputs tooutputs. This function is the meaning of the program.Exampleexec [[while E do C]] =let exec-while env sto =let Boolean tr = evaluate [[E]] env sto iniftr thenexec-while env (exec [[C]] env sto)else stoinexec-while[15]520—Spring 2005—50Denotational Semantics...We need three things:1.
View Full Document
Unlocking...