DOC PREVIEW
UA CSC 520 - Study Notes

This preview shows page 1-2-3 out of 8 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 8 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 8 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 8 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 8 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

↓ 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

UA CSC 520 - Study Notes

Documents in this Course
Handout

Handout

13 pages

Semantics

Semantics

15 pages

Haskell

Haskell

15 pages

Recursion

Recursion

18 pages

Semantics

Semantics

12 pages

Scheme

Scheme

32 pages

Syllabus

Syllabus

40 pages

Haskell

Haskell

17 pages

Scheme

Scheme

27 pages

Scheme

Scheme

9 pages

TypeS

TypeS

13 pages

Scheme

Scheme

27 pages

Syllabus

Syllabus

10 pages

Types

Types

16 pages

FORTRAN

FORTRAN

10 pages

Load more
Download Study Notes
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Study Notes and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Study Notes 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?