Using Computer Algebra techniques for the specification, verification and synthesis of recursive programs

Nikolaj Popov and Tudor Jebelean

Mathematics and Computers in Simulation (MATCOM), 2009, vol. 79, issue 8, 2302-2309

Abstract: 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. The process is carried out by means of CA (Computer Algebra) and AC (Algorithmic Combinatorics) and is implemented in the Theorema system (using Mathematica). 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. 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 presented in the first part of this paper.

Keywords: Specification and verification; Program synthesis; Computer Algebra (search for similar items in EconPapers)
Date: 2009
References: View references in EconPapers View complete reference list from CitEc
Citations:

Downloads: (external link)
http://www.sciencedirect.com/science/article/pii/S037847540800373X
Full text for ScienceDirect subscribers only

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:eee:matcom:v:79:y:2009:i:8:p:2302-2309

DOI: 10.1016/j.matcom.2008.11.017

Access Statistics for this article

Mathematics and Computers in Simulation (MATCOM) is currently edited by Robert Beauwens

More articles in Mathematics and Computers in Simulation (MATCOM) from Elsevier
Bibliographic data for series maintained by Catherine Liu ().