Title :
Proving Partial Correctness and Termination of Mutually Recursive Programs
Author :
Popov, Nikolaj ; Jebelean, Tudor
Author_Institution :
Res. Inst. for Symbolic Comput., Johannes Kepler Univ. of Linz, Linz, Austria
Abstract :
We present an environment for proving correctness of mutually recursive functional programs. As usual, correctness is transformed into a set of first-order predicate logic formulae - verification conditions. As a distinctive feature of our method, these formulae are not only sufficient, but also necessary for the correctness.
Keywords :
functional programming; recursive functions; logic formulae verification; mutually recursive program; recursive functional program; Computers; Concrete; Contracts; Open systems; Programming; Silicon;
Conference_Titel :
Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2010 12th International Symposium on
Conference_Location :
Timisoara
Print_ISBN :
978-1-4244-9816-1
DOI :
10.1109/SYNASC.2010.65
