#| CS 2800 Homework 3 - Fall 2019 This homework is done in groups: instructions as per homework 02. For this homework you will use ACL2s. Technical instructions: as per homework 02, but change file names appropriately (e.g., submit hwk03.lisp instead of hwk02.lisp, etc). Instructions for programming problems: as per homework 02. |# #| 3.1. Define using defdata the type lpos of (true) lists of positive integers (integers must be strictly positive, not zero). |# ;; ANSWER: (defdata lpos ... #| 3.2. Your defdata definition above automatically generates the recognizer lposp, which checks whether a given object is a list of positive integers. Write several tests to make sure your definition of lpos is correct: |# ;; ANSWER: (check= (lposp ... (check= ... (check= ... (check= ... ... #| 3.3. Define a recognizer tllenmult3p for the set of all true lists whose length is a multiple of 3. Write several tests for your recognizer. You may have to define helper functions. As usual, write tests also for the helper functions. |# ;; ANSWER: ... #| 3.4. Define a function add-by-threes which takes as input a list of positive integers l, such that the length of l is a multiple of 3. Then add-by-threes "compresses" l by adding consecutive triples into a single sum, and outputs the list of these sums. For example, if l=(1 2 3) then the output should be the list (6). If the input is (1 2 3 4 5 6) then the output should be the list (6 15). Etc. Make sure that the constraints on the input l above are enforced by the input contract of add-by-threes. You may have to use defunc instead of definec. In this and every homework, feel free to use any answer to a previous question. For example, you can use lpos or tllenmult3p in your answer here. |# ;; ANSWER: ... #| 3.5. Let x be the output of (add-by-threes l). What do we know about x? Write everything we know about x in the answer space below. Write the conditions about x both in English, and as ACL2s code, but write everything in the comments. For example, if we know that x is a true list, write: - (tlp x) : x is a true list ;; ANSWER: ... Food for thought, this part is not graded: How strong can you make the output contract of add-by-threes? Define a new version add-by-threes-strong-output-contract that has a stronger output contract than add-by-threes. Try to make it as strong as possible. Think what you know about the output list, based on your answer above, and try to capture this knowledge in the output contract. Notes: - The input contract and body of the function should not change. - ACL2s may not be able to prove automatically your stronger version. You may have to use some of the directives below: |# ;(set-defunc-termination-strictp nil) ;(set-defunc-function-contract-strictp nil) ;(set-defunc-body-contracts-strictp nil) ;(set-guard-checking t) ;; ANSWER: ... #| 3.6. Your friend has defined the function list-delete below: (definec list-delete (l :tl i :nat) :tl (if (endp l) nil (cons (first l) (list-delete (rest l) (- i 1))))) The function is supposed to take a list l and a nat i, and delete the i-th element of l, starting from i=0. Your friend has also provided a bunch of tests: (check= (list-delete '(1) 0) '()) (check= (list-delete '(1 2 3) 2) '(1 2)) (check= (list-delete '(1 2 3) 1) '(1 3)) Is the definition of your friend correct? In particular, does it satisfy body contracts? If yes, argue why. If not, provide a counter-example and explain which contract is violated. ;; ANSWER: ... |# #| 3.7. Your other friend thinks they can do better. They rewrite the definition as follows: (definec list-delete (l :tl i :nat) :tl (if (equal i 0) (rest l) (cons (first l) (list-delete (rest l) (- i 1))))) Does this new definition satisfy body contracts? Again, provide either an argument or a counter-example with explanation. ;; ANSWER: ... |# #| 3.8. Is the last definition of list-delete above correct? That is, does it return what you would expect in all possible cases? Note that even if it satisfies the contracts, that doesn't mean it is correct. If you think it's not correct, provide a counter-example, in the form of a test which is violated by the last definition, and an explanation: ;; ANSWER: ... |# #| 3.9. If you think the last definition is not correct, how would you fix it? If there are more than one solutions, explain. |# ;; ANSWER: ... #| 3.10. Define a function tl-to-l which takes a true list l and returns a list by removing the nil terminator from l. In particular, tl-to-l should work as follows: - if l is the empty list, the result should be the empty list - if l is a list of a single element, (x), then the result should be (x . x), i.e., the terminator nil should be replaced by a copy of x - if l is a list of more than one elements, then the terminating nil should be removed. For example, the true list (1 2) should become the cons (1 . 2). The true list (1 2 3) should become (1 . (2 . 3)). Etc. You may have to define helper functions. As usual, write tests! |# ;; ANSWER: ... ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Feedback (5 points) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| Each we'll take a short survey to monitor homework difficulty and to solicit feedback. This survey is anonymous. We don't collect names, emails, etc. Each student responds individually. If you answer all mandatory questions, you get 5 points for this homework set. You report who among your team answered the survey in your homework answers, and we trust you that you reported this truthfully. Please fill out the following form (one response per team member): https://docs.google.com/forms/d/e/1FAIpQLSe4av8JCsdc_OseKPmPkwm9c6AJ2LhNC3FmrdTsPRdKi6pVWg/viewform?usp=sf_link Report here who in your team filled the form: The following team members filled out the feedback survey provided by the link above (replace the ...'s with the names of the team members who filled out the questionnaire). ... ... ... |#