FlipFlop
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 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

flipflop xs)  a list like xs, but with disjoint
adjacent pairs swapped

Example: (flipflop (list 1 2 3 4 5 6 7)) is (list 2 1 4
3 6 5 7)
Properties
 The length of (flipflop xs) is the same as that of xs
 Every element of xs is an element of (flipflop xs) and vice versa
 Element 2n of xs (zerobased indexing) is element 2n+1 of (flipflop xs)
when the length of xs exceeds 2n+1
 Element 2n+1 of xs (zerobased indexing) is element 2n of (flipflop xs)
when the length of xs exceeds 2n+1