Homework #1

Due Monday, Jan 22 @ 5:00pm

1. Install ACL2 and Dracula.

   • If you run Windows, then get the Windows ACL2 installer.
   • If you run *nix, then you may have to build ACL2 yourself. Look at the ACL2 news page to help you choose a Common Lisp. On Linux, GCL is probably your best bet, and I use OpenMCL on Mac OS X.

2. Bad software kills; bad software causes large projects to fail; bad software causes mistakes with great financial repercussions. Find two examples of software gone bad and write a summary paragraph on each one. Think about these questions as you write:

   • What was the nature of the bug?
   • What harm did it cause?
   • How might it have been prevented?

   Be sure to list your references. Do not include the full text of the articles referenced when you turn in the assignment.

3. ACL2 does not provide define-struct. But we saw in class that we can represent structured data by manually defining a constructor, predicate, and selectors.

   1. What functions would DrScheme define for you when it sees the data definition

      ;; A Posn is (make-posn Number Number)
(define-struct posn (x y))

   2. Port this data definition to ACL2. That is, in ACL2, manually design those functions to represent a posn structure.

4. Using the technique you practiced in the last exercise, develop a data definition and a representation for a binary tree of numbers. One number should be contained in each branch and leaf. For example, here is an artist's rendition of one instance of a binary tree of numbers:

         5
        / \
       2   4
      / \
     8   10

   Develop functions according to these purpose statements:

   • Sum the numbers in a binary tree.

   • Flatten the binary tree into a list of numbers.

   • Sum a list of numbers.

   Formulate test cases that demonstrate that the sum of a binary tree is the same as the sum of the list of numbers obtained by flattening the tree.

   You may wish to use defconst to give names to your example trees. Look it up in Help Desk.

5. When you've finished writing your code for the previous problems, save your code and click the Start ACL2 button in the upper-right corner of Dracula. Once you have pointed it at your ACL2 installation, it will open up a second window. Go back to the main Dracula/DrScheme window and click the Admit All button. Your code should now be highlighted in green. If something is highlighted red, that probably means that you didn't follow the design recipe.

   How does ACL2 know whether your code is the product of the recipe? Stay tuned for that over the next few lectures!

   If your code is highlighted red, but you think you've followed the recipe, then show your work to the instructor!