s a different subpath. Eventually the The acceptance test is the customer's check that the system meets outputs from the symbolic execution are compared with the its requirements. The tests will probably cover the same ground as corresponding part of the specification. Symbolic execution is the system test, though usually not so comprehensively. not widely used in practice, though there are some tools to support symbolic execution in languages such as Fortran and Lisp. 25.7.3.4 Regression testing 4. Proof. It is slowly becoming possible to specify software math- Regression testing applies to an enhanced system or component, ematically, and one of the anticipated benefits of this is that it and is a check to see that modifications have not caused unintended then becomes possible to use mathematical proof methods to effects and that the system or component still meets its require- obtain confidence in the program. Proof tools now exist and it ments. The regression test usually consist of a battery of tests is practical, though still difficult, to produce proofs of small constructed during earlier development and enhancement of the systems. The application of this technique is today in the system, often extracted from a test library and run automatically. verification of key components of a system, where the need for correctness is high enough to warrant the investment in the 25.7.4 Debugging proof. Standards emerging for safety critical software are al- ready beginning to demand the use of formal verification and Tests may discover faults in a system; debugging is the activity of proof (Ould, 1991). The ability to prove correctness does not isolating and correcting them. take away the need for testing. The proof usually must assume some form of correctness of the environment in which the unit 25.7.4.1 Dumps and traces being proved is to exist, and some of the non functional at- tributes, such as usability, of the unit may not be susceptible to The basic approaches to debugging involve the collection and proof (Lind