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

 HTML markup LaTeX markup

blah blah blah ...

~blah blah blah ...~          Note: "~" means "newline character" blah blah blah ... \emph{blah blah blah ...}
• blah blah blah ...
• ...
\begin{itemize}\item{blah blah blah...}... \end{itemize}
1. blah blah blah ...
2. ...
\begin{enumerate}\item{blah blah blah...}... \end{enumerate}
r1c1...r1cn...
...... \begin{tabular}r1c1 & ... & r1cn \\ ... \end{tabular}