Verification of Algorithms

Two important questions:

1. Whether the chosen approach will actually lead to the required solution?
2. Whether the already developed components are correct, i.e., whether they fulfill the specifications?

• Ideally we would like to be able to prove at any time that for every imaginable input the algorithms included in the design and their interplay will deliver the expected results according to the specification.
• Since today’s large software systems permit the complete description of neither the input set nor the anticipated result set (due to combinatorial explosion), such systems can no longer be completely tested. Thus efforts must be made to achieve as much clarity as possible already in the design phase about the correctness of the solution.
• Proof of correctness cannot be handled without formal and mathematical tools ([McCarthy 1962], [Naur 1966], [Hoare 1969], [Manna 1969], [Knuth 1973], [Dijkstra 1976], see overview in [Elspas 1972].)
• The use of a verification procedure forces the software engineer to reproduce all design decisions and thus also helps in finding logical errors. Verification is an extremely useful technique for early detection of design errors and also complements the design documentation. Verification itself can be fallible, however, it cannot replace testing of a software product.
• Verification can be used successfully to prove the correctness of short and simple algorithms. For the production of larger software systems, the difficulties rise so sharply that it should be clear that verification fails as a practical test aid.