In-class (Fall 2002)

Lambda Calculus

1. [20%] (a) Using Church's representation for the boolean type, develop an XOR function in lambda calculus. Write this out in Lambda notation (not ML).

   [10%] (b) Using your definition, show a full manual reduction for (T XOR F).

2. [5%] Write a lambda expression that reduces to "L a L b (a (b a))" when reduced by normal order but does not have a terminating reduction when reduced in applicative order.

   Model Checking

3. Write CTL formulae to express these properties of a program P:

   [5%] (a) It is possible during execution of P for variable k to be less than 0, but it only happens immediately after k was exactly 0.

   [5%] (b) During execution of P, it never happens that k becomes greater than 100 and later returns to being less than 100.

   [5%] (c) If resource R is requested, it is eventually granted; and, once granted, resource R is eventually released.

4. [10%]Why was Clark's algorithm for checking CTL formulae an important advancement in the early days of model checking?

5. [5%] (a) What are the advantages of Model Checking over manual correctness proofs for program verification?

   [5%] (b) What are the disadvantages of Model Checking over manual correctness proofs for program verification?

   ADT Specs

6. [30%] Consider the type Double Ended Stack (DES):

      new    :    -> DES
      pushL  : DES x ELT --> DES
      pushR  : DES x ELT --> DES
      popL   : DES       --> DES
      popR   : DES       --> DES
      topL   : DES       --> ELT
      topR   : DES       --> ELT
      empty  : DES       --> boolean
      size   : DES       --> int
   

   Using Guttag's heuristic, write axioms specifying the behavior of this type. It is basically two stacks glued together "back to back" at their bases. You can push and pop on either end, and you can inspect the top item on each end (without removing it). You can also tell if the entire stack is empty. Note that the following sequence of operations is fine:

      topR(popR(topR(popR(topR(pushL(pushL(pushL(new(),1),2),3))))))
   

   and will produce the items 1, 2, 3 out in that order. We pushed the items onto the Left end, but popped them off the Right end... no problem. In this case, we got FIFO order out of the DES (very queue-like).