Homework代写|Reasoning about Software代写|Type Systems and Dataflow Analysis代写|COMP503|

Reasoning about Software                                                                 January 29, 2019

Rice University                                                                          COMP 503, Spring 2018

Swarat Chaudhuri                                                                                         Homework 2

                Homework 2: Type Systems and Dataflow 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 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 | (e₁ e₂) | λx.e₁ | e₁ + e₂ | e₁ ≥ 0 | let x = e₁ in e₂ | if e₁ then e₂ else e₃

where x represents variables and c represents constants.

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 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. Define a data flow 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 questions.

(a) What is the dataflow lattice for this setting?

(b) What are the dataflow equations?

(c) Why does your analysis terminate?

(d) How do you use the information computed by your analysis to construct the two sets specified above for output to the user?

(e) How does your dataflow analysis operate on the following program, and what are the variable sets of interest for the label c in the code?

           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 identities hold:

(a) For all x, y, z,                         x H (y H z) = (x H y) H z

(b) For all x, y,                           (x H y) H x = x.