دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش: 2
نویسندگان: Jacques Loeckx. Kurt Sieber (auth.)
سری: Series in Computer Science
ISBN (شابک) : 9783322967541, 9783322967534
ناشر: Vieweg+Teubner Verlag
سال نشر: 1987
تعداد صفحات: 236
زبان: German
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود)
حجم فایل: 5 مگابایت
کلمات کلیدی مربوط به کتاب مبانی تأیید برنامه: مهندسی، عمومی
در صورت تبدیل فایل کتاب The Foundations of Program Verification به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب مبانی تأیید برنامه نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
این یک کتاب درسی در مورد تأیید برنامه است. این روش بر روی آن دسته از روشهای راستیآزمایی متمرکز است که اکنون کلاسیک شدهاند، مانند روش ادعاهای استقرایی فلوید، روش بدیهی Hoare و القاء نقطه ثابت اسکات. هدف کتاب ارائه این روش های مختلف تأیید و توضیح پیشینه ریاضی آنها است. موضوع با دقت ریاضی بررسی می شود و مثال های زیادی در آن گنجانده شده است. در سرتاسر کتاب، همین مثالها دوباره ظاهر میشوند تا چگونگی ارتباط روشهای مختلف را نشان دهند. مطالب مستقل و بدون دانش قبلی از منطق یا معناشناسی قابل دسترسی است، اما دانش ابتدایی زبان های برنامه نویسی، زبان های رسمی و تئوری محاسبات مفید است. دغدغه اصلی ارائه موضوع در محیطی ساده تا حد امکان بوده است. به همین دلیل سه زبان برنامه نویسی ابتدایی و معرف معرفی شده اند: زبان برنامه نویسی فلوچارت، زبان برنامه های while و زبان برنامه های بازگشتی. برای این زبان های برنامه نویسی معنای عملیاتی و معنایی معرفی شده است. سپس هر روش راستیآزمایی در مناسبترین این زبانها نشان داده میشود و با کمک مناسبترین معناشناسی، درستی آن ثابت میشود.
This is a textbook on program verification. It concentrates on those verification methods that have now become classic such as the inductive assertions method of Floyd, the axiomatic method of Hoare and Scott's fixpoint induction. The aim of the book is to present these different verification methods and to explain their mathemati cal background. The subject is treated with mathematical precision, and many examples are included. Throughout the book the same examples will reappear to illustrate how the different methods are related. The material is self-contained and accessible without prior knowledge of logic or semantics, but elementary knowledge of programming languages, formal languages and the theory of computation is helpful. A main concern has been to present the subject in as simple a setting as possible. For this reason three elementary, representative programming languages are in troduced: a flowchart programming language, a language of while-programs and a language of recursive programs. For these programming languages the operational and denotational semantics are introduced. Each verification method is then illustrated in the most appropriate of these languages and proved correct with the help of the most appropriate of the semantics.
Front Matter....Pages i-ix
Front Matter....Pages 1-1
Mathematical Preliminaries....Pages 3-17
Predicate Logic....Pages 18-37
Front Matter....Pages 39-39
Three Simple Programming Languages....Pages 41-70
Fixpoints in Complete Partial Orders....Pages 71-91
Denotational Semantics....Pages 92-110
Front Matter....Pages 111-111
Correctness of Programs....Pages 113-131
The Classical Methods of Floyd....Pages 132-148
The Axiomatic Method of Hoare....Pages 149-173
Verification Methods Based on Denotational Semantics....Pages 174-198
LCF, A Logic for Computable Functions....Pages 199-214
Front Matter....Pages 215-215
An Overview of Further Developments....Pages 217-221
Back Matter....Pages 222-230