tharun5859@IndianArmy

Views:
 
Category: Education
     
 

Presentation Description

No description available.

Comments

Presentation Transcript

Denotational Semantics:

Programming Language Principles . Denotational Semantics

Semantic Descriptions:

Semantic Descriptions In general, three approaches to describing semantics of a programming language: Axiomatic approach: Good formalizing type systems. Skipped.  Operational approach: Describe semantics by giving a process . The “meaning” of a program is the result of the process. Program behavior gleaned from process. RPAL: scan, parse, standardize, evaluate.

Denotational Semantics:

Denotational Semantics Denotational approach: Describe semantics by “denoting” constructs, usually with functions. The “meaning” of a program is given by a collection of semantic functions , on a construct-by-construct basis. Program behavior gleaned from behavior of semantic functions. We will specify Tiny.

Denotation Descriptions:

Denotation Descriptions A denotational semantic description has three parts: A set of syntactic domains (usually AST’s). A set of semantic domains . Usually, objects and/or states. A set of semantic functions . Functions describe how PL constructs manipulate/change values in the semantic domains. We will use RPAL notation to describe functions 

Sample Denotational Description:

Sample Denotational Description Let’s describe the behavior of an ‘add’ instruction in a fictitious machine. Syntactic domain: ASTs of the form <Opcode Operand1 Operand2> 2. Semantic domains: Register: {0,1,2,3,4,5,6,7} Value: {16-bit number} Address: {16-bit number} Memory: Address → Value RegValues : Address → Value

Sample Denotational Description:

Sample Denotational Description Semantic function: EE (for EEvaluate). EE: AST → (RegValues x Memory) → (RegValues x Memory) EE takes an AST, and returns a function that takes a (registers,memory) pair, and returns a new (registers,memory) pair. EE shows how the “state” is changed by the construct in the AST. “state”: current register contents, and current memory contents.

Sample Denotational Description:

Sample Denotational Description Description of the ‘add’ operation: EE[<+ r m>] = λ (R,M). let Result = R r + M m in (R, ( λ a. a eq m → Result | M a)) Get contents of register r, add to contents of memory location m (yielding Result). Build new “state”: Registers (mapping) R unchanged. New memory, maps m to Result, otherwise maps as M does.

Sample Denotational Description:

Sample Denotational Description A different ‘add’ operation: EE[<+ r m>] = λ (R,M). let Result = R r + M m in (( λ p. p eq r → Result | R p), M) Get contents of register r, add to contents of memory location m (yielding Result). Build new “state”: New registers: register r contains Result. Memory M unchanged.

Sample Denotational Description:

Sample Denotational Description Clearly, the denotational description specifies the semantics of the <+ r m> instruction. Behavior depends on (is function of) R and M. Add contents of register r and memory m. We specified two versions: Store result in memory location m. Store result in register r.

Functions as “Storage”:

Functions as “Storage” Where do R and M come from ? Consider R 0 = ( λ ().0) all registers contain zero. R 1 = ( λ p. p eq 2 → 3 | R 0 p ) register 2 contains 3, others zero . R 2 = ( λ p. p eq 4 → 7 | R 1 p ) register 2 contains 3, 4 contains 7, others zero. R 3 = ( λ p. p eq 2 → 5 | R 2 p ) register 2 contains 5 ! (3 forgotten) register 4 contains 7, others zero.

Some Useful Notation:

Some Useful Notation The “pipeline” operator (=>): x => f denotes x eq error → error | f(x) Before applying a function f to an argument: Check whether it’s error. If it is, cancel application of f, return error. x f

Some Useful Notation (cont’d):

Some Useful Notation (cont’d) The “ o ” (composition) operator is defined as o = λ f. λ g. λ x. f x eq error → error | g(f x) The “ o ” function takes two functions, f and g, and an argument x. Evaluate f(x): If f(x) is error, return error (cancel application of g) Otherwise, return g(f(x)).

Some Useful Notation (cont’d):

Some Useful Notation (cont’d) We will use “ o ” as an infix operator, writing f o g instead of o f g. Advantage: (f o g o h) x means calculate h(g(f(x))), but cancel all applications if the result is ‘error’ anywhere along the way. x f g h

Some Useful Notation (cont’d):

Some Useful Notation (cont’d) In our expressions, o has higher precedence than => Example: x => f o g o h means (f o g o h) x which is h(g(f(x) unless any value (including x) is ‘error’ along the way. Also, both => and o are left associative.

Tiny’s Denotational Semantics:

Tiny’s Denotational Semantics Tiny’s syntactic domains: AST = E + C + P, where E = 0 | 1 | 2 ... | true | false | read | Id | <not E> | < ≤ E E> | <+ E E> C = <:= I E> | <print E> | <if E C C> | <while E C> | <; C C> P = <program C>

Tiny’s Denotational Semantics (cont’d):

Tiny’s Denotational Semantics (cont’d) Tiny’s Semantic Domains. State: Mem x Input x Output Mem: Id → Val Input: Val* (zero or more values) Output: Val* Val: Num + Bool

Tiny’s Denotational Semantics (cont’d):

Tiny’s Denotational Semantics (cont’d) Tiny’s semantic functions. EE: E → State → (Val x State) CC: C → State → State PP: P → Input → Output

Some Auxiliary Functions:

Some Auxiliary Functions Return: Val → State → (Val x State) λ v. λ s. (v,s) Check: Domain → (Val x State) → (Val x State) λ D. λ (v,s). v  D → (v,s) | error Dummy: State → State λ s. s Cond: (State → State) λ F 1 . → (State → State) λ F 2 . → (Val x State) λ (v,s). → State s => (v → F 1 | F 2 ) Replace: Mem → Id → Val → Mem λ m. λ i. λ v. ( λ i'. i' eq i → v | m i')

Now, for EE, CC, and PP:

Now, for EE, CC, and PP EE[0] = Return 0; EE[1] = Return 1; EE[2] = Return 2; ... etc. EE[true] = Return true; EE[false] = Return false EE[read] = λ (m,i,o). Null i → error | (Head i, (m, Tail i, o)) EE[I] = λ (m,i,o). m I eq  → error | (m I, (m,i,o))

The EE Semantic Function (cont’d):

The EE Semantic Function (cont’d) EE[<not E>] = EE[E] o (Check Bool) o ( λ (v,s).((not v),s) ) EE[<≤ E1 E2>] = EE[E1] o (Check Num) o ( λ (v1,s1). s1 => EE[E2] => (Check Num) => ( λ (v2,s2).(v1 ≤ v2,s2) )

The EE Semantic Function (cont’d):

The EE Semantic Function (cont’d) EE[<+ E1 E2>] = EE[E1] o (Check Num) o ( λ (v1,s1). s1 => EE[E2] => (Check Num) => ( λ (v2,s2).(v1 + v2,s2) )

The CC Semantic Function:

The CC Semantic Function CC[<:= I E>] = EE[E] o ( λ (v,(m,i,o)). (Replace m I v, i, o)) CC[<print E>] = EE[E] o ( λ (v,(m,i,o)). (m,i,o aug v)) CC[<if E C1 C2>] = EE[E] o (Check Bool) o (Cond CC[C1] CC[C2])

The CC and PP Semantic Functions:

The CC and PP Semantic Functions CC[<while E C>] = EE[E] o (Check Bool) o (Cond (CC[<; C <while E C>>]) Dummy) CC[<; C1 C2>] = CC[C1] o CC[C2] PP[<program C>] = ( λ i. CC[C] (( λ () .  ), i, nil)) o ( λ (m,i,o).o) The meaning of a Tiny program <program C> is PP[<program C>]

Semantics of Tiny:

Semantics of Tiny Issues enforced: true, false, read not, if, while, print treated as reserved words. Can’t read from empty input. Can’t use undefined variable values. Argument of ‘not’ must be Bool. ≤ comparison allowed only on Nums. ‘+’ allowed only on Nums. ‘If’ control expression must be Bool. ‘while’ control expression must be Bool.

Semantics of Tiny (cont’d):

Semantics of Tiny (cont’d) Issues not enforced: Can store Bools ? Yes, even in a variable currently holding a Num ! Legal values to print ? Anything. No type checking on input values. Typing issues difficult to enforce: Tiny has no declarations.

PowerPoint Presentation:

Than Q

authorStream Live Help