EveryOther
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 following functions
 Package the functions you define as a book.
 DoubleCheck the properties stated below
 Use ACL2 to prove the properties
 Package the theorems as a book.
Requirements

(everyother xs)  every other element of xs, starting
with the first

(everyodd xs)  every other element of xs, starting
with the second

(shuffle xs ys)  elements come from xs then ys then
xs ... extra elements appended to end of list
Example: (shuffle (list 1 2 3 4 5) (list 6 7 8)) is (list 1 6 2 7 3 8 4 5)
Properties
 The sum of the lengths of (everyother xs) and (everyodd xs) is the
length of xs
 Every element in (everyother xs) is an element of xs
 Every element in (everyodd xs) is an element of xs
 (shuffle (everyother xs) (everyodd xs)) is xs
 Element n of (everyodd xs) (zerobased indexing) is element 2n of xs when the length of xs
exceeds 2n
 Element n of (everyodd xs) (zerobased indexing) is element 2n+1 of xs when the length of xs
exceeds 2n+1
Potentially useful ACL2 intrinsic functions
 (length xs)
 (truelistp xs)
 (memberequal x xs)
 (nth n xs)
 (natp n)
 (<= m n)