Flip-Flop

Purpose of exercise

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

Activities

• 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.

Requirements

• flip-flop xs) -- a list like xs, but with disjoint adjacent pairs swapped
• Example: (flip-flop (list 1 2 3 4 5 6 7)) is (list 2 1 4 3 6 5 7)

Properties

• The length of (flip-flop xs) is the same as that of xs
• Every element of xs is an element of (flip-flop xs) and vice versa
• Element 2n of xs (zero-based indexing) is element 2n+1 of (flip-flop xs) when the length of xs exceeds 2n+1
• Element 2n+1 of xs (zero-based indexing) is element 2n of (flip-flop xs) when the length of xs exceeds 2n+1