Split

Purpose of exercise

• Get started writing equation-based programs
• Practice specifying correctness properties
• Use DrACuLa DoubleCheck for predicate-based, random testing
• Certify correctness properties using ACL2

Activities

• Define the following function
• Package the function you define as a book.
• DoubleCheck the properties stated below
• Use ACL2 to prove the properties
• Package the theorems as a book.

Requirements

• (split n xs) -- delivers (list prefix suffix) where prefix is the first n elements of xs and suffix is the remaining elements
  Example: (split 3 (list 1 2 3 4 5 6 7)) is (list (list 1 2 3) (list 4 5 6 7))

Properties

• Appending the two lists in the list delivered by split reproduces its second argument
• Both of the elements of the list delivered by split are true-lists if its second argument is a true list
• The sum of the lengths of the two lists delivered by split is the length of its second argument

Notes

The following intrinsic ACL2 functions will be useful in this problem

• (length xs)
• (true-listp xs)

Notes:

• You probably will need to look at some details of ACL2 proof attempts and apply The Method
• You may find it useful to put use-instance hints in some theorems.