کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
421523 | 684871 | 2015 | 15 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
A Certifying Square Root and Division Elimination
ترجمه فارسی عنوان
ریشه مربع تضمین کننده و حذف بخش
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
چکیده انگلیسی
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
Journal: Electronic Notes in Theoretical Computer Science - Volume 317, 18 November 2015, Pages 117-131