Reasoning about Software
COMP 503, Spring
Homework 2
北美计算机作业代写 Present a type system for information ow analysis of programs in this language. Your answer should clarify the following points.
Homework 2: Type Systems and Data ow Analysis 北美计算机作业代写
Due Wednesday, February 13, 2019
Reminders
Please submit your homework on Canvas.
Collaboration is permitted, but you must write the solutions by yourself without assistance. Getting solutions from outside sources such as the Web or students not enrolled in the class is forbidden.
1.Consider the information ow type system that you studied in the paper \A Sound Type System for Secure Flow Analysis”, by Volpano, Smith, and Irvine. 北美计算机作业代写
Now suppose that you have a func-tional rather than imperative language. The grammar of programs e in the language is given by
e ::= x j c j (e1 e2) j x:e1 j e1 + e2 j e1 0 j let x = e1 in e2 j if e1 then e2 else e3
where x represents variables and c represents constants.
Present a type system for information ow analysis of programs in this language. Your answer should clarify the following points. 北美计算机作业代写
(a)What is the form of a type judgment in this setting?
(b)What does a type environment look like?
(c)Does the grammar of the language need to be augmented with additional type annotations? Recall that while type-checking the -calculus, we needed to add a type annotation to the input variable x in -terms.
(d)What are the typing rules? Please present the rules formally, and also write a sentence or two explaining each rule.
2.De ne a data ow analysis that can be used to compute two sets of variables for each statement in a program: 北美计算机作业代写
those which are de nitely not de ned before use, and those which may not be de ned before use. These sets can be used to provide extra error checking of programs. Your answer should answer the following questions.
(a)What is the data ow lattice for this setting?
(b)What are the data ow equations?
(c)Why does your analysis terminate?
(d)How do you use the information computed by your analysis to construct the two sets speci ed above for output to the user? 北美计算机作业代写
(e)How does your data ow analysis operate on the following program, and what are the variable sets of interest for the label c in the code?
1
s := 0
while (i < n) { s := s + i
i := i + 1
}
- Consider any lattice L = (S; v; t; u) where S is a set, v is a partial order, and t and u are respectively the join and meet operators. Show that the following identities hold:
(a)For all x, y, z, 北美计算机作业代写
x t (y t z) = (x t y) t z
(b)For all x, y,
(x t y) u x = x:
更多代写：北美金融代写 雅思代考 英国经济学网课代修 英语Essay太难写代写教你 英语研究论文Research Paper代写 留学生代考被抓
