firstN

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 functions required below (here are some predefined functions that you might find helpful)
• Package the required function in a book and certify it
• Package DoubleCheck tests for the properties stated below in another 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

Terminology

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

Requirements

1. Define a function firstN that delivers a list comprised of the first n elements of its second argument (which is  a list)
   Example: (firstN 3 (list 1 2 3 4 5 6 7)) is (list 1 2 3)

Properties

1. Under appropriate conditions on n, k, and xs, the k-th element of (firstN n xs) is the k-th element of xs
2. (firstN n xs) ia a true-list when xs is a true-list
3. (firstN n xs) has n or fewer elements
4. (firstN n xs) has exactly n elements when xs has at least n elements

ACL2 intrinsics useful in this exercise

• true-listp
• len
• natp
• Nth

Notes

• firstN is an inefficient version of the intrinsic "take"
• firstN facilitates reasoning, while take facilitates computation