Q2: Steps: Use the 0-CFA to identify for each object what is the run

Q3: struct Closure {
	bool isAlreadyEvaluated;
	union {
		int val; // assuming that functions only return integers.
		int (*fp)(); // pointer to body

	}ValExp 
    } 
    int get(struct Closure sc){

	    if sc.isAlreadyEvaluated  return sc.ValExp.val;
	    tm = sc.ValExp.fp();
	    sc.ValExp.val = tm;
	    sc.isAlreadyEvaluated = true;
	    return tm;
    }

    For each function call of the form foo(e1, e2) 
	->
    For each argument ei do
    	fi = Create a new function corresponding to ei;
	  // body of fi is same as ei. args to fi -- one each for the free variables of ei.
    	sc_i = Create a new struct Closure corresponding to ei.
    	sc_i.isAlreadyEvaluated = false;
	sc_i.ValExp.fp = f1;
    emit the code "foo(sc_1, sc_2, ..)"

    In the body of the function foo -- 
    	- Change the type of each argument to struct Closure
    	- for each occurrance of the argument a_i of foo, replace it with get(a_i);
Q4. universal precondition - false, universal post condition - true

   Post condition: b*Y + X = a AND X < b
   Pre condition: a > 0 AND b > 0
   Loop invariant: (directly from the post condition) b * Y + X = a

   Rest of the triples are straight forward.

Q5: Post condition: X = x - y 
    Loop invariant: X - Y = x - y
    The rest of the triples are straightforward.
Q6: a) Treat each cell as a process, that is in an infinite loop, does the following in each iteration (=generation) 
	"receives" status of all its neighbors, computes its status and "sends" its status.
    b) require cond -> if (cond == false) {if rescue block exists -> emit {goto rescue block}. else {set a global excp and return}}
       ensure  cond -> if (cond == false) {if rescue block exists -> emit {goto rescue block}. else {set a global excp and return}}
       retry ->  keep a copy of the original arguments (using deep copy). 
                 call the function with original arguments. 
       function call return -> Check if the global variable excp is set, if so {if rescue block exists -> emit {goto rescue block}. else {set a global excp and return}}

   e) Y * X! = x!