Reasoning about Software January 29, 2019
Dataflow Analysis代写 Collaboration is permitted, but you must write the solutions by yourself without assistance. Getting solutions from outside sources
Rice University COMP 503, Spring 2018
Swarat Chaudhuri Homework 2 Dataflow Analysis代写
Homework 2: Type Systems and Dataflow Analysis Due Wednesday, February 13, 2019
Reminders Dataflow Analysis代写
- Please submit your homework on
- 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 flow 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 | c | (e1 e2) | λx.e1 | e1 + e2 | e1 ≥ 0 | let x = e1 in e2 | if e1 then e2 else e3
where x represents variables and c represents constants.Dataflow Analysis代写
Present a type system for information flow analysis of programs in this language. Your answer should clarify the following points.
(a)What is the form of a type judgment in thissetting?
(b)What does a type environment looklike?
(c)Doesthe 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
2.Define a data flow analysis Dataflow Analysis代写
that can be used to compute two sets of variables for each statement in a program: those which are definitely not defined before use, and those which may not be defined before use. These sets can be used to provide extra error checking of programs. Your answer should answer the following
(a)What is the dataflow lattice for thissetting?
(b)What are the dataflowequations?Dataflow Analysis代写
(c)Why does your analysisterminate?
(d)How do you use the information computed by your analysis to construct the two sets specified above for output to theuser?
(e)How does your dataflow analysis operate on the following program, and what are the variable sets of interest for the label c in thecode?
s := 0
c: while (i < n) { s := s + i
i := i + 1
}
3.Consider any lattice L = (S, ±, H, H) where S is a set, ± is a partial order,
and H and H are respectively the join and meet operators. Show that the following identitieshold:
(a)For all x, y,z,
x H (y H z) = (x H y) H z Dataflow Analysis代写
(b)For all x,y,
(x H y) H x = x.Homework
其他代写:algorithm代写 analysis代写 app代写 assembly代写 assignment代写 C++代写 code代写 course代写 dataset代写 java代写 java代写 web代写 北美作业代写 编程代写 考试助攻 北美作业代写 program代写