In order to test Lisex we intend to use functional testing based on formal specifications [HP95].

Lisex 0.0 has not been tested as extensively as it should have due to lack of resources and to the fact that the development team expects to be able to automate a significant part of this essential activity. So far, a total of 365 model-level test cases have been (manually) generated and only 10% of them were executed without finding any errors. Besides, we have a preliminary version of an algorithm for extracting testing sets from specifications in Coq.

Functional testing based on formal specifications is a technique that uses a formal specification of the system requirements to generate the test cases that are, later, executed on the code. In addition, it allows the use of the formal model as an oracle to decide whether or not an error in the program was discovered using a test case.

In short, the technique consists of the following activities:

1. Syntactic analysis of the specification, with the aim of finding out all the functional alternatives it describes

   	This results in a collection of testing sets, each one representing a different functional alternative
   	In the analysis a testing strategy is applied (e.g., normal disjunctive form, specification mutation, domain propagation, etc.)

2. Another testing strategy is applied to the sets obtained in the first analysis, generating a new collection of sets (not less populated than the first one)
3. The process is repeated iteratively until the required quantity of testing sets is achieved
4. A representative item is chosen from each set of the last collection generated
5. The representatives are projected onto the implementation level
6. The test cases obtained this way are executed on the code
7. Output from every execution is captured
8. Each output is projected onto the model level
9. Every pair (test case, output) is applied to the specification in order to verify that the output is as expected (with base on the specification for that input)
10. If the specification shows that an output does not match the input, an error was found

The process continues by correcting the code and executing all the necessary cases again.

The Lisex team has documented every model-level test case in HTML and Postscript.