1. Because for a function, the interpreter has to evaluate each of the given arguments, bind the value of each to the corresponding parameter of the function and add it to the a-list being constructed. In the case of a form, what is done to the given arguments depends on the particular argument in question. So, for a form, the eval[] function looks at each form and decides the appropriate action to be taken.

2. Essentially what you need to do is change the eval[] as follows:

Main loop:
	S = input();
	… if defun, add it to dList, print msg., cont. with next iteration…
	R = eval[S, NIL];
	output(R);

evlis[list, aList]		=
		[ null[list] --> NIL;
		|	T --> cons[ eval[car[list], aList], evlis[cdr[list], aList] ] ]
evcon[be, aList]	=   // be is of form ((b1 e1) ... (bn en))
		[	null[be] --> ***exception!***
		|	eval[caar[be], aList] --> eval[cadar[be], aList];
		|	T --> evcon[cdr[be], aList] ]

...
| atom[car[exp]] -->
    		 [ eq[car[exp],QUOTE] --> cadr[exp];
		 | eq[car[exp],COND]  --> evconNew[cdr[exp], aList];
		 | T --> apply[car[exp], evlis[cdr[exp],aList], aList]  ]

where you define a new function evconNew[] as follows:

evconNew[condList, aList] =
  = [null[condList] --> "exception"
    |T --> evlisNew[cdr[condList[1]], condList, aList] ]

evlisNew[val, condList, aList] =
    [ null[condList] --> val;
    | T --> evlisNew[val, cdr[condList, aList]] ]

What does is to "save" the value of e1 so that it can be returned if all the bi's evaluate to NIL.

3. (a) is invalid because if we start in, say, the state 
   <x=1, y=2, z=3>
(assuming x, y, z is the set of program variables), this state does satisfy 
the given pre-condition, the execution will terminate immediately and the
final state (which will be <x=0, y=2, z=3>) will not satisfy false, 
the given post-condition.

(b) is valid since there are no initial states satisfying the pre-condition so it is impossible to find a counter-example to show invalidity.

(c) valid. Same reason as for (b).

(d) is valid because no matter what state you start in, the final state will be the same, except the value of x will be 0. And this state will satisfy true since every state does.

Total correctness: (a) will be invalid because the final state will not satisfy false since no state does.
(b) will be valid because the set of possible initial states that satisfies false is empty.
(c) valid for same reason as (b).
(d) invalid for same reason as (a).

4. (a) will be valid because the given statement will not terminate so there are no final states to worry about that can serve as a counterexample.
(b) will be invalid because the very first "read x;" will abort because when it tries to get head(IN), it will fail since IN is now empty.

The axiom will also be incomplete. For example, we cannot derive the following
result using the existing axiom (and the rule of conseq.):

  { in=<1> && out=<> } read x; { out=<1> }

You should be able to argue intuitively that the above result cannot be
derived. But *showing* that this result cannot be derived, especially given the
rule of consequence, is a bit involved; we will talk about that after the
midterm.

5. According to the new model of read, "read x" is essentially equivalent to the
following:

   x := head(in); out := out^head(in); in := tail(in)

So the corresponding axiom:

  {( ( p[in/tail(in)] )[out/out^head(in)] )[x/head(in)] } read x {p}

The justification of the axiom is based on the equivalence noted above.

6. Notation: In this problem, #OUT is the *length* of OUT; i.e., # essentially
denotes the length function, so #OUT is the number of elements in OUT. Also
OUT[1] is the first element of OUT, i.e., is the same as head(OUT); you can
access other elements of OUT by writing, e.g., OUT[2] etc; using head() and
tail(), you would write that as head(tail(OUT))

The given result may be derived by using the read and write axioms, the
assignment axiom, the rule of sequential composition, and the rule of
consequence. First, we derive the following:
  
  { OUT^(head(IN)+head(tail(IN)))[1] = head(IN)+head(tail(IN)) } (read axiom)
  read x;
  { OUT^(x+head(IN))[1] = x+head(IN) } (read axiom)
  read y;
  { OUT^(x+y)[1] = x+y }
  write (x+y);
  { OUT[1] = x+y }  (assignment axiom)
  z := x+y
  { OUT[1] = z }

Note that we have used the sequential composition rule several times in
the above. 

Finally, we note that:
  (#OUT = 0) ==> [OUT^(head(IN)+head(tail(IN)))[1] = head(IN)+head(tail(IN))]

Therefore, the given result follows from the rule of consequence.

7. This rule is both inconsistent and incomplete. It is inconsistent because it
will let us derive the following:
  {x=0} x:=x+1; x:= x+1 {x=1}
(from the result {x=0}x:=x+1{x=1}).

It is also incomplete because it will not let us derive the following:
  {x=0} x:=x+1; x:= x+1 {x=2}
Again, formally showing that the rule is incomplete, given the rule of consequence, 
is challenging; we will talk about that after the midterm.


This sample has too many questions ... the actual exam will probably have five 
questions.

If you have any comments or questions, please email or post on Piazza.

--Neelam