#| Lab 3. Make sure you are in ACL2s mode. Note that you can only change the mode when the session is not running, so set the correct mode before starting the session. |# (set-defunc-function-contract-strictp nil) (set-defunc-body-contracts-strictp nil) ;; Part 1: Definitions ; You have to provide definitions for the function stubs below. You ; can use auxiliary definitions, if you need them. You have to use the ; design recipe and the design guidelines presented in class. ; Make sure that the check='s and test?'s below pass. ; Provide sufficient check='s and test?'s of your own. ; Use llen for determining the length of a (true) list for this lab. (definec llen (l :tl) :nat (if (endp l) 0 (+ 1 (llen (rest l))))) (check= (llen ()) 0) (check= (llen '(1 2 3)) 3) (test? (equal (llen (list a b)) 2)) (test? (implies (and (tlp x) (tlp y)) (equal (llen (app x y)) (+ (llen x) (llen y))))) ; replace-element: All x All x TL -> TL ; (replace-element: old new l) replaces every element of l ; which is equal to old by new. (definec replace-element ...) (check= (replace-element '(2 1) '(1 2) '(1 2 (1 2) (2 1))) '(1 2 (1 2) (1 2))) (check= ...) (check= ...) (test? ...) (test? ...) (defdata lor (listof rational)) ; orderedp: lor -> Boolean ; Returns t if the input is ordered with respect to <=, ie, ; is non-decreasing and is nil otherwise. (definec orderedp ...) (check= (orderedp '(1 1 3/2 8/5)) t) (check= (orderedp '(1 3/2 13/10)) nil) (check= ...) (check= ...) (test? ...) (test? ...) ; del: All x TL -> TL ; (del e l) will delete every occurrence of e in l (definec del ...) (check= ...) (check= ...) (test? ...) (test? ...) ;; Part 2: Properties ; You partner has a number of informal conjectures. ; First, determine if they are true. ; Second, formalize them using test? and see if ACL2s agrees with you. ; Make sure the formalized conjectures pass contract checking. ; Conjecture 1: If a list is ordered, then deleting from it yields an ordered list ; True? Yes or No ; Formalize (test? ...) ; Conjecture 2: If we delete a rational from an lor, the length decreases. ; True? Yes or No ; Formalize (test? ...) ; Conjecture 3: The order of deletions does not matter. ; True? Yes or No ; Formalize (test? ...) ; Conjecture 4: Delete does not increase the length of the input list. ; True? Yes or No ; Formalize (test? ...) ; Conjecture 5: replace-element does not change the length of l ; True? Yes or No ; Formalize (test? ...) ; Conjecture 6: if old=new then replace-element returns l ; True? Yes or No ; Formalize (test? ...) ; Conjecture 7: if l is an lor, then (replace-element old new l) is an lor. ; True? Yes or No ; Formalize (test? ...) ; Conjecture 8: if l is an lor and new is a rational, then ; (replace-element old new l) is an lor. ; True? Yes or No ; Formalize (test? ...) #| We will define an interpreter for simple arithmetic expressions. An arithmetic expressions, aexpr, is one of the following: - a rational number (we use the builtin type rational) - a variable (we use the builtin type var) - a list of the form (- ) where is an arithmetic expression - a list of the form ( ) where is one of +, -, or * and both 's are arithmetic expressions. |# ; Notice that none of the operators are vars, but symbols such as ; x, y, z, etc are vars. (check= (varp '-) nil) (check= (varp '+) nil) (check= (varp '*) nil) (check= (varp '/) nil) (check= (varp 'x) t) ;; Use defdata to define boper the binary operators (defdata boper (enum ...)) (check= (boperp '*) t) (check= (boperp '^) nil) ;; Use defdata to define aexpr (defdata aexpr (oneof rational var (list '- aexpr) ...)) (check= (aexprp '((x + y) - (- z))) t) (check= (aexprp '(x + y + z)) nil) ;; An assignment is an alist from var's to rationals. ;; An alist is just a list of conses. (defdata assignment (alistof var rational)) (check= (assignmentp '((x . 1) (y . 1/2))) t) ;; This is nil because (1), (1/2) are not rationals. (check= (assignmentp '((x 1) (y 1/2))) nil) ;; Define aeval, a function that given an aexpr and an ;; assignment evaluates the expression, using the assignment ;; to assign values to var's. ;; If a var appears in the aexpr but not in the assignment, then ;; the value of the var should be 1. ;; Remember to use the "template" defdata's give rise to as per ;; Section 2.14 of the lecture notes. ;; You will need the following helper function to lookup the ;; value of v in a (remember return 1 if v isn't in a) (definec lookup (v :var a :assignment) :rational ...) (definec aeval (e :aexpr a :assignment) :rational (cond ((rationalp e) ...) ((varp e) ...) ...)) (check= (aeval '((x + y) - (- z)) '((y . 3/2) (z . 1/2))) 3) ;; Specify the following properties using aeval ;; 1. -x = -(-(-x)), for symbol x (test? ...) ;; 2. (x - y) = (x + (- y)), for vars x, y ;; Hint: the backquote/comma combo is your friend. (test? ...) ;; 3. (x * (y + z)) = ((x * y) + (x * z)), for aexpr's x, y, z (test? ...)