firstN
Purpose of exercise
 Get started writing equationbased programs
 Practice specifying correctness properties
 Use DrACuLa DoubleCheck for predicatebased, 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
 truelist: nil or (cons x xs), where xs is a truelist (the
predicate truelistp tests for truelists)
Requirements

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
 Under appropriate conditions on n, k, and xs, the kth element of (firstN
n xs) is the kth element of xs
 (firstN n xs) ia a truelist when xs is a truelist
 (firstN n xs) has n or fewer elements
 (firstN n xs) has exactly n elements when xs has at least n elements
ACL2 intrinsics useful in this exercise
Notes
 firstN is an inefficient version of the intrinsic "take"
 firstN facilitates reasoning, while take facilitates computation