#| CS 2800 Homework 12 - 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 hwk12.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. |# #| Part A: Find invariants using the invariant game. You will use the invariant game to find invariants for some of the programs displayed in that game. For each program, you have to: (a) Come up with an invariant I. (b) Come up with the three proof obligations for I as per the lecture notes, namely, that: (1) I holds initially; (2) I is inductive; (3) I implies the guarantee. (c) State the above three proof obligations as ACL2s theorems and prove them using ACL2s. Example: Do (a), (b), (c) above for: http://invgame.atwalter.com/game/multiply answer: The invariant is: cnt<=m & res=cnt*n Proof obligations: |# ; 1. the invariant holds initially: (thm (implies (and (natp n) (natp m) (intp res) (intp cnt) (equal res 0) (equal cnt 0)) (and (<= cnt m) (equal res (* cnt n))))) ; 2. the invariant is inductive: (thm (implies (and (natp n) (natp m) (intp res) (intp cnt) (<= cnt m) (equal res (* cnt n)) (< cnt m)) (and (<= (+ cnt 1) m) (equal (+ res n) (* (+ cnt 1) n))))) ; 3. the invariant implies the guarantee: (thm (implies (and (natp n) (natp m) (intp res) (intp cnt) (<= cnt m) (equal res (* cnt n)) (>= cnt m)) (equal res (* n m)))) #| A1. Do (a), (b), (c) above for: http://invgame.atwalter.com/game/mult-by-1000 ; answer The invariant is: ... Proof obligations: |# ; 1. the invariant holds initially: ... ; 2. the invariant is inductive: ... ; 3. the invariant implies the guarantee: ... #| A2. Do (a), (b), (c) above for: http://invgame.atwalter.com/game/mult-of-6 ; answer The invariant is: ... Proof obligations: |# ... #| A3. Do (a), (b), (c) above for: http://invgame.atwalter.com/game/summation ; answer The invariant is: ... Proof obligations: |# ... #| A4. Do (a), (b), (c) above for: http://invgame.atwalter.com/game/summation2 ; answer The invariant is: ... Proof obligations: |# ... #| A5. Do (a), (b), (c) above for: http://invgame.atwalter.com/game/mult-by-add ; answer The invariant is: ... Proof obligations: |# ... #| A6. Do (a), (b), (c) above for: http://invgame.atwalter.com/game/square-times-2 ; answer The invariant is: ... Proof obligations: |# ... #| A7. Do (a), (b), (c) above for: http://invgame.atwalter.com/game/square-times-const ; answer The invariant is: ... Proof obligations: |# ... #| A8. Do (a), (b), (c) above for: http://invgame.atwalter.com/game/cube ; answer The invariant is: ... Proof obligations: |# ... #| A9. Do (a), (b), (c) above for: http://invgame.atwalter.com/game/cube2 ; answer The invariant is: ... Proof obligations: |# ... #| A10. Do (a), (b), (c) above for: http://invgame.atwalter.com/game/int-square-root ; answer The invariant is: ... Proof obligations: |# ... #| A11. Do (a), (b), (c) above for: http://invgame.atwalter.com/game/binary-product ; answer The invariant is: ... Proof obligations: |# ... #| Part B: Prove manually (without ACL2s) the invariant you found in A7. That is, prove all three proof obligations for this invariant using any of the techniques we learned in the course. ;answer We have to prove the following: ; 1. the invariant holds initially: ... ; 2. the invariant is inductive: ... ; 3. the invariant implies the guarantee: ... |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; 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/1FAIpQLSfqIl6Szx8W14xKuV31uQ41XD75g8qBmq8--WcVWYMQEmMtSw/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). --------------------------------------------- ... |#