DocumentCode
2536711
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
fYear
2010
fDate
23-26 Sept. 2010
Firstpage
153
Lastpage
156
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/SYNASC.2010.65
Filename
5715281
Link To Document