کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
1140109 956713 2009 8 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Using Computer Algebra techniques for the specification, verification and synthesis of recursive programs
موضوعات مرتبط
مهندسی و علوم پایه سایر رشته های مهندسی کنترل و سیستم های مهندسی
پیش نمایش صفحه اول مقاله
Using Computer Algebra techniques for the specification, verification and synthesis of recursive programs
چکیده انگلیسی
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.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Mathematics and Computers in Simulation - Volume 79, Issue 8, April 2009, Pages 2302-2309
نویسندگان
, ,