### Purpose of exercise

• Practice specifying correctness properties
• Use DrACuLa DoubleCheck for predicate-based, random testing
• Learn about importing books of theorems to support the theorem proving process
• Certify correctness properties using ACL2

### Activities

• Package DoubleCheck tests for the properties stated below in a book (the "test book"), and run some tests
• Convert the DoubleCheck predicates to ACL2 theorems, package them in another book (the "verification book"), and certify it
• Here are some predefined functions that you might find helpful

### Terminology

• true-list: nil or (cons x xs), where xs is a true-list (the predicate true-listp tests for true-lists)

### Properties

1. The first (length xs) elements of (append xs ys) is xs
2. (append xs ys) without its first (length xs) elements is ys
3. The length of the list append delivers is the sum of the lengths of its arguments
4. Appending the first n elements of a list with its elements beyond the first n reproduces the list

• true-listp
• len
• natp
• NthCdr
• firstN

### Useful books of theorems

• arithmetic-3/top