# Problem Set 3: Semantic Analysis

due: Monday, September 30

Update 9/29:
• do-until should execute until the until-expression evaluates to true
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 `Maybe`s. Lastly, add rules for a new statement `exists (v in e) s` that is like `for` but only works on `Maybe`s.