Stats

Write a program that computes and displays the average of a sequence of numbers, their standard deviation, and the relative frequency of each number in the sequence.

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
• Practice with ACL2 file i/o

Activities

• Define the functions required below (here are some predefined functions that you might find helpful)
• Package the functions in a book (the "service book"), and certify it
• DoubleCheck the properties stated below
• Package DoubleCheck tests for the properties stated below in another book (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

• true-list: nil or (cons x xs), where xs is a true-list (the predicate true-listp tests for true-lists, and the predicate rational-listp tests for true-lists of rational numbers)

Requirements

1. Define a function avg  that computes the average of a list of rational numbers
2. Define a function var that computes the variance of a list of rational numbers
3. Define a function reps that computes the number of times a value occurs in a list
   Example: (reps 2 (list 1 2 3 2 1 2 3 4 5 4 3 2 1)) is 4
4. Define a function sigDgts that, given a string that is the standard-format decimal numeral of a rational number, delivers the number of significant digits in the numeral
5. Define a function that reads the required input file and produces the required output file

Properties

1. (avg xs) is a rational number if xs is a true-list of rational numbers
2. (var xs) is a non-negative, rational number if xs is a true-list of rational numbers
3. (reps x xs) is a non-negative integer
4. (reps x xs) does not exceed the number of elements in xs
5. (reps x (remove1-equal x xs) xs) is one less than (reps x xs) under certain conditions

I/O

The input file will contain a sequence of numbers, in standard formats, separated by whitespace. A whitespace character, for purposes of this project, is a blank, newline, carriage return, or line feed character.

The output file will contain approximations of the average and variance of the numbers in the input file. The approximations will be accurate to the maximum number of decimal places specified in the number from the input file with the greatest number of digits. The output file will also contain a table of frequencies. That is, it will include a sequence of pairs in which the first component of a pair is a number, x, from the input file, and the second component is the number of times x occurs in the input file. Each number that occurs in the input file will appear exactly once as the first-component of some pair that occurs in the output table.

ACL2 intrinsics and other functions and commands useful in this exercise

• true-listp
• rational-listp
• len
• member-equal
• remove1-equal
• str->rat -- defined in io-utilities teachpack
• rat->str -- defined in io-utilities teachpack
• file->string -- defined in io-utilities teachpack
• string-list->file -- defined in io-utilities teachpack
• packets -- defined in list-utilities teachpack