#|

In this lab we will review the sample exam.  Solutions to the practice
exams and exams will not be distributed during the lab, nor will they
be posted anywhere; if you have questions, go to the lab.

Since the practice exam was from a previous semester and there are
difference between definitions, below we include a text version of the
sample exam that is based on the definitions we have seen this
semester. If you have difficulty making out some of the symbols, refer
to the pdf version.

|#

#|

Question 1: ACL2 Programming

This question asks you to write ACL2 functions. For each function
definition, you must provide both contracts and a body. You must also
supply test cases, in addition to the tests provided. Your test cases
must take into consideration the data definitions of the involved
types. For instance, if an argument is a list, you must test the case
that the list is empty. Use check= to specify the expected output of
your test, as shown in the examples.

The following data definition introduces the type “list of naturals”,
along with a recognizer Natlistp for that type:
|#

(defdata Natlist (listof Nat))

#|

(a) Define an ACL2 function inc-all : Nat x Natlist -> Natlist that
takes a number i and a natlist l and adds i to every object in l, if
any.

(check= (inc-all 1 ’(1 2 3)) ’(2 3 4)) 

Provide two more tests, according to the guidelines stated above.  

|#

...
    
(check= (inc-all 1 '(1 2 3)) '(2 3 4))

#|

(b) Define an ACL2 function positions : All x TL -> TL that takes an
object x and a TL l and returns the list of positions where x occurs
in l, if any. As always, position counting starts from 0.

|#

...

(check= (positions 'x '(1 2 x 2 1)) '(2))
(check= (positions  1 '(1 2 3 2 1)) '(0 4))

#|

Provide two more tests, according to the guidelines stated
above. Hint: use inc-all from part (a).

|#

#|

Question 2: Contracts and Termination

Consider the following function definition template f, in which C, X,
Y and Z are placeholders.

(defunc f (a b)
  :input-contract (and (integerp a) (tlp b))
  :output-contract C
  (cond (X       (len b))
        ((> a 0) Y)
        (t       Z)))

The following problems provide a substitution σ and ask you to
identify reasons why the function obtained by applying σ to the
function template f is rejected by ACL2s. In each case, give an input
that satisfies the input contract but demonstrates the violation
causing rejection. Explain the violation.

Writing down f|σ explicitly will be helpful.

1. σ = ((C (posp (f a b))) (X (consp b)) (Y (f (- a 1) b)) (Z (f (- a 1) b)))

Show that f|σ may fail to terminate.

...

2. σ = ((C (natp (f a b))) (X (consp b)) (Y (f (- a 1) b)) (Z (f a (tail b))))

Show that f|σ may cause body contract violations.

...

3. σ = ((C (posp (f a b))) (X (equal a 0)) (Y (f (- a 1) b)) (Z (f (+ a 1) b)))

Show that f|σ may cause output contract violations. Think carefully
what kind of input you have to give to demonstrate this.

...

|#

#|

Question 3: Satisfiability

Decide whether the following formulas are satisfiable, falsifiable,
valid, or unsatisfiable. Recall that more than one of these four
characterizations will apply; give them all. You can use any means to
derive your answer, including truth table, simplifications, proof by
case analysis, and even “assignment guessing” to show satisfiability
or falsifiability. However, for satisfiable/falsifiable formulas, you
must in the end show a satisfying/falsifying assignment (a truth table
will do).

(a) 
(a ⇒ b) ∧ (¬a ⇒ c) ⊕ (a ∧ b) ∨ (¬a ∧ c) 

...

(b) 
   (x ⇒ y) ∧ z ∧ ¬(y ⇒ x)

...

(c)
(p ⇒ q) ∧ (r ⇒ s) ∧ (p ∨ r) ⇒ (q ∨ s)

....

|#

#|

Question 4: Quick and Tidy

For the following claims, decide whether they are true or false, and
justify your answer. For a false claim, a counterexample suffices as
justification. For each part we have set aside several points for the
justification, so wild guessing is of limited value.

(a) Let f be a Boolean formula. If f is neither valid nor
unsatisfiable, then f is both satisfiable and falsifiable.

...

(b) It is impossible to define and admit (in :logic mode) an
ACL2s function with one argument x whose input contract is (natp x)
and whose output contract is nil.

...

(c) Let f and g be Boolean formulas such that exactly one of f, g is
satisfiable, and both are falsifiable. Then both f ≡ g and f ⊕ g are
satisfiable.

...

(d) For any formula g and any substitution σ, g is valid if and only
if the formula g|σ is valid.

...

(e) Let f and g be Boolean formulas such both f ≡ g and f ⊕ g are
satisfiable. Then exactly one of f, g is satisfiable.

...

(f) Let f be a recursively defined ACL2s function of one argument, and
x an input that satisfies f’s input contract. Function f terminates on
input x if and only if the set of distinct arguments f is called on
recursively while evaluating (f x) is finite.

...
|#


#|

Question 5: Equational Reasoning

Consider the following two function definitions:

(defunc mem (x l)
  :input-contract (tlp l)
  :output-contract (booleanp (mem x l))
  (cond ((endp l)            nil)
        ((equal x (first l)) t)
        (t                   (mem x (rest l)))))

(defunc concat (h l)
  :input-contract (and (tlp h) (tlp l))
  :output-contract (tlp (concat h l))
  (if (endp h)
    l
    (cons (first h) (concat (rest h) l))))

1. Prove the following conjecture using equational reasoning:

(tlp l) => ( (consp l) => (mem x l) = (x = (first l)) \/ (mem x (rest l)) ) 

Hint: use the fact that cond is defined as a special structure of
nested ifs, and that ACL2s’ or, which is equivalent to the Boolean \/,
can be defined via if. 

...

QED


2. Prove the following conjecture using equational reasoning:

(implies (and (tlp h)
              (consp h)
              (tlp l)
              (equal (mem x (concat (rest h) l))
                     (or (mem x (rest h))
                         (mem x l))))
         (equal (mem x (concat h l))
                (or (mem x h)
                    (mem x l))))

If you use existing theorems in your proof, justify that via an
appropriate substitution.

...

QED
|#