A1. 
Assume that each statement has an unique label. 
We use [exp, L] to denote the flow set of exp immediately after the label
L.

For each statement L:s, we have zero or more "next" statements, given by
the set next(L).

We may omit the label to indicate the flow set of that expression at any
point in the program.

Generate four types of constraints:

L: new A() ---> [new A(), L] = {A}.
L: x = e ---> [x, L] = [e, L].
L: a.foo(exp), where foo is defined in some class X as 
   
   L1: foo(id){ ... }

   then --> if X \in [a, L] => [exp, L1] \subseteq [id]

for each L
  for each L1 \in next(L)
    for each expression e, 
      if [e, L1] is not defined using above rules then
        [e, L1] \superseteq [e, L]

Solving of the constraints: Similar to 0-CFA. Just add a new function to
process equality constraints.
Process ([a,l1] = [b, l2]) -- Same as Process ([a, l1] \subseteq [b, l2]).

A2. Standard.

A3. values and types are not extended.
    
    A |- e1: int, A[x=int]|- e2: t
    --------------------------------
    ploop (x e1) e2 : unit

    Operational semantics
   
    <Store, e1> -> <Store', e1'>
    ----------------------------------
    <Store, ploop (x e1) e2> -> <Store, ploop (x e1') e2>

    <Store, ploop (x n) e2> -> <Store, {(e2[x/1], false), (e2[x/2], false) ...  (e2[x/n], false)}>

Picking any term -
    <Store, {(e1, v1), (e2, v2), ..., (ei, vi), ..., (en, vn)}>
       -> 
    <Store, {(e1, v1), (e2, v2), ..., (ei', inProgress), ..., (en, vn)}>
    assuming none of v1 ... vn is "inProgress", and any i.


Process any term
    <Store, (ei, inProgress)> -> <Store', (ei', inProgress)> 
    ---------------------------------------------
    <Store, {(e1, v1), (e2, v2), ..., (ei, inProgress), ..., (en, vn)}>
       -> 
    <Store', {(e1, v1), (e2, v2), ..., (ei', inProgress), ..., (en, vn)}>

Complete any term
    <Store, (ei, inProgress)> -> <Store', (v, done)> 
    ---------------------------------------------
    <Store, {(e1, v1), (e2, v2), ..., (ei, inProgress), ..., (en, vn)}>
       -> 
    <Store', {(e1, v1), (e2, v2), ..., (v, done), ..., (en, vn)}>


    <Store, {(v1, done), (v2, done) ... (vn, done)}> -> <Store', unit>

(This does not show strict parallelism. But it demonstrates non
deterministic execution respecting the described semantics).

A4.
The algorithm may not terminate if the underlining is not done carefully. 
for example partial evaluation of an incorrect implementation of factorial
function: 
int fact(int i){
	return i*fact (i-1);
}
will never terminate.

Some ways to ensure termination - underline carefully. Set a cutoff K, and
stop evaluating a function after a K instances.

A5:
Status = {closed, open}
Type dictionary A : maps strings to Status. The dictionary returns
"closed", if not found.

Type of each statement \in set of type dictionaries.

Simple lookup -  A |- Str : A(Str)

A |- e1 : A'      A' |- e2 -> A''
---------------------------------------------
            A |- e1; e2 : A''

A |- e: closed
-------------------------
A |- open e: A[e -> open]


A |- e: open
----------------------------
A |- close e : A[e -> closed]


A |- e : open
--------------
A |- read e: A