کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
421523 684871 2015 15 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
A Certifying Square Root and Division Elimination
ترجمه فارسی عنوان
ریشه مربع تضمین کننده و حذف بخش
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
چکیده انگلیسی

This paper presents the implementation of a program transformation that removes square roots and divisions from functional programs without recursion, producing code that can be exactly computed. This transformation accepts different subsets of languages as input and it provides a certifying mechanism when the targeted language is Pvs. In this case, we provide a relation between every function definition in the output code and its corresponding one in the input code, that specifies the behavior of the produced function with respect to the input one. This transformation has been implemented in OCaml and has been tested on different algorithms from the NASA ACCoRD project.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 317, 18 November 2015, Pages 117-131