کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
438806 | 690331 | 2006 | 26 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Towards imperative modules: Reasoning about invariants and sharing of mutable state
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
Imperative and object-oriented programs make ubiquitous use of shared mutable objects. Updating a shared object can and often does transgress a boundary that was supposed to be established using static constructs such as a class with private fields. This paper shows how auxiliary fields can be used to express two state-dependent encapsulation disciplines: ownership, a kind of separation, and friendship, a kind of sharing. A methodology is given for specification and modular verification of encapsulated object invariants and shown sound for a class-based language. As an example the methodology is used to specify iterators, which are problematic for previous ownership systems.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 365, Issues 1–2, 10 November 2006, Pages 143-168
Journal: Theoretical Computer Science - Volume 365, Issues 1–2, 10 November 2006, Pages 143-168