#| CS 2800 Homework 2 - Fall 2019 This homework is done in groups. (Doing the homework in groups does not mean you split the problems among members of the group. EVERY member of the group should try to do ALL problems. Then you meet and compare notes. Help each other. If you cannot solve a problem, ask your team mates, but only after you tried it yourself.) * Groups should consist of 2-3 people. * One group member will create a group in BlackBoard. See the class Webpage for instructions on how to do that. * Other group members then join the group. * Homework is submitted by only one person per group. Therefore make sure the person responsible for submitting actually does so. If that person forgets to submit, your team gets 0. - We recommend that groups email confirmation messages and submit early and often. * Submit the homework file (this file) on Blackboard. Do not rename this file. There will be a 10 point penalty for this. * You must list the names of ALL group members below, using the given format. This way we can confirm group membership with the BB groups. If you fail to follow these instructions, it costs us time and it will cost you points, so please read carefully. The format should be: FirstName1 LastName1, FirstName2 LastName2, ... For example: Names of ALL group members: Frank Sinatra, Billy Holiday There will be a 10 pt penalty if your names do not follow this format. Replace "..." below with the names as explained above. Names of ALL group members: ... * Later in the term if you want to change groups, the person who created the group should stay in the group. Other people can leave and create other groups or change memberships. See the class Webpage. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; For this homework you will need to use ACL2s. Technical instructions: - Open this file in ACL2s as hwk02.lisp - Make sure you are in ACL2s mode. This is essential! Note that you can only change the mode when the session is not running, so set the correct mode before starting the session. - Insert your solutions into this file where indicated (usually as "..."). Sometimes we require textual explanations (e.g., complexity analysis below) so just add your explanation inside the ACL2s comments. - Make sure the entire file is accepted by ACL2s. In particular, there must be no "..." left in the code. If you don't finish all problems, comment the unfinished ones out. Comments should also be used for any English text that you may add. This file already contains many comments, so you can see what the syntax is. - Only add to the file. Do not remove or comment out anything pre-existing (except the ..., which you will replace with your answers). - When done, save your file and submit it as hwk02.lisp - Do not submit the session file (which shows your interaction with the theorem prover). This is not part of your solution. Only submit this lisp file. Instructions for programming problems: For each function definition, you must provide both contracts and a body. You must also ALWAYS supply your own tests. This is in addition to the tests sometimes provided. Make sure you produce sufficiently many new test cases. This means: cover at least the possible scenarios according to the data definitions of the involved types. For example, a function taking two lists should have at least 4 tests: all combinations of each list being empty and non-empty. Beyond that, the number of tests should reflect the difficulty of the function. For very simple ones, the above coverage of the data definition cases may be sufficient. For complex functions with numerical output, you want to test whether it produces the correct output on a reasonable number of inputs. Use good judgment. For unreasonably few test cases we will deduct points. We will use ACL2s' check= function for tests. This is a two-argument function that rejects two inputs that do not evaluate equal. You can think of check= roughly as defined like this: (defunc check= (x y) :input-contract (equal x y) :output-contract (equal (check= x y) t) t) That is, check= only accepts two inputs with equal value. For such inputs, t (or "pass") is returned. For other inputs, you get an error. If any check= test in your file does not pass, your file will be rejected. The problems below are numbered 2.1, 2.2, etc. When you ask questions (in class, in piazza, at office hours, etc) tell us which problem you are talking about. For example, you can start your question as follows "In problem 2.x of homework 2, I don't understand what ... means ...". Since this is our first programming exercise, we will simplify the interaction with ACL2s somewhat. Instead of requiring ACL2s to prove termination and contracts, we allow ACL2s to proceed even if a proof fails. However, if a counterexample is found, ACL2s will report it. See section 2.17 of the lecture notes for more information. This is achieved using the following directives (do not remove them): |# (set-defunc-termination-strictp nil) (set-defunc-function-contract-strictp nil) (set-defunc-body-contracts-strictp nil) #| Also, if ever you have trouble getting your function admitted by ACL2s because of contract violations, not being able to prove termination, etc, try to see if you can get your function admitted in "program mode". Insert this directive :program before your function. You can return to logic mode by inserting :logic |# #| Function definitions with contracts. You already took a fantastic course on programming (CS2500), and have seen how to define functions in a functional programming style. One new thing in CS2800 is contracts. The goal of this homework is to get you use to writing functions with contracts. Make sure you give yourselves enough time to develop solutions and feel free to define helper functions as needed. |# #| 2.1. Define the function multnat that multiplies two natural numbers. The signature of the function is given: multnat: Nat x Nat -> Nat |# ;; ANSWER (definec multnat ... ...) (check= (multnat 1 2) 2) (check= (multnat 3 134) 402) (check= (multnat 1000 0) 0) #| 2.2. Stop and think: what should happen if you try the following? (check= (multnat -1 2) -2) Why should this happen? Try it in ACL2s and confirm that this is indeed what happens. Answer what happens with your explanation below: ANSWER: ... |# #| 2.3. Define a function called "division" that divides two integers. You have to figure out what the output contract is. Also pay attention to the input contract. You may have to use defunc instead of definec. Test your function especially with corner cases, to make sure it is correct. |# ;; ANSWER: ... #| This part of the homework is ungraded, and is included for you to practice. Look at each line below. Think: is it a valid expression? (i.e., can it be evaluated in ACL2s?). If you think it's valid, predict what the resulting value will be. If not, explain why it's not valid. Although this part will not be graded, you should still do it, to make sure you understand the syntax and semantics of ACL2s. This is important. You want to start by mastering the basics, so as not to have problems later. Also, we may ask these or similar questions in quizzes. (if t 0) (if t 0 "hello") (if nil 0 "hello") (if nil (if t 0) 0) (and) (and "hello") (and "hello" 0) (or "hello" 0) (implies "hello" 0) (implies 0 "hello") (implies 7 9) (implies 7 nil) (implies nil "hello") (cons 1 2) (cons 1 nil) (cons nil) (cons 1 2 nil) (list 1 2 nil) (list 1 2) (equal (list 1 2) (list 1 2 nil)) (cons (list) (list)) (cons list list) (cons (list) list) (cons list (list)) (cons (list) nil) (equal (cons (list) nil) (cons (list) (list))) (equal (cons 1 nil) (list 1)) (cons 1 "hello") (list 1 "hello") |# #| This part is still ungraded. For each object below, think and decide whether or not it is: (a) a cons; (b) a list; (c) a true list. (1 2) (1 . 2) (1 2 nil) (1 2 . nil) |# ;; ANSWER: #| 2.4. Define a function add-number-to-list-v1 which takes a true list l and a rational number x, and adds x to each element of l, whenever such an addition makes sense (i.e., whenever that element of x is a number). For this version v1 of the definition, you are requested to use definec, so as to have input and output contracts that are simple types. Do not forget to add tests! |# ;; ANSWER: (definec add-number-to-list-v1 ... (check= (add-number-to-list-v1 (list 1 2 3) -1) ... (check= (add-number-to-list-v1 (list 1 nil 3) -1) ... (check= (add-number-to-list-v1 (list nil nil "hello") -1) ... ... #| 2.5. Define a function add-number-to-list-v2. This is version v2 of the above function. The difference is that version v2 has a stronger output contract than version v1. In particular, think what more is known about the length of the output list and its relation to the length of the input list. Express that relation in the output contract. You may have to use defunc instead of definec to define version v2. |# ;; ANSWER: ... #| 2.6. Define a function add-number-to-list-v3. This is version v3 of the above functions. The difference is that version v3 has a stronger input contract than version v2. In particular, we want to enforce that the input list l only contains numbers. One way to do this is using data types, but we haven't learned about defining data types yet (defdata) so don't use that. Instead, you may want to define a helper function that checks whether a given list contains only numbers. Then use your helper function in the input contract of version v3. Note: whenever you define helper functions, you have to add tests for those helper functions too. |# ;; ANSWER: ... #| 2.7. Compare the bodies of implementation versions v2 and v3 above. Are the bodies of the two functions the same? If yes, define a new version, add-number-to-list-v4, which improves version v3 by eliminating "dead code", that is, code which is guaranteed never to be executed. |# ;; ANSWER: ...