Pattern Search - FAQ

Purpose of exercise

• Practice writing equation-based programs
• Practice specifying correctness properties
• Use DrACuLa DoubleCheck for predicate-based testing
• Certify correctness properties using ACL2, including the use of lemmas and hints
• Practice using ACL2 file i/o

Activities

• Define the required functions, package them in a book, and certify it
• Define the predicates needed to express the required properties, package them in a book (...-prd), and certify it
• Define DoubleCheck tests for the required properties, package them in a book (...-tst), certify it, and run the tests
• Define theorems expressing the required properties, package them in a book (...-ver), and certify it
• Define the required i/o commands, package them in a book (...-io), define test input files for the commands, and run the encode command against the test input files and the decode command against the resulting encoded files

Requirements

1. predicate: (is-prefix ps xs) is non-nil if and only if ps (the "pattern") is a prefix of xs
   Note: A prefix is a list xs is a contiguous sublist that starts at the beginning: (if xs is (list 1 2 3), then nil, (list 1), (list 2), and (list 1 2 3) are all prefixes of xs)
2. predicate: (pattern-in ps xs) is non-nil if and only if ps occurs as a contiguous sublist of xs
3. function: (match-prefix ps xs) is (list psbf  psaf  xsaf)
     where
     a.  psbf is the longest list prefixing both ps and xs
     b. (append  psbf  psaf) equals ps
     c. (car psaf ) does not equal (nth (len psbf) xs) when psaf  is non-empty
         (that is, the first element in xs that fails to match the pattern differs from the first element in psaf)
4. function: (break-at-pattern ps xs) is (list bf af)
     where
     a. (append bf ps af) equals xs if ps occurs as a contiguous sublist of xs
     b. bf is the shortest list for which property "a" holds
     c. (list bf af) equals (list xs nil) if ps doesn't occur as a contiguous subsequence of xs
   Note: The function break-at in list-utilities is simpler than break-at-pattern. The break-at function splits a list at an element with a specified value, but break-at-pattern splits a list at a specified sequence of values.

Required properties

1. If xss is a true-list of true-lists and (length xss) is 3, then the cdr and cddr of xss are non-nil, the cdddr is nil, and the car, cadr, and caddr are true-lists.
2. match-prefix delivers a true-list of three true-lists
3. If the second element of (match-prefix ps xs) is nil, then ps is a prefix of xs
4. If the second and third elements of the value match-prefix delivers are both non-empty, then their first elements are different
5. Appending the first and second elements of (match-prefix ps xs) reproduces ps
6. Appending the first and last elements of (match-prefix ps xs) reproduces xs
7. break-at-pattern delivers a true-list of two true-lists
8. When the pattern ps does not occur in the list xs, the first element of (break-at-pattern ps xs) is equal to xs and the second element is nil
9. When the pattern ps occurs in the list xs, appending the first element of (break-at-pattern ps xs),  ps, and the second element of (break-at-pattern ps xs) reproduces xs
   Note: This involves appending three lists in the specified order

File I/O

• Define an i/o command, htm-file->ltx-file, that  reads file with HTML markup and writes file with equivalent LaTeX markup. The HTML markup is limited to the tags in the table below

HTML Markup Tags and the Equivalent LaTeX