کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
9656884 | 686148 | 2005 | 28 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Proving pointer programs in higher-order logic
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: Proving pointer programs in higher-order logic Proving pointer programs in higher-order logic](/preview/png/9656884.png)
چکیده انگلیسی
Building on the work of Burstall, this paper develops sound modelling and reasoning methods for imperative programs with pointers: heaps are modelled as mappings from addresses to values, and pointer structures are mapped to higher-level data types for verification. The programming language is embedded in higher-order logic. Its Hoare logic is derived. The whole development is purely definitional and thus sound. Apart from some smaller examples, the viability of this approach is demonstrated with a non-trivial case study. We show the correctness of the Schorr-Waite graph marking algorithm and present part of its readable proof in Isabelle/HOL.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 199, Issues 1â2, 25 Mayâ15 June 2005, Pages 200-227
Journal: Information and Computation - Volume 199, Issues 1â2, 25 Mayâ15 June 2005, Pages 200-227
نویسندگان
Farhad Mehta, Tobias Nipkow,