Fall 2013

**due**: Monday, September 30

Update 9/29:

- do-until should execute until the until-expression evaluates to true

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.`if (x + 2 == 4) return x;`

`x := 0; while (f(x,y)) x := x + f(y,x);`

`return [b, get`

([3, f], y)];

In context Ψ = ∅ and Θ =

`A`

,`B`

, show the full typing derivation proving that`Iterable<A&B>`

is a subtype of`Iterable<A>&Iterable<B>`

.- 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 safex := 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. (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`[`

be*e*]`Maybe`

s. Lastly, add rules for a new statement`exists (`

that is like*v*in*e*)*s*`for`

but only works on`Maybe`

s.