| Konferenzartikel| [1] | Thilo Gaul, Wolfgang Goerigk, Wolf Zimmermann, Correct Programs without Proof? On Checker-Based Program Verification, Proceedings of the ATOOLS'98, May 1998.
|
ZusammenfassungCorrect Programs without Proof ? On Checker-Based Program Verification Introduction In many cases, the efort of proving the correctness of large program systems seems not to be justifyable. Since heuristics and programming tricks are used and necessary to successfully solve complex problems, mathematical inductive argumentation often fails, because the algorithms to be verifyed get too complex and tricky. We need more modular approaches to guarantee program correctness. Our paper proposes a checker-based approach to program veri,cation, which works, if partial correctness of the application succes. In many cases, it is much easier to check a given result to be a correct solution of a problem than to verify the generating algorithm. A classical example is the solution of systems of linear equations, where simple matrix-vector multiplication is sufficient to double check the calculated results. If we build checker routines into the program code, large program parts need not to be veri,ed at all. Thus, we propose a modular approach using a combination of checking and proving. We may concentrate on the full correctness of small program parts in order to guarantee the partial correctness of the entire program. Moreover, checker routines are transformational, and we can formulate them as correctness predicates in a sufficiently small functional language.
Autoren
| |
