append

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

ACL2 instrinsics and other functions useful in this exercise

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

Useful books of theorems

• arithmetic-3/top