کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
9657440 | 1441794 | 2005 | 39 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Rewriting of imperative programs into logical equations
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
This paper describes SOSSubC: a system for automatically translating programs written in SubC, a simple imperative language, into a set of first-order equations. This set of equations represents a SubC program and has a precise mathematical meaning; moreover, the standard techniques for mechanizing equational reasoning can be used for verifying properties of programs. Part of the system itself is formulated abstractly as a set of first-order rewrite rules. Then, the rewrite rules are proven to be terminating and confluent. This means that our system produces, for a given SubC program, a unique set of equations. In our work, simple imperative programs are equational theories of a logical system within which proofs can be derived.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 56, Issue 3, MayâJune 2005, Pages 363-401
Journal: Science of Computer Programming - Volume 56, Issue 3, MayâJune 2005, Pages 363-401
نویسندگان
Olivier Ponsini, Carine Fédèle, Emmanuel Kounalis,