کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
401667 | 675418 | 2010 | 30 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Reflexive transitive invariant relations: A basis for computing loop functions
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
هوش مصنوعی
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
Invariant assertions play an important role in the analysis and verification of iterative programs. In this paper, we introduce a related but distinct concept, namely that of invariant relation. While invariant assertions are useful to prove the correctness of a loop with respect to a specification (represented by a precondition/ postcondition pair) in Hoare’s logic, invariant relations are useful to derive the function of the loop in Mills’ logic.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Symbolic Computation - Volume 45, Issue 11, November 2010, Pages 1114-1143
Journal: Journal of Symbolic Computation - Volume 45, Issue 11, November 2010, Pages 1114-1143