Purpose of exercise
Get started writing equation-based programs
Practice specifying correctness properties
Use DrACuLa DoubleCheck for predicate-based, random
Certify correctness properties using ACL2
- Define the following function
- Package the function you define as a book.
- DoubleCheck the properties stated below
- Use ACL2 to prove the properties
- Package the theorems as a book.
- Appending the two lists in the list delivered by split reproduces its
- Both of the elements of the list delivered by split are true-lists if its
second argument is a true list
- The sum of the lengths of the two lists delivered by split is the length
of its second argument
The following intrinsic ACL2 functions will be useful in
- (length xs)
- (true-listp xs)
- You probably will need to look at some details of ACL2 proof attempts and
apply The Method
- You may find it useful to put use-instance hints in some theorems.