کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
436771 | 690035 | 2006 | 19 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Algebras of modal operators and partial correctness
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
Modal Kleene algebras are Kleene algebras enriched by forward and backward box and diamond operators. We formalise the symmetries of these operators as Galois connections, complementarities and dualities. We study their properties in the associated operator algebras and show that the axioms of relation algebra are theorems at the operator level. Modal Kleene algebras provide a unifying semantics for various program calculi and enhance efficient cross-theory reasoning in this class, often in a very concise pointfree style. This claim is supported by novel algebraic soundness and completeness proofs for Hoare logic and by connecting this formalism with an algebraic decision procedure.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 351, Issue 2, 21 February 2006, Pages 221-239
Journal: Theoretical Computer Science - Volume 351, Issue 2, 21 February 2006, Pages 221-239