کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
434504 | 689745 | 2014 | 27 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
An observationally complete program logic for imperative higher-order functions
ترجمه فارسی عنوان
یک منطق برنامه مشاهدهی کامل برای توابع اجباری مرتبه بالاتر
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
تکمیل فرمول های خاص، منطق برنامه، تابع مرتبه بالاتر، برنامه نویسی حقیقی هم ارزیابی مشاهده
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
چکیده انگلیسی
We establish a strong completeness property called observational completeness of the program logic for imperative, higher-order functions introduced in [1]. Observational completeness states that valid assertions characterise program behaviour up to observational congruence, giving a precise correspondence between operational and axiomatic semantics. The proof layout for the observational completeness which uses a restricted syntactic structure called finite canonical forms originally introduced in game-based semantics, and characteristic formulae originally introduced in the process calculi, is generally applicable for a precise axiomatic characterisation of more complex program behaviour, such as aliasing and local state.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 517, 16 January 2014, Pages 75–101
Journal: Theoretical Computer Science - Volume 517, 16 January 2014, Pages 75–101
نویسندگان
Kohei Honda, Nobuko Yoshida, Martin Berger,