کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
6875936 689595 2016 24 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Completeness for recursive procedures in separation logic
ترجمه فارسی عنوان
تکمیل روش های بازگشتی در منطق جداسازی
کلمات کلیدی
ترجمه چکیده
این مقاله به تکمیل یک پسوند منطق هوآر و منطق جداسازی برای برنامه های اشاره گر با روش های متقابل بازگشتی ثابت می کند. این مقاله بیانگر بیان زبان حاکم است. این مقاله با معرفی دو قاعده استنتاج جدید، سیستم جدیدی را به وجود می آورد و یک محرک را حذف می کند که در منطق جداسازی و سایر قوانین استنتاج بیش از حد برای نشان دادن کامل بودن، غیر منطقی است. این عبارت جدیدی را معرفی می کند که برای توصیف اطلاعات کامل یک حالت مشخص در یک پیش شرط استفاده می شود. این کار همچنین از پیش شرط لازم و کافی برای برنامه ای برای اجرای اعدام بدون وقفه استفاده می کند، که ما را قادر می سازد تا از قوی ترین پست شرایط استفاده کنیم.
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش مقاله
تکمیل روش های بازگشتی در منطق جداسازی
چکیده انگلیسی
This paper proves the completeness of an extension of Hoare's logic and separation logic for pointer programs with mutual recursive procedures. This paper shows the expressiveness of the assertion language as well. This paper achieves a new system by introducing two new inference rules, and removes an axiom that is unsound in separation logic and other redundant inference rules for showing completeness. It introduces a novel expression that is used to describe complete information of a given state in a precondition. This work also uses the necessary and sufficient precondition of a program for the abort-free execution, which enables us to utilize strongest postconditions.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 631, 6 June 2016, Pages 73-96
نویسندگان
, ,