CSc 520 — Principles of Programming Languages54: Semantics — Denotational Semantics — Static SemanticsChristian CollbergDepartment of Computer ScienceUniversity of [email protected] 2005 Christian CollbergApril 27, 20051 Context-Sensitive Syntax• We can use a denotational-semantic style to define the context-sensitive syntax (the context conditions,the static semantic rules) of the language.• These are the rules that a compiler will typically check during the semantic analysis phase of compi-lation.2 Pelican Context Conditions1. The program name identifier lies in a scope outside the main block.2. All identifiers that appear in a block must be declared in that block or in an enclosing block.3. No identifier may be declared more than once at the top level of a block.4. The identifier on the left side of an assignment command must be declared as a variable, and theexpression on the right side must be of the same type.5. An identifier occurring as an (integer) element must be an integer variable or an integer constant.6. An identifier occurring as a Boolean element must be a Boolean variable or a Boolean constant.3 Pelican Context Conditions. . .7. An identifier occurring in a read command must be an integer variable.8. An identifier used in a procedure call must be defined in a procedure declaration with the same (zeroor one) number of parameters.9. The identifier defined as the formal parameter in a procedure declaration is considered to belong tothe top level declarations of the block that forms the body of the procedure.10. The expression in a procedure call must match the type of the formal parameter in the procedure sdeclaration.1The Static Semantics of Pelican4 Abstract Syntactic DomainsThese are the abstract syntactic domains of Pelican:P : ProgramB: BlockC: CommandD: DeclarationT : TypeE: ExpressionO: OperatorN: NumeralI: Identifier5 Abstract Syntax of PelicanProgram ::= program identifier is Block endBlock ::= Declaration* begin Command endDeclaration ::= var Identifier : Type | const Identifier = Expression | procedure Identifier is Block |procedure Identifier ( identifier : Type ) is Block |Type ::= integer | booleanCommand ::= . . . |declare BlockIdentifier |Identifier ( Expression )Expression ::= . . .6 Semantic Domains of Pelican• Environments map identifiers to types.• Sort represents all the different types an expression can take on.• We distinguish between variables (IntVar,BoolVar) and constants (Integer,Boolean).Sort = {Integer, Boolean, IntVar, BoolVar, Program, unbound }Boolean = {true, false}Env = Identifier → Sort27 Semantic Functions of Pelican• We return true if a program satisfies all it static semantic constraints:validate : Program → Boolean• To check a block we need access to an environment containing declared identifiers:examine : Block → Env → Boolean• The result of checking an expression is its type:typify : Expression → Env → Sort8 Semantic Functions of Pelican. . .• To elaborate a declaration we need two environments:elaborate : Declaration → (Env, Env) → (Env, Env)1. The first environment lenv holds the identifiers local to the block. It is used to check for multiplydeclared identifiers.2. The second environment env holds accumulated declarations.• Commands (statements) are checked given an environment of identifiers and their types:check : Command → Env → Boolean9 Environment ADT• The environment is a structure that maps identifiers to their types:• Example:env = {c 7→ Integer, a 7→ IntVar}emptyEnv : EnvextendEnv : Env × Identifier × Sort → EnvapplyEnv : Env × Identifier → SortSemantic Equations310 Programs• We validate the program (check its context conditions) by checking the main block B:validate [[program I is B]] = examine [[B]] envwhere env = extendEnv (e, I, Program)where e = emptyEnv• lenv1will contain all the identifiers declared in D. env contains the identifiers inherited from enclosingblocks:examine [[D begin C end]] env = check [[C]] env1where (lenv1, env1) = elaborate [[D]] (e, env)where e = emptyEnv11 Declarations• Sequences of declarations build up the environment:elaborate [[]] (lenv, env) = (lenv, env)elaborate [[D1D2]] env = elaborate [[D2]] ◦ elaborate [[D1]]• Constant declarations add an entry id 7→ type to the environment, first checking for multiple declara-tions:elaborate [[const I = E]](lenv, env) =if applyEnv (lenv, I) == unbound then(l, e) else errorwhere t = typify [[E]] envl = extendEnv (lenv, I, t)e = extendEnv(env, I, t)12 Declarations. . .• Variable declarations add an entry id 7→ type to the environment, first checking for multiple declara-tions:elaborate [[var I : T ]] (lenv, env) =if applyEnv (lenv, I) == unbound then(l, e) else errorwhere t = type(T )l = extendEnv (lenv, I, t)e = extendEnv(env, I, t)13 Commands• A sequence of commands is OK, if each individual command is:check [[C1; C2]] env = (check [[C1]] env) & (check [[C2]] env)Note that both commands get the same environment.4• The skip command is always OK:check [[skip]] env = true14 Commands. . .• The assignment statement looks up the identifier in the environment and compares it to the type ofthe right hand side:check [[I:= E]] env = (l = IntVar & r = Integer) |(l = BoolVar & r = Boolean)where l = applyEnv (env, I)r = typify [[E]] env• Note that I cannot be an identifier declared to be a constant.15 Commands. . .• If-statements:check [[if E then C]] env = p &check [[C]]where p = typify [[E]] env• If-then-else-statements:check [[if E then C1else C2]] env = p &check [[C1]] &check [[C2]]where p = typify [[E]] env• Loops:check [[while E do C]] env = p &check [[C]]where p = typify [[E]] env16 Commands. . .• Local scope:check [[declare B]] env = examine [[B]] env• Input and Output:check [[read I]] env = applyEnv(I, env) = IntVarcheck [[write E]] env = typify [[E]] env = Integer517 Expressionstypify [[I]] env = if v ∈ {IntVar, Integer} then Integerelse if v ∈ {BoolVar, Boolean} then Booleanelse if v = unbound then errorwhere v = applyEnv(env, I)• We look up the identifier I in the current environment.• Integer variables and constants generate an Integer sort, Boolean variables and constants generate aBoolean sort.• Undeclared identifiers generate an error.18 Expressions. . .typify [[N ]] env = Integertypify [[true]] env = Booleantypify [[false]] env = Booleantypify [[E1+ E2]] env = if m = n = Integerthen Integerelse errorwhere
View Full Document
Unlocking...