کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4951375 | 1441446 | 2017 | 24 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Executing and verifying higher-order functional-imperative programs in Maude
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
We incorporate higher-order functions and state monads in Maude, thereby embedding a higher-order functional language with imperative features in the Maude framework. We illustrate, via simple programs in the resulting language: the concrete and symbolic execution of programs; their verification with respect to properties expressed in Reachability Logic, a language-parametric generalisation of Hoare Logic; and the verification of program-equivalence properties. Our approach is proved sound and is implemented in Full Maude by taking advantage of its reflective features and module system.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 93, December 2017, Pages 68-91
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 93, December 2017, Pages 68-91
نویسندگان
Vlad Rusu, Andrei Arusoaie,