#| 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 |#