Blocks

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

• (blocks n xs) -- repackage xs as a list of n-element contiguous segments of xs so that (concat (blocks n xs)) is the same as xs
  Example: (blocks 3 (list 1 2 3 3 4 5 6 7 8)) is ((list 1 2 3) (list 4 5 6) (list 7 8))

Properties

• All of the elements in (blocks n xs) are true lists
• Prove that if xs has n or more elements, then the first element of (blocks n xs) has exactly n elements
• Prove that if xs has mn or more elements, then each of the first m elements of (blocks n xs) have exactly n elements
• Prove that (concat (blocks n xs)) reproduces xs

Notes

The following intrinsic ACL2 functions will be useful in this problem

• (length xs)
• (true-listp xs)
• (true-list-listp xss)

You may find it helpful to define the following functions

• (split n xs) -- delivers (list prefix suffix) where prefix is the first n elements of xs and suffix is the remaining elements
• (concat xss) -- elements of the list xss (which are, themselves, lists) concatenated, forming a single list