The test vector file contains the data that will be used to test the axia described in the axiom file. Test vectors must be supplied for all free variable types in the axiom file, and in essence, provide values to the variable types during testing.
The test vectors are described by a vector name and an expression, which determines the type. The expression may include any known function (from the signature file), constant (including alii), or other test vector name, but may not be defined recursively. The type may also be explicitly assigned by prefixing the value with the type name and enclosing the value in parentheses.
The user can also ensure that a vector is evaluated only once per side of axiom evaluation, so different free variables referring to the same test vector will result in only one instance of the test vector, by enclosing the name of a test vector in curly braces. The test vector will still be evaluated on both sides of the same axiom, so the two sides will be guaranteed of starting with the same value for the vector. Care must be taken to ensure that code that may change the value of the "once" test vectors as a side effect will not create an error.
Because each axiom is tested for all possible values of the test vectors, it may be useful or necessary to separate vectors of the same type but used differently into pseudo-types corresponding to their respective roles. This is done by using alii. The user creates a different pseudo-type for each role the data type plays, and uses that pseudo-type throughout the axiom, signature, and vector files. Then, in the alias file, the pseudo-types are mapped back to their original type By doing so, the user ensures that the number of test cases is kept to a minimum, and that the vectors are used correctly.
Previous Topic
Next Topic