دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
دسته بندی: جبر ویرایش: 1 نویسندگان: Markus Müller-Olm (auth.) سری: Lecture Notes in Computer Science 1283 ISBN (شابک) : 3540634061, 9783540634065 ناشر: Springer-Verlag Berlin Heidelberg سال نشر: 1997 تعداد صفحات: 256 زبان: English فرمت فایل : DJVU (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) حجم فایل: 2 مگابایت
کلمات کلیدی مربوط به کتاب تأیید کامپایلر مدولار: یک رویکرد جبری اصلاحی که از انتزاع گام به گام حمایت می کند: زبانهای برنامهنویسی، کامپایلرها، مترجمان، مهندسی نرمافزار، منطق و معانی برنامهها، سیستمهای مبتنی بر هدف خاص و برنامهها
در صورت تبدیل فایل کتاب Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب تأیید کامپایلر مدولار: یک رویکرد جبری اصلاحی که از انتزاع گام به گام حمایت می کند نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
این کتاب طراحی تایید شده یک مولد کد را ارائه میکند که یک زبان برنامهنویسی بیدرنگ را به یک ریزپردازنده واقعی، Inmos Transputer ترجمه میکند. بر خلاف بسیاری از کارهای دیگر در مورد تأیید کامپایلر، و با تأکید خاص بر ماژولار بودن، به طور سیستماتیک صحت ترجمه را تا کد واقعی ماشین پوشش می دهد، که یک ضرورت در حوزه سیستم های حیاتی ایمنی است. چارچوب رسمی ارائه شده و همچنین ایدههای جدید مهندسی اثبات شده که در تولیدکننده کد تأیید شده گنجانده شدهاند، به طور کلی برای طراحی نرمافزار مرتبط هستند.
This book presents the verified design of a code generator translating a prototypic real-time programming language to an actual microprocessor, the Inmos Transputer. Unlike most other work on compiler verification, and with particular emphasis on modularity, it systematically covers correctness of translation down to actual machine code, a necessity in the area of safety-critical systems. The formal framework provided as well as the novel proof-engineering ideas incorporated in the verified code generator are also of relevance for software design in general.
Introduction....Pages 1-7
Complete Boolean lattices....Pages 9-14
Galois connections....Pages 15-22
States, valuation functions and predicates....Pages 23-38
The algebra of commands....Pages 39-83
Communication and time....Pages 85-104
Data refinement....Pages 105-111
Transputer base model....Pages 113-125
A small hard real-time programming language....Pages 127-134
A hierarchy of views....Pages 135-178
Compiling-correctness relations....Pages 179-187
Translation theorems....Pages 189-214
A functional implementation....Pages 215-231
Conclusion....Pages 233-237