DOC PREVIEW
UF COP 5555 - NOTES ON THE DENOTATIONAL SEMANTICS OF TINY

This preview shows page 1-2 out of 7 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 7 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 7 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 7 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

COP 5555 PROGRAMMING LANGUAGE PRINCIPLES NOTES ON THE DENOTATIONAL SEMANTICS OF TINY 1 The operator The operator is defined as follows f g x f x eq error error g f x i e takes two functions f and g and yields a new function on x that returns g f x if f x does NOT evaluate to error and error if f x does evaluate to error simply serves as a convenient way to put error checking in our denotational definition everywhere without laboriously specifying it ourselves everywhere In the denotational semantics description of Tiny we will be using as an INFIX operator writing f g instead of f g Thus f g x f x eq error error g f x This is purely a syntactic convention of ours that turns out to make denotational semantics descriptions read easier It allows a left to right flow reading of such descriptions exemplified below Consider an example where f y 2 y g z z 3 Then f g x y 2 y x eq error error z z 3 y 2 y x x Consider applying f 2 x eq error error 2 x 3 g to an actual argument say 4 f g 4 2 4 eq error error 2 4 3 2 4 3 3 1 2 Now consider f g 0 2 0 eq error error 2 0 3 error since 2 0 eq error division by zero It is to catch things like division by zero or undeclared identifiers that we use Now here s the left to right bent for Re consider f the diagram PLP Notes g 4 The computation can be depicted by Tiny s Denotational Semantics 2 4 f x f g f x g 4 gets sent into f and the result pops out on the other side of f i e f x This result f x gets sent into g unless it equals error in which case the computation in g is skipped and the final answer is g f x So you can read expressions very naturally in a left to right manner In general read the expression f1 f f 2 k as denoting that function of x that first sends x through f1 the result of which is sent through f2 the result of which is sent through f3 the result of which is sent through fk with error checking at each step so that if the evaluation of any fi applied to its argument is error then the evaluation of functions fi 1 fk are SKIPPED and the final answer is error therefore takes two functions and produces a third 2 The operator x f denotes x eq error error f x The difference between and is that takes two FUNCTIONS while takes a value and a function Note If we have x f g h we can replace this with x f g h Also is left associative 3 TINY s rules 3 1 Syntactic domains AST E C P E C P where 0 1 2 true false read Id not E E E E E I E Print E if E C C while E C C1 C2 program C 3 2 Semantic Domains State Mem PLP Notes Mem Input Output Id Val Tiny s Denotational Semantics 3 Output Val Input Val Val Num Bool 3 3 Functionalities of semantic functions EE E State Val State CC C State State PP P Input Output 3 4 Definitions of semantic functions Auxiliary functions Return Val State Val State v s v s Check Domain Val State Val State D v s v D v s error Dummy State State s s Cond State State State State ValxState State F1 F2 v s s v F1 F2 Replace Mem Id Val Mem m i v i i eq i v m i Return takes a value and a state and returns them as a tuple which is the output of EE Check checks that the Val parameter is in the Domain If so it merely returns the Val and State Dummy doesn t do very much it returns the given state Cond takes two State to State functions and a Value State pair It returns the result of applying one of the functions to the State depending on the Value Finally Replace takes an old Mem Id and Val and produces a new Mem in which the Id is associated with the Val 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 read pulls the first input symbol from the input and replaces the input with the rest of the input Example EE read m 5 3 1 o for any memory m and output o has value 5 m 3 1 o The latter is a Val State pair The new State reflects the fact that a value has been pulled off the input Null checks for the nil tuple Head gets the first element of the tuple and Tail gets the tuple containing all but the first element PLP Notes Tiny s Denotational Semantics 4EE I m i o m I eq error m I m i o Look up an identifier return its value along with the same state that came in EE not E EE E Check Bool v s not v s Evaluate the expression make sure it is boolean and negate it EE E1 E2 EE E1 Check Num v1 s1 s1 EE E2 Check Num v2 s2 v1 v2 s2 Evaluate the first argument then the second Return their comparison and the new state EE E1 E2 EE E1 Check Num v1 s1 s1 EE E2 Check Num v2 s2 v1 v2 s2 Evaluate the arguments and return their sum with the new state v m i o Replace m I v i o CC Print E EE E v m i o m i o aug v CC if E C C EE E Check Bool Cond CC C CC C CC while E C EE E Check Bool Cond CC C while E C Dummy CC C C CC C CC C PP program C i CC C i i nil m i o o CC I E 1 1 EE E 2 2 1 1 2 2 The meaning of a program program C is a function that takes an input i computes the value of CC C applied to an initial configuration with an everywhere undefined memory the input i and a null output takes the resulting value from CC C and sends it into a function that discards everything but the output END OF DENOTATIONAL DESCRIPTION OF TINY 4 A Tiny example Let us work out a TINY example which won t be so tiny What is the meaning of PP program Print read 1 2 5 PLP Notes Tiny s Denotational Semantics 5 PP program is a function from input to output the input in our particular …


View Full Document

UF COP 5555 - NOTES ON THE DENOTATIONAL SEMANTICS OF TINY

Download NOTES ON THE DENOTATIONAL SEMANTICS OF TINY
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 NOTES ON THE DENOTATIONAL SEMANTICS OF TINY 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 NOTES ON THE DENOTATIONAL SEMANTICS OF TINY 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?