↓ cut ↓ ↓ cut ↓ 2/26/106static10FOIL 1| |+ +Static Semantics— structural constraints not captured by BNF orabstract grammar— resolvable at "semantic analysis time" (aftersymbol-table built)ex: Command ::= while Expression doCommand— Expression must be boolean valued— can be expressed by CFG, but introducing morenon-terminals complicates grammarex: Dec_list ::= Dec ; Dec_list | DecDec ::=var Identifier:Type-denoter— constraint: no variable name declared twice— cannot be expressed by a CFG (BNF)ex: Command ::= Identifier := Expression— constraint: id type = var-t where t = expr type— in theory can be enforced by a huge CFG+ +| | 2/26/106static10FOIL 2| |+ +Static Semantics: Typing Functions— Types are a kind of coarse "value"— Type checker: semantic maps that sendExpression s, etc. to Type values— Type values not "run-time" or "dynamic" values.— Type a very simple semantic domainType = bool − type + int − type+ var − bool − type + var − int − type + err − type+ +| | 2/26/106static10FOIL 3| |+ +Type Environment "Static Environment" (implementable by symbol table) Type-Environ = Identifier→Type— typenv : Type-Environ a type assignment thatmaps identifiers to types— typenv usually produced by scanning a declarationlist— analogous to Environ (run-time or "dynamic"environments) Auxiliary functions for Type-Environempty − environ : Type-Environbind : Identifier × Type→Type-Environoverlay : Type-Environ × Type-Environ→Type-Environfind : Type-Environ × Identifier→Type Static semantic function signatures:typify : Expression→(Type-Environ→Type )constrain : Command→(Type-Environ→Boolean )declare : Declaration→(Type-Environ→Boolean × Type-Environ )+ +| | 2/26/106static10FOIL 4| |+ +Expression Typing typify : Expression→Type-Environ→Type— Expressions have a type value in a given typeenvironment— type environments produced by declarationtypify[[N]] typenv =int − typetypify[[true ]] typenv =bool − typetypify[[false ]] typenv =bool − typetypify[[I]] typenv =coerce − type( find(typenv, I) )auxiliary function:coerce − type : Type→Typecoerce − type(bool − type) = bool − typecoerce − type(int − type) = int − typecoerce − type(var − bool − type) = bool − typecoerce − type(var − int − type) = int − type— coerce − type does "type dereferencing"+ +| | 2/26/106static10FOIL 5| |+ +Expression Typing (cont’d)typify[[E1+ E2]] typenv =if int − type = typify [[E1]] typenv∧ int − type = typify [[E2]] typenvthen int − typeelse err − typetypify[[E1< E2]] typenv =if int − type = typify [[E1]] typenv∧ int − type = typify [[E2]] typenvthen bool − typeelse err − typetypify[[not E]] typenv =if bool − type = typify [[E]]typenvthen bool − typeelse err − type. . .+ +| | 2/26/106static10FOIL 6| |+ +Command Typing constrain : Command→(Type-Environ→Boolean ) expressions are constrained as consistent or not in agiven type environmentconstrain[[skip ]] typenv =trueconstrain[[I:= E]] typenv =let typval = typi fy[[E]] typenv inlet vartypval = find(typenv, I) in(vartypval = var(typval) )var : Type→Typevar(int − type) = var − int − typevar(bool − type) = var − bool − typeconstrain[[let D in C]] typenv =let (ok, typenv′) = declare[[D]] typenv inif okthen constrain[[C]] (overlay(typenv′, typenv))else false+ +| | 2/26/106static10FOIL 7| |+ +Command Typing (cont’d)constrain[[C1; C2]] typenv =constrain[[C1]] typenv ∧ constrain[[C2]] typenvconstrain[[if E then C1else C2]] typenv =(typify[[E]] typenv = bool − type)∧ constrain[[C1]] typenv∧ constrain[[C2]] typenvconstrain[[while E do C]] typenv =(typify[[E]] typenv = bool − type)∧ (constrain[[C]] typenv)+ +| | 2/26/106static10FOIL 8| |+ +Declaration Typing declare : Declaration→(Type-Environ→Boolean × Type-Environ )— declarations are declared in a type environment— produce a new elementary type environment— T : Type-denoter has a meaning in Typedeclare[[const I ∼ E]] typenv =let typ = typi fy[[E]] typenv inif (typ = err − type)then ( false, empty − environ )else ( true, bind(I, typ) )declare[[var I : T]] typenv =let typ = type − denoted − by [[T]] in( true, bind(I, var(typ)) )type − denoted − by[[bool ]] = bool − typetype − denoted − by[[int ]] = int − type+ +| |↑ cut ↑ ↑ cut
View Full Document