CSc 520Principles of Programming Languages50: Semantics — IntroductionChristian CollbergDepartment of Computer ScienceUniversity of [email protected] 2005 Christian CollbergApril 22, 20051 Formal Semantics• In order for1. compiler writers to know exactly how to implement a language, and2. language users to know exactly what (combinations of) language constructs mean,the meaning of a language needs to be defined.• Most definitions of real languages are in a stylized, but informal, English.• It is also possible to give formal semantic language definitions.2 Formal Semantics. . .• In practice, most languages are not defined in a formal, precise, mathematical way.• There have been some attempts, for example Modula-2, Algol 68, and PL/I.• “Simple” languages such as Scheme and Haskell are comparatively easy to define formally, comparedto C, C++, Java, etc.3 Formal Semantics — Modula-2• The Modula-2 specification was written in VDM-SL (Vienna Development Method - Specification Lan-guage), a formalism for giving a precise definition of a programming language in a denotational style.• It was over 500 pages long, and didn’t include specifications of the standard libraries.• Wirth’s original Modula-2 report was 28 pages.1• For a history of this disastrous standardization effort, see http://www.scifac.ru.ac.za/cspt/sc22wg13.htm.• Note also that Modula-2 is a very simple language compared to Ada, C++, Java, etc.4 Formal Semantics — PL/I• VDL (Vienna Definition Language) was used to specify PL/I.• A specification has two parts:1. A translator that specified a translation into an abstract syntax tree,2. an interpreter of the abstract syntax tree.• VDL is a kind of operational semantics.• PL/I is large and complex.• The resulting (large) document was called the Vienna Telephone Directory. It was impossible tocomprehend.5 MethodsIn this class we will consider two methods for defining the semantics of programming languages:• Operational semantics define a computation by giving step-by-step transformations on a abstract ma-chine that simulate the execution of the program.• Denotational semantics constructs a mathematical object (typically a function) which is the meaningof the program.6 Contextual Constraints• A compiler performs syntactic and semantic analysis. There really isn’t a sharp distinction betweenthe two.• Is String x; · · ·; print x/2 a syntactic or semantic error?• Some would say that it violates the static semantic rules of the language, and hence is a semantic (nota syntactic) error.• Others would say it violates context-sensitive syntax rules of the language. I.e., they’d consider theprogram as a whole to determine if it is well-formed or not.• We will use the term contextual constraints for those rules that restricts the programs which areconsidered well-formed.27 Operational Semantics• Operational Semantics specifies a language through the steps by which each program is executed.• This is often done informally. For example, the statement while E do C is specified as1. Evaluate E to a truthvalue B;2. If B = true then execute C, then repeat from 1).3. If B = false, terminate.• The emphasis is on specifying the steps needed to execute the program. This makes the specificationuseful for language implementers.8 Operational Semantics. . .• We need two things:1. an abstract syntax, and2. an interpreter.• The abstract syntax defines the structure of each construct in the language, for example, that anif-statement consists of three parts: the test e, the then-part c1and the else-part c2:if ::= e:bool expr c1:statement c2:statementNote that no syntactic information is given.• The interpreter generates a sequence of machine configurations that define the program’s semantics.The interpreter is defined by rewriting rules.9 Operational 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 ∈ Nat10 Operational Sem. — Peano Arithmetic• The rewrite rules are used to turn an expression into standard form, containing only S (succ) and 0.• S(S(S(S(0)))) = 4.311 Operational Sem. — Simple. . .• Simple is a language with if-statements, while-statements, assignment-statements, and integer arith-metic.• 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 the program) is the resulting store.12 Operational 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, σ) = false13 Operational 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 Denotational Semantics• We think of each program as implementing a mathematical function.• An imperative program is a function from inputs to outputs. This function is the meaning of theprogram.• Example4exec [[while E do C]] =let exec-while env sto =let Boolean tr = evaluate [[E]] env sto inif tr thenexec-while env (exec [[C]] env sto)else stoinexec-while15 Denotational Semantics. . .• We need three things:1. an abstract syntax,2. a semantic algebra defining a computational model, and3. valuation functions.• The valuation functions map the syntactic constructs of the language to the semantic algebra.• Denotational semantics relies on defining an object in terms of its constituent parts.16 Denotational Sem. — Peano ArithmeticAbstract Syntax (N ∈ Nat, the Natural Numbers):N ::= 0 | S(N) | (N + N) | (N × N)Semantic Algebra:+ : Nat → Nat → NatValuation Function:D : Nat → NatD [[(n + 0)]] = D [[n]]D [[(m + S(n))]] = D [[(m + n)]] + 1D [[(n × 0)]] = 0D [[(m × S(n))]] = D [[((m × n) + m)]]where m, n ∈ Nat17 Denotational Sem. — SimpleAbstract Syntax:• C ∈ Command• E ∈ Expression• O ∈ Operator• N ∈ Numeral5• V ∈ VariableC ::= V := E | if E then
View Full Document
Unlocking...