New User Special Price Expires in

Let's log you in.

Sign in with Facebook


Don't have a StudySoup account? Create one here!


Create a StudySoup account

Be part of our community, it's free to join!

Sign up with Facebook


Create your account
By creating an account you agree to StudySoup's terms and conditions and privacy policy

Already have a StudySoup account? Login here

Programming Language Foundations

by: Tamia Bernhard

Programming Language Foundations 22C 185

Marketplace > University of Iowa > ComputerScienence > 22C 185 > Programming Language Foundations
Tamia Bernhard
GPA 3.87


Almost Ready


These notes were just uploaded, and will be ready to view shortly.

Purchase these notes here, or revisit this page.

Either way, we'll remind you when they're ready :)

Preview These Notes for FREE

Get a free preview of these Notes, just enter your email below.

Unlock Preview
Unlock Preview

Preview these materials now for free

Why put in your email? Get access to more of this material and other relevant free materials for your school

View Preview

About this Document

Class Notes
25 ?




Popular in Course

Popular in ComputerScienence

This 5 page Class Notes was uploaded by Tamia Bernhard on Friday October 23, 2015. The Class Notes belongs to 22C 185 at University of Iowa taught by Staff in Fall. Since its upload, it has received 24 views. For similar materials see /class/228059/22c-185-university-of-iowa in ComputerScienence at University of Iowa.


Reviews for Programming Language Foundations


Report this Material


What is Karma?


Karma is the currency of StudySoup.

You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!

Date Created: 10/23/15
22C1185 Attribute Grammar Example This example illustrates the most common use of attribute grammars prototyping compilers It is adapted from B Courcelle Attribute grammars theory and applications Formalization of Programming Concepts Lect Notes in Comp Sci V107 This example concerns itself with only a small part of a compiler namely translating assignment statements In particular it focuses on the process of allocating temporary storage for the evaluation of expressions For instance in the expression abc the result of bc must first be computed and stored in some memory location d and then the addition ad performed In complicated expressions numerous intermediate results must be generated and the locations where they are stored retained for later use as appropriate This methodology is described here by means of an attribute grammar Some pool of available temporary memory locations must be assumed In order to focus on the desired issues this is taken to be the symbolic locations L0 L1 L2 Courcelle expresses the code for an assignment statement in terms of three address instructions That is the usual precedence is used to resolve the order of operations and suitable temporary locations are determined but the code is symbolically indicated to avoid computer architecture details Also temporary locations are reused when their prior use is completed For example the assignment X 314 XY will be translated into L0 314 L1 L2 L1 L1L2 L0 L0L1 X L0 This attribute grammar uses the attribute free to denote the first unused temporary memory location available the attribute res to denote the memory location used to hold the result of an expression term etc and code to denote the sequence of instructions for an assignment expression etc The semantic rules also use the function next applied to temporary memory locations with the obvious result eg nextLO L1 etc ham1 1 22C1185 BNF Semantic Rules 1ltasngt gtltidgt lteXpgt asncode expcode id expr es asnFr ee L0 expFr ee asnFr ee 2ltexpgt gtlttrmgt expcode tr39mcode expr es tr39mr39es tr mFr ee expFr ee 3ltexpgtO gtltexpgt1lttrmgt exp0code exp1code tr39mcode exp1r39es exp1 r39estr39m res exp0r39es exp1r39es exp1Fr ee exp0Fr ee tr m Fr ee nextCexp1r39es 4 lttrmgt gt ltfctgt tr mcode Fctcode tr mr es Fctr es FctFr ee tr mFr ee 5lttrmgtO gtlttrmgt1ltfctgt tr39mocode trm1code Fctcode tr mor es tr m1r esFctr es tr39mor39es tr39m1r39es tr m1Fr ee tr mOFr39ee FctFr ee nextCtr m1r39es 6ltfctgt gt lteXpgt Fctcode expcode Fctr es expr es expFr ee FctFr ee 7ltfctgt gtltidgt Fctcode FctFr ee id Fctr es FctFr ee 8ltfctgt gtltconstgt Fctcode FctFr ee const Fctr es FctFr ee The attribute grammar above omits subtraction and division operations for brevity but they would be treated entirely similarly to table entries 3 and 5 respectively The attribute dependencies in this example are rather intricate These are perhaps best depicted in terms of the associated derivation tree nodes 80 for production 1 there are the following dependencies where the arrow shows the direction of information flow ltasngt coiifrix ltidgt lteXpgt code res free ham1 9 22C1185 This indicates that code is a synthesized attribute and is dependent on res and that free is an inherited attribute If we continue this analysis for production 2 we the dependencies ltexpgt Cfde free res lttrmgt code free res These dependencies are consistent with those of production 1 Continuing with production 3 we have ltex de ee res code free res ltexpgt lttrmgt code ee res This is also consistent with the prior observations but reflects more complicated attribute interrelationships In fact using the production numbers to indicate where the dependencies arise we have the following free 78 78 35 code res 135 This suggests a potential circularity free depends on res and viceversa But in fact a more careful analysis reveals there is no actual circularity in any of the possible derivation trees The dependency of res on free is in productions 7 and 8 that correspond to leaf nodes that have no further dependencies and the potential circularity is broken by the nature of the tree structure However there is an interdependency that prevents full attribute evaluation in one pass up and down the derivation tree In fact the number of passes will depend on the depth of nesting in the expression For instance in the example tree on the next page evaluation must proceed in the following way evaluate free top down evaluate res bottom up continue evaluating free top down continue evaluating res bottom up complete evaluating free top down complete evaluating res bottom up evaluate code bottom up lmo39lthON l ham1 3 asn fL0 l I trmfLo rLo cLo314 fct fLo rLo cLo314 COl39lSt 314 exp fLO rLo trm fLo rL0 22C1185 cL1X fct fL1 rL1 L21Y L1 L1L2 c L1X exp fL1rL1 L2Y L1L1L2 exp fL1 rL1 cL1X trm fL1 rL1 cL1X fct f L1 rL1 cL1X A partially completed attribute evaluation tree ham1 4 trm fL2 rL2 cL2Y fct fL2 rL2 cL2Y 22C1185 Fall 2004 Proof Rules for Arrays Arrays We have seen that the regular Assignment Axiom is not valid for assignments involving arrays This does not preclude proving with arrays but we can t use the regular Assignment Axiom In this presentation we examine how to perform valid deductions when array assignments are permitted In fact the regular Assignment Axiom is still valid when arrays are present as long as assignment to subscripted variables is prohibited in the programs to be proven ie read only arrays It is when assignments to subscripted variables are permitted that we need to change To accomplish sound reasoning about readwrite arrays it will be shown sufficient to require assertions that treat arrays exclusively as a whole Assertions only characterize the values of array variables not element variables This is a restriction on the logical assertions not the program text Syntax Wren and Pelican for arrays is described informally Identifiers are declared to denote arrays and we refer to them as arrayidentifiers We will consider only one dimensional arrays here and we will assume that the items in an array are of type integer We will not be concerned about the subscript ranges at this point As a practical matter our assertions commonly restrict the range of subscript values The syntax denoting an array entry will be the familiar form arrayidinteger expr and subscripted variables may appear at any point where ordinary variables are allowed For this discussion we focus on the proof elements For an array value including but not restricted to a variable say a we use the notation ai e where subscript i and expression e are integers to denote the array value that is identical to a except at index i and at that position contains the value e since ai e is another array value similar notation may again be applied to it etc This notation is reserved for use in assertions not in program code The following rules are provided for array value deductions Array assignment axiom The conventional assignment axiom is forbidden for use with assignment to array elements ie subscripted variables but continues to be used for simple variables For assignment to subscripted variables we provide an additional axiom scheme Pa gt ai egt ai e P ARRAYASSIGN for any postcondition P Note that each occurrence of the arrayidentifier is to be replaced Hence each element variable ak in the postcondition P would be changed to ai ek in the precondition We also add the following auxiliary rules Array value rules ARRAYVAL m or we could write a i D ai e 2 am 7 or we could write 2 i D ai e e Note that i and are permitted to be integer expressions in these proof rules


Buy Material

Are you sure you want to buy this material for

25 Karma

Buy Material

BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.


You're already Subscribed!

Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'

Why people love StudySoup

Steve Martinelli UC Los Angeles

"There's no way I would have passed my Organic Chemistry class this semester without the notes and study guides I got from StudySoup."

Anthony Lee UC Santa Barbara

"I bought an awesome study guide, which helped me get an A in my Math 34B class this quarter!"

Jim McGreen Ohio University

"Knowing I can count on the Elite Notetaker in my class allows me to focus on what the professor is saying instead of just scribbling notes the whole time and falling behind."


"Their 'Elite Notetakers' are making over $1,200/month in sales by creating high quality content that helps their classmates in a time of need."

Become an Elite Notetaker and start selling your notes online!

Refund Policy


All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email


StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here:

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.