Maximums and Minimums

Purpose of exercise

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

Activities

• Define the functions required below (here are some predefined functions that you might find helpful)
• Package the functions in a book and certify it
• Define the predicates required below and package them in another book (the "test book")
• Package DoubleCheck tests for the properties stated below in the test book, and run some tests
• Convert the DoubleCheck predicates to ACL2 theorems, package them in another book (the "verification book"), and certify it

Terminology

• measure pair: a two-element list whose first element, a rational number, is the measure of its other element
• true-list: nil or (cons x xs), where xs is a true-list

Requirements

1. Define a function, maximum, that delivers the largest value in a non-empty list of rational numbers.
2. Define a function, min-pair, that delivers the smaller of two measure-pairs.
3. Define a function, minimium-pair, that delivers the smallest measure-pair from a non-empty list of measure-pairs.
4. Define a predicate, measure-pairp, that is true if and only if its argument is a measure-pair.
5. Define a predicate, measure-pair-listp, that is true if and only if its argument is a true-list of measure-pairs.

Properties

1. If xs is a non-empty true-list of rational numbers, then (maximum xs) is a rational number
2. The value (maximum xs) occurs in the list xs
3. The value (maximum xs) is at least as large as any element in xs
4. If xs is a non-empty true-list of measure pairs, then (minimum-pair xs) is a measure-pair
5. If xs is a non-empty true-list of measure-pairs, then (minimum-pair xs) is an element of xs
6. If xs is a true-list of measure-pairs, then no element of xs has a smaller measure than (minimum-pair xs)

ACL2 functions useful in this exercise

• max
• true-listp
• rationalp
• rational-listp
• member-equal

Note

• The ACL2 intrinsic member is more efficient member-equal, but member-equal can check for the occurrence of any kind of value in a list, while member is reliable only for numbers, characters, and symbols.