## 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.