کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
432108 1441296 2006 34 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Kleene under a modal demonic star
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Kleene under a modal demonic star
چکیده انگلیسی

In relational semantics, the input-output semantics of a program is a relation on its set of states. We generalise this in considering elements of Kleene algebras as semantical values. In a nondeterministic context, the demonic semantics is calculated by considering the worst behaviour of the program. In this paper, we concentrate on while loops. Calculating the semantics of a loop is difficult, but showing the correctness of any candidate abstraction is much easier. For deterministic programs, Mills has described a checking method known as the while statement verification rule. A corresponding programming theorem for nondeterministic iterative constructs is proposed, proved and applied to an example. This theorem can be considered as a generalisation of the while statement verification rule to nondeterministic loops. The paper generalises earlier relation-algebraic work to the setting of modal Kleene algebra, an extension of Kozen’s Kleene algebra with tests that allows the internalisation of weakest liberal precondition and strongest liberal postcondition operators.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: The Journal of Logic and Algebraic Programming - Volume 66, Issue 2, February–March 2006, Pages 127-160