Encoding integer sequences by summing adjacent pairs, modulo a given base ... and decoding them

- Practice writing equation-based programs
- Practice specifying correctness properties
- Use DrACuLa DoubleCheck for predicate-based, random testing
- Certify correctness properties using ACL2

- Define the functions required below (here are some predefined functions that you might find helpful)
- Package the functions in a book and certify it
- Define the predicates required below and package them in another book (the "predicate book")
- Express the properties stated below in DoubleCheck form, package them in another book (the "test book"), and run the tests
- Convert the properties from Double-Check form to ACL2 theorems, package them in another book (the "verification book"), and certify it

*encoding base*: an integer that is two or greater*encodable integer*: a nonnegative integer that is smaller than the encoding base*true-list*: nil or (cons x xs), where xs is a true-list

(Note: if xs is a true-list, then xs must be nil if it is an atom, and (cdr xs) must be a true-list if xs isn't an atom)

- Define a function,
*encode*, that, given an encoding base*m*and a non-empty sequence x_{0}, x_{1}, ... x_{n-1}of encodable integers, delivers the sequence of encodable integers y_{0}, y_{1}, ... y_{n-1}, with y_{i}= (x_{i}+ x_{i+1}) mod*m*, where x=_{n}*m*-1 - Define a function,
*decode*, that inverts*encode*: (decode m (encode m xs)) = xs - Define a predicate,
*basep*, such that (basep m) is true if and only if m is an encoding base - Define a predicate,
*encodable-integerp*, such that (encodable-integerp m x) is true if and only if x is an encodable integer - Define a predicate,
*encodable-listp*, such that (encodable-listp m xs) is true if and only if m is an encoding base and xs is a true-list, all of whose elements are encodable integers

- If
*m*is an encoding base and xs is a true-list of encodable integers, then (encode m xs) is a true-list of encodable integers - If
*m*is an encoding base and ys is a true-list of encodable integers, then (decode m ys) is a true-list of encodable integers - If
*m*is an encoding base and xs is a true-list of encodable integers, then (a) the last element of (encode m xs) is the difference, mod*m*, of the last element of xs and 1, and (b) the*i*-th element of (encode m xs) is the sum, mod*m*, of the*i*-th and*i*-plus-first element of xs - If
*m*is an encoding base and xs is a true-list of encodable integers, then (decode (encode xs)) = xs

- mod
- natp
- Nth

- arithmetic-3/top
- ariithmetic-3/floor-mod/floor-mod