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.
(concat xss) -- elements of the list xss (which are,
themselves, lists) concatenated, forming a single list
Example: (concat (list 1 2 3) (list 4 5 6 7) (list 8 9) is the list (1 2 3 4
5 6 7 8 9)
- The length of the list delivered by concat is the sum of the lengths of
the lists in its argument
- Prove the laws of conservation for concat. That is, prove the following
1. Any element in a list in the argument of concat is an element of
the list concat delivers.
2. Any element in the list concat delivers is an element of one of
the lists in its argument.
The following intrinsic ACL2 functions will be useful in
- (length xs)
- (member-equal x xs)
- (true-list-listp xss)
To state the necessary predicates, it will be helpful to define the
- (sum-of-lengths xss) -- the sum of the lengths of the lists in xss
- (member-some x xss) -- true if and only if x is an element of at least
one of the lists in xss.