کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4951848 1441610 2017 61 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Verifying relational properties of functional programs by first-order refinement
ترجمه فارسی عنوان
بررسی ویژگی های ارتباطی برنامه های کاربردی با پالایش مرتبه اول
کلمات کلیدی
تأیید خودکار، زبان عملکردی بالاتر، انواع پاکسازی
ترجمه چکیده
اخیرا پیشرفت های زیادی در مورد تایید کامل برنامه های عملکردی مرتب شده بر اساس نوع پالایش و چک کردن مدل مرتبه بالاتر انجام شده است. با این حال، بسیاری از این تکنیک های تأیید بر اساس نوع پالایش اولیه مرتبه اول هستند و از این رو قادر به بررسی برخی خصوصیات توابع (مانند برابری دو توابع بازگشتی و یکنواختی یک تابع هستند که ما به آن خواص نسبی اشاره می کنیم). برای استحکام این محدودیت، یک فرم محدود از انواع پالایش مرتبه بالا را معرفی می کنیم که در آن اصطلاحات پیکربندی میتوانند به توابع اشاره کنند و فرمول یک تحول برنامه سیستماتیک را برای کاهش نوع چک کردن / استنتاج برای نوع پیکربندی مرتبه بالاتر به آن برای انواع پالایش مرتبه اول ، به طوری که می توان آن را به صورت خودکار با استفاده از یک چک کننده مدل نرم افزار موجود حل کرد. ما همچنین ثبات تحول را ثابت می کنیم، و در مورد پیاده سازی و آزمایش ها گزارش می کنیم.
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش مقاله
بررسی ویژگی های ارتباطی برنامه های کاربردی با پالایش مرتبه اول
چکیده انگلیسی
Much progress has been made recently on fully automated verification of higher-order functional programs, based on refinement types and higher-order model checking. Most of those verification techniques are, however, based on first-order refinement types, hence unable to verify certain properties of functions (such as the equality of two recursive functions and the monotonicity of a function, which we call relational properties). To relax this limitation, we introduce a restricted form of higher-order refinement types where refinement predicates can refer to functions, and formalize a systematic program transformation to reduce type checking/inference for higher-order refinement types to that for first-order refinement types, so that the latter can be automatically solved by using an existing software model checker. We also prove the soundness of the transformation, and report on implementation and experiments.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 137, 1 April 2017, Pages 2-62
نویسندگان
, , ,