Take-home Midterm Exam (Fall 2005)


COMP 204 Midterm Exam

Due Wed, Nov. 23 1:00 pm. when Thanksgiving break starts
This exam is open-book, open-notes, open-web, open-instructor, but closed-friends-and-classmates. Please sign a pledge here, and hand in this first page of the exam paper with your solution. Your signature signifies that you have done your own work within these guidelines.


(signature) ______________________________________________________________


(name printed) ___________________________________________________________

Overall, I want you to print this exam paper, attache your written solution to all the problems, and hand that in to me for grading. So, I want all problem solutions on paper to read.

Hand in the paper to my mailbox or office. In the paper you write, make sure you explicitly state for the problems with program parts something like "emailed attached program p1a.txt" or whatever (see special ML instructions following) so I will know to look for it and that you did not overlook the problem. There may well be other explanatory information needed for the program parts as well.

SPECIAL INSTRUCTION FOR ML PROBLEMS
In all the problems that require you to write ML code, (there is "[ML]" after the "%" in the problem header) I want a second thing, in addition to the written solution on paper. Please submit *via email* a text file that contains your code, and your test cases, so that I can run the ML interpreter without having to type in a ton of text. I want it in email, .txt file as an attachment, not as a URL pointing to the files.

For the written part, I want to see the ML code, etc that you sent in email; I also want ML interpreter output, so "use" your file, and show the execution... have the execution demonstrate via tests the correctness of your solution.

Also, put a comment at the top of each ML program telling me whether you used a Win PC version of ML, or the Unix version that I have online for the class. Oh, I guess there is a third possibility... a Linux version of the latest ML on PC.

You can send me one email for all the ML problems, but please attach a separate text file (.txt suffix please) for each problem. Name the files according to problem... such as "p1a.txt", "p2b.txt" etc...

Make the file names end in ".txt" so my mailer will auto-display the attached files too.

    ADT Specs

  1. [25%][ML]
    Consider the ADT RING of ELT informally defined as follows:

    The ring has two main kinds of activity... adding and removing elements, and reading out values. Adding and deleting are done at the end (add) and head (rem) of the ring; adding is subject to the ring being full, causing overwrite of an element in the ring. Reading out values happens from a second spot, the "next" element. Reading an element returns a value, and causes advancement of the "next" location, but does not alter the contents of the ring. Reading can continue around and around the ring endlessly even if no new elements are added or deleted. Reading starts at the head the very first time.

    The ring is always a circularly connected list (meaning reading will go from the end element back to the head element), even if it is not all slots are filled with elements. However, there is a max number of slots beyond which the ring cannot grow.

    Using Guttag's heuristic, write consistent and complete algebraic specifications for type RING. Do this by expressing the appropriate axioms as partial functions in ML, as we did for earlier assignments. Write a thorough suite of tests to convince you the behavior is correctly implemented.

    Lambda Calculus

  2. [5%] Write in Lambda notation (not ML) 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. Here, the "L" is the lambda symbol. Show each reduction (for the nonterminating one, just show the reduction until you reach a form you already had).

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

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

    [2.5%][ML] (c) Using the approach we studied for representing Lambda calculus in ML, implement your NOR function and demonstrate that it works.

  4. [5%] (d) Using Church's lambda calculus representation for non-negative integers, develop a "enext" function that will take an integer as argument, and produce the next larger even integer. Write this out in lambda notation (not ML). This function should work for no matter if the argument is even or odd. Note that "enext" will serve as a generator for even numbers if you seed it with zero.

    If you cannot get a function that works for any non-negative integer argument, at least write one that works assuming the integer argument in even.

    [2.5%][ML] (e) Implement your "enext" function in ML, using the methods we studied for representing lambda calculus in ML. Show that it works.

    Model Checking

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

    [2.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.

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

    [2.5%] (c) During execution of P, If resource R is requested, it is eventually granted; once granted, resource R is eventually released.

    [2.5%] (d) P can never execute is a way such that if resource R has been granted, it is granted again without first being released.

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

    [2.5%] (b) What are the disadvantages of Model Checking over manual correctness proof methods?

  7. [5%] Explain the sources of possible error in Model Checking. That is, what could happen in the various steps involved in using a model checker to "verify" a program that would lead you to believe that the results are not 100% guaranteed.

    Higher-Order Functional Programming

  8. [15%][ML] Write in ML a higher-order function called HOF. Make it curried.

    HOF takes three arguments -- let's call them p, f, and g. When HOF is executed on some p, f, and g, it will return a function... let's call that returned function R.

    Here is how the returned function R should behave:
    When we eventually execute function R we will give it two arguments... the first is a non-negative integer, the second can be anything. Function "p" will act like a "picker", selecting which of function "f" or "g" to apply, based on the first integer argument.

    That integer will be passed to "p" as its argument. If p returns a value greater than 1000 (or less than -1000), then R will apply "f" to the second argument. Otherwise, then R will apply "g" to the second argument.

    Demonstrate your function by creating some function p, some function f, and some function g, and explain what you expect to happen when you run the function created by your HOF on them. Show some executions to support your explanation.

  9. [5%][ML] Does ML use eager evaluation, or lazy evaluation? Write an ML funtion that will answer this question... that is, if I run the ML function it will print either "eager" or "lazy" depending on which is the correct method ML uses.