#| CS 2800 Homework 7 - Spring 2019 This homework is done in groups. * 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. When done, save your file and submit it as hwk07.lisp. Make sure your Blackboard submission is valid ACL2s code. One way to check this is to download your submission from Blackboard after you've uploaded it, and check it using ACL2s. * 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. - 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. - Only add to the file. Do not remove or comment out anything pre-existing. - 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. We will deduct points for files that are not accepted by ACL2s: we sometimes ask explicitly to insert your answer in the comments, when the answer is not to be accepted by ACL2s. When asked to insert your answer in the comments, do so. - Do not submit the session file (which shows your interaction with the theorem prover). This is not part of your solution. Only submit the 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 use the following ASCII character combinations to represent the Boolean connectives: NOT ~ AND /\ or & OR \/ or + IMPLIES => EQUIV <=> XOR >< or XOR The binding powers of these functions are listed from highest to lowest in the above table. Within one group (no blank line), the binding powers are equal. This is the same as in class. |# #| DEFINITIONAL PRINCIPLE For each function definition below, check whether it is admissible, i.e., whether it satisfies all the rules of the definitional principle. If you claim admissibility, BRIEFLY 1. Explain in English why the body contracts hold. 2. Explain in English why the contract theorem holds. 3. Explain in English why the function terminates. Otherwise, identify a rule in the Definitional Principle that is violated. If you blame one of the purely syntactic rules (variable names, non-well-formed body etc), explain the violation in English. If you blame one of the semantic rules (body contract, contract theorem or termination), you must provide an input that satisfies the input contract, but causes a violation in the body or violates the output contract or causes non-termination. Remember that the rules are not independent: if you claim the function does not terminate, you must provide an input on which the function runs forever *without* causing a body contract violation: a body contract violation is not a counterexample to termination. Similarly, if you claim the function fails the contract theorem, you must provide an input on which it terminates and produces a value, which then violates the output contract. Your explanations should be brief but clear. We are not looking for a page of text per question but we also want to clearly see that you understand the function and if/what is wrong with it. Note that there is a difference between a function being admissible, as per the definitional principle, and ACL2s automatically proving that it is admissible. For instance, there are many functions that are admissible, but ACL2s will not admit them without help from the user, so don't just try ACL2s and report what it reports. |# (definec f1 (x :nat) :nat (/ x 2)) (defunc f2 (n l) :input-contract (and (natp n) (tlp l)) :output-contract (and (tlp (f2 n l)) (not (endp (f2 n l)))) (cond ((endp l) '(n)) ((equal n 0) '(0)) (t (f2 (- n 1) l)))) (defunc f3 (x y) :input-contract (and (rationalp x) (natp y)) :output-contract (and (rationalp (f3 x y))) (if (> x y) 0 (/ (* f3 x) (+ y 1)))) (definec f4 (x :nat y :nat z :nat) :nat (cond ((and (equal x 0) (equal y 0) (equal z 0)) 0) ((and (<= x y) (<= x z)) (f4 (- x 1) (- y 1) (- z 1))) ((and (<= y x) (<= y z)) (f4 (- x 1) (- y 1) (- z 1))) ((and (<= z x) (<= z y)) (f4 (- x 1) (- y 1) (- z 1))) (t 0)) ) (defdata natlist (listof nat)) (definec f5 (l :natlist) :natlist (cond ((equal (len l) 0) nil) ((equal (len l) 1) (f5 (list (+ (first l) 1)))) (t (cons (+ (first l) 1) (f5 (rest l)))))) (definec f6 (n :nat) :nat (cond ((equal n 0) 0) ((evenp n) (f6 (/ n 2))) (t (f6 (+ n 1))))) (definec f7 (n :nat) :nat (cond ((equal n 0) 0) ((equal n 2) 1) ((evenp n) (f7 (/ n 2))) (t (f7 (+ n 1))))) (definec f8 (x :nat y :pos) :nat (cond ((equal x 0) x) ((< y 2) (f8 (- x 1) x)) (t (f8 x (- y 1))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Part III: Feedback (5 points) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| Each week we will ask a few questions to monitor how the course is progressing and to solicit suggestions for improvement. Please fill out the following form. https://docs.google.com/forms/d/e/1FAIpQLScDPYhKNWn7oFPyb_9zDAECcJiKg-aYIMHKQmrWJ0d89CBq8Q/viewform?usp=sf_link Feedback is anonymous and each team member should fill out the form (only once per person). After you fill out the form, write your name below in this file, but not on the questionnaire. We have no way of checking if you submitted the file, but by writing your name below you are claiming that you did, and we'll take your word for it. The questionnaire is worth 5 points (hence the rest of the homework problems are worth 95 points). 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). --------------------------------------------- ... |#