We describe an innovative method for proving total correctness of tail
recursive programs having a specific structure, namely programs in
which an auxiliary tail recursive function is driven by a main
nonrecursive function, and only the specification of the main function
is provided.
The specification of the auxiliary function is obtained almost fully
automatically by solving coupled linear recursive sequences with
constant coefficients [3].
The process is carried out by means of CA (Computer Algebra) and AC
(Algorithmic Combinatorics). We demonstrate this method on an example
involving polynomial expressions.
Furthermore, we develop a method for synthesis of recursive programs
for computing polynomial expressions of a fixed degree by means of
``cheap'' operations e.g., additions, subtractions and
multiplications. For a given polynomial expression, we define its
recursive program in a schemewise manner [5].
The correctness of the synthesized programs follows from the general
correctness of the synthesis method, which is proven once for all,
using the verification method developed in [4].
[1] | B. Buchberger, A. Craciun, T. Jebelean, L. Kovacs, T. Kutsia, K. Nakagawa, F. Piroi, N. Popov, J. Robu, M. Rosenkranz, and W. Windsteiger. Theorema: Towards Computer-Aided Mathematical Theory Exploration. Journal of Applied Logic, 2005. | |
[2] | N. Popov and T. Jebelean. Proving Termination of Recursive Programs by Matching Against Simplified Program Versions and Construction of Specialized Libraries in Theorema. In D. Hofbauer and A. Serebrenik, editors, Proceedings of 9th International Workshop on Termination (WST'07), pages 48-52, Paris, France, June 2007. | |
[3] | L. Kovacs, N. Popov, and T. Jebelean. Verification Environment in Theorema. Annals of Mathematics, Computing and Teleinformatics (AMCT), 1(2):27--34, 2005. | |
[4] | N. Popov. Functional Program Verification in Theorema. PhD thesis, RISC, Johannes Kepler University Linz, Austria, July 2008. | |
[5] | N. Popov and T. Jebelean. Using Computer Algebra Techniques for the Specification, Verification and Synthesis of Recursive Programs. Mathematics and Computers in Simulation, 2008. To appear. |
Tudor Jebelean is an Associate Professor in the Theorema group (leader: Bruno Buchberger and Tudor Jebelean) at the Research Institute for Symbolic Computation (RISC), Johannes Kepler University of Linz, Austria. His main research interests are automated reasoning and program verification using logic and algebraic methods. He holds a PhD in Computer Science and Habilitation title from Johannes Kepler University of Linz.
Contact Nikolaj and Tudor at:
Dr. Nikolaj Popov
Research Institute for Symbolic Computation (RISC)
Johannes Kepler University of Linz
A-4040 Linz, Austria
popov at risc.uni-linz.ac.at
http://www.risc.uni-linz.ac.at/home/npopov/
Prof. Dr. Tudor Jebelean
Research Institute for Symbolic Computation (RISC)
Johannes Kepler University of Linz
A-4040 Linz, Austria
Tudor.Jebelean at risc.uni-linz.ac.at
http://www.risc.uni-linz.ac.at/home/tjebelea/