CS 4120: Introduction to Compilers
Fall 2013

Problem Set 3: Semantic Analysis

due: Monday, September 30

1. For each of the following Cubex statements, give typing contexts Δ and Γ (assume Ψ=Ψ₀ and the other contexts are empty) in which it type checks with some return type and outgoing context, or else explain why it can't be done.

   1. if (x + 2 == 4) return x;
   2. x := 0; while (f(x,y)) x := x + f(y,x);
   3. return [b, get([3, f], y)];

2. In context Ψ = ∅ and Θ = A, B, show the full typing derivation proving that Iterable<A&B> is a subtype of Iterable<A>&Iterable<B>.

3. Suppose that Cubex is extended with a new “do-until” statement:
   

       do s until (e)

   The do-until statement executes the statement s until afterwards e evaluates to true. In particular, s is evaluated at least once, and is always evaluated by the time e is evaluated. Consequently, the following program is safe

       x := 0;
       do {
         y := x + 1;
         x := y + 1;
       } until (x * y > 100)
       return integerToString(x * y);

   and produces the string “132”.

   Give a suitable type rule for do-until extending the Cubex specification for statements without returns.

4. (CS 5120 only) A common pattern in Cubex is to have iterables that are either empty or singleton. Extend the various typing and validity rules so that Cubex has a new type Maybe<T> that is a subtype of Iterable<T> and covariant with respect to T. There should be special rules making [] and [e] be Maybes. Lastly, add rules for a new statement exists (v in e) s that is like for but only works on Maybes.