Show how the tree might be type-checked

Assignment Help Programming Languages

Reference no: EM131906

1. Consider the following attributed tree grammar for type checking a program AST. For simplicity, it hard codes, declarations for "X" and "Y", the identifier "X" and "Y", and the constants 2 and 3. Note also, that it encodes lists of declarations and lists of statements by simply having each declarations/statements last child be the next declaration.

start: start ::= declarations statements

^ statements.env = declarations.env

^ start.type_ok ::= statements.type_ok

decl_stop: declarations ::= Îμ

^ declarations.env = nil

decl_x_int: declarations1 ::= declarations2

^ declarations1.env = <X, INT, declarations2>

decl_y_int: declarations1 ::= declarations2

^ declarations1.env = <Y, INT, declarations2>

decl_x_bool: declarations1 ::= declarations2

^ declarations1.env = <X, BOOL, declarations2>

decl_y_bool: declarations1 ::= declarations2

^ declarations1.env = <Y, BOOL, declarations2>

stmt_stop: statements ::= Îμ

^ statements.type_ok = true

stmt_if: statements1 ::= expr statements2 statements3 statements4

^ statements1.type_ok = (expr.type == BOOL)

and statements2.type_ok

and statements3.type_ok

and statements4.type_ok

^ expr.env = statements1.env

^ statements2.env = statements1.env

^ statements3.env = statements1.env

^ statements4.env = statements1.env

stmt_writeint: statements1 ::= expr statements2

^ statements1.type_ok = (expr.type == INT) and statements2.type_ok

^ expr.env = statements1.env

^ statements2.env = statements1.env

<: expr1 ::= expr2 expr3

^ expr1.type = if expr2.type == INT and expr3.type == INT then BOOL else ERR

^ expr2.env = expr1.env

^ expr3.env = expr1.env

+: expr1 ::= expr2 expr3

^ expr1.type = if expr2.type == INT and expr3.type == INT then INT else ERR

^ expr2.env = expr1.env

^ expr3.env = expr1.env

*: epxr1 ::= expr2 expr3

^ expr1.type = if expr2.type == INT and expr3.type == INT then INT else ERR

^ expr2.env = expr1.env

^ expr3.env = expr1.env

2: expr ::= Îμ

^ expr.type = INT

3: expr ::= Îμ

^ expr.type = INT

id_x: expr ::= Îμ

^ expr.type = lookup(X, expr.env)

id_y: expr ::= Îμ

^ expr.type = lookup(Y, expr.env)

With the auxilary function lookup:

lookup(X, env) = if env = nil

then ERR

else let <Y, n env2> = env in

if Y = X then n else lookup(X, env2)

end

(a) Of the attributes, declarations.env, statements.env, statements.type_ok, expr.env, and expr.type, which are inherited? Which are synthesized?

(b) Is the grammar L-attributed?

start

+-decl_x_int

| |

| +-decl_y_bool

| |

| +-decl_stop

+-stmt_if

+-<

| |

| +-id_x

| |

| +-3

+-stmt_write

| |

| +-id_y

| |

| +-stmt_stop

+-stmt_stop

Show how the tree might be type-checked. Annotate the nodes in the tree with numbers indicating the order in which you calculated them? Below, using the same numbering, show the attribute values computed at each step of the evaluation.

(d) Is there a type error in the program represented by this AST? If so, what is it?

2. Consider the TL13' type rules in the posted lecture notes.

(a) Derive a proof tree showing that the following program is well-typed according to those rules:

program begin while true do writeInt 25 ; end ; end

That is, the judgement:

[] |- program begin while true do writeInt 25 ; end ; end

(b) Derive a proof tree justifying the judgement that following statement sequence is well-typed under the

environment [][x -> int][b -> bool]:

while b do writeInt x end ;

That is, the judgement:

[][x -> int][b -> bool] |- while b do writeInt x end ;

(c) Attempt to derive proof tree for the judgment [][x -> bool] |- x * 5 + 2 : int. What premise cannot be satisfied because it doesn't match any rule? Show your incomplete tree circling the unjustified leaf premise (at the top of the tree)

Reference no: EM131906

Questions Cloud

Using the annual statistics create an excel plot : Using the annual statistics create an Excel plot with standard deviation (volatility) on the x-axis and average return on the y-axis

Design a dedicated datapath : Design a dedicated datapath

Prepare a set-list for a social gathering : Prepare a set-list for a social gathering

Quantitative analysis for decision making class : Quantitative analysis for decision making class

Show how the tree might be type-checked : Attempt to derive proof tree for the judgment Show how the tree might be type-checked

Determine the inorder, preorder and postorder traversal : Determine the Inorder, preorder and postorder traversal

Prepare the required journal entry : Prepare the required journal entry to record the tax expense

What factors reduce the capacity of the organization : What factors reduce the capacity of the organization to get its objectives?

Prepare a complete cash flow statement : Prepare a complete cash flow statement for the year ending December 31, 2013 using the indirect method. The statement must include all titles, headings, captions, sections, totals, subtotals and disclosures one would normally expect on the face o..

User Account

All Pages