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
- 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
- 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
- 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
- Define a function, maximum, that delivers the largest value
in a non-empty list of rational numbers.
- Define a function, min-pair, that delivers the smaller of two
- Define a function, minimium-pair, that delivers the smallest
measure-pair from a non-empty list of measure-pairs.
- Define a predicate, measure-pairp, that is true if and only
if its argument is a measure-pair.
- Define a predicate, measure-pair-listp, that is true if and
only if its argument is a true-list of measure-pairs.
- If xs is a non-empty true-list of rational numbers, then (maximum xs) is a
- The value (maximum xs) occurs in the list xs
- The value (maximum xs) is at least as
large as any element in xs
- If xs is a non-empty true-list of measure pairs, then (minimum-pair xs) is
- If xs is a non-empty true-list of measure-pairs, then (minimum-pair xs) is an
element of xs
- 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
- 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.