CS 4120: Introduction to Compilers
Fall 2013

Problem Set 3: Semantic Analysis

due: Monday, September 30

Update 9/29:
  1. For each of the following Cubex statements, give typing contexts Δ and Γ (assume Ψ=Ψ0 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.