دانلود کتاب Verification of sequential and concurrent programs (به فارسی: تایید برنامه های متوالی و همزمان) نوشته شده توسط «Krzysztof R. Apt – Frank S. de Boer – Ernst-Rüdiger Olderog»
اطلاعات کتاب تایید برنامه های متوالی و همزمان
نوع: کتاب الکترونیکی
ناشر: Springer
نویسنده: Krzysztof R. Apt – Frank S. de Boer – Ernst-Rüdiger Olderog
زبان: english
فرمت کتاب: PDF (قابل تبدیل به سایر فرمت ها)
سال انتشار: 2009
تعداد صفحه: 524
حجم فایل: 2.10 مگابایت
کد کتاب: 1848827458 , 9781848827455
نوبت چاپ: 3rd
توضیحات کتاب تایید برنامه های متوالی و همزمان
برنامه‌های رایانه‌ای بخش ضروری بسیاری از سیستم‌هایی هستند که ما در زندگی روزمره به آن‌ها تکیه می‌کنیم، و عملکرد صحیح و ایمنی این سیستم‌ها از اهمیت بالایی برخوردار است. بنابراین، توسعه روش‌هایی که صحت برنامه را تضمین می‌کنند، یک چالش کلیدی برای دانشمندان رایانه است.
این نسخه سوم مورد انتظار تأیید برنامه‌های متوالی و همزمان، کاوش سیستماتیک یکی از برنامه‌ها را ارائه می‌کند. رایج ترین رویکردها برای تأیید برنامه، که به عنوان رویکرد “ادعای” شناخته می شود. با پیروی از فرمول موفقیت آمیز نسخه های قبلی، این رویکرد برای برنامه های متوالی قطعی و غیر قطعی با پیچیدگی های مختلف، همراه با برنامه های همزمان موازی و توزیع شده اعمال می شود. محتوای گسترده این نسخه کامل جدید همچنین شامل پوشش تأیید برنامه های شی گرا است. برای هر دسته از برنامه ها، نویسندگان یک سیستم معناشناسی عملیاتی و اثبات را برای تأیید صحت جزئی و کلی معرفی می کنند که به طور رسمی در قضایای صحت متناظر توجیه شده است. مطالعات موردی ارائه شده در سراسر کتاب، استفاده از سیستم‌های اثبات را برای تأیید رسمی راه‌حل‌های مشکلات کلاسیک، مانند مرتب‌سازی، دستکاری فهرست‌ها، تولیدکننده/مصرف‌کننده و طرد متقابل نشان می‌دهد.
موضوعات و ویژگی ها:
- شامل یک بخش مقدماتی کامل است که خواننده را با مفاهیم اولیه و نمادهای استفاده شده در کتاب آشنا می کند. به عنوان ساختار کتاب
- رویکرد Hoare را برای تأیید برنامه‌ها برای برنامه‌های while توضیح می‌دهد، و اثبات درستی یک برنامه برای پارتیشن‌بندی یک آرایه (جدید) را ارائه می‌دهد
- هر یک را نتیجه می‌گیرد. فصلی با تمرین‌ها و نکات کتاب‌شناختی برای مطالعه بیشتر
- برنامه‌های بازگشتی را مورد بحث قرار می‌دهد که برنامه‌های قطعی را با رویه‌ها و رویه‌های بدون پارامتر با مکانیزم پارامتر فراخوانی به ارزش گسترش می‌دهند، و اثبات درستی برنامه مرتب‌سازی سریع را ارائه می‌دهد. (جدید)
- برنامه‌های غیر قطعی و توزیع‌شده را کاوش می‌کند و یک تأییدیه برای من ارائه می‌کند روش برنامه های توزیع شده بر اساس تبدیل به برنامه های غیر قطعی
- برنامه های شی گرا را با تمرکز بر ویژگی های اصلی اشیا (NEW) ارائه می کند
- بررسی می کند برنامه های موازی با متغیرهای مشترک و با همگام سازی
- مساله انصاف را در چارچوب برنامه های غیر قطعی با رویکردی مبتنی بر روش زمان بندی صریح مطالعه می کند
- شامل پیشگفتاری از پروفسور امیر پنولی است
این به روز رسانی مدرن از یک کتاب درسی کلاسیک و خواننده پسند برای یک دوره مقدماتی عالی است تأیید برنامه برای دانشجویان پیشرفته کارشناسی یا کارشناسی ارشد، و همچنین ممکن است به عنوان مقدمه ای برای معناشناسی عملیاتی استفاده شود. رئوس مطالب دوره های ممکن در پیشگفتار کتاب پیشنهاد شده است. این کتاب در پرداختن به راستی‌آزمایی ادعایی تمام کلاس‌های ضروری برنامه‌های امری منحصربه‌فرد است: برنامه‌های ضمنی، برنامه‌های بازگشتی، برنامه‌های شی‌گرا، برنامه‌های غیر قطعی، برنامه‌های موازی، و برنامه‌های توزیع‌شده.
Computer programs are an indispensable part of many of the systems we rely upon in our daily lives, and the proper functioning and safety of these systems is of paramount importance. The development of methods that ensure program correctness is therefore a key challenge for computer scientists.
This widely anticipated third edition of Verification of Sequential and Concurrent Programs provides a systematic exploration of one of the most common approaches to program verification, known as the “assertional” approach. Following the successful formula of previous editions, this approach is applied to deterministic and nondeterministic sequential programs of varying complexity, together with both parallel and distributed concurrent programs. The expanded content of this thorough new edition also includes coverage of the verification of object-oriented programs. For each class of programs, the authors introduce an operational semantics and proof systems for the verification of partial and total correctness, justified formally in corresponding soundness theorems. Case studies supplied throughout the book demonstrate the use of the proof systems to formally verify solutions to classical problems, such as sorting, manipulation of lists, producer/consumer and mutual exclusion.
Topics and Features:
- Includes a thorough introductory section, familiarizing the reader with the basic concepts and notation used in the book, as well as the book’s structure
- Explains Hoare’s approach to program verification for while programs, providing a correctness proof of a program for partitioning an array (NEW)
- Concludes each chapter with exercises and bibliographic remarks for further reading
- Discusses recursive programs that extend deterministic programs by parameterless procedures and procedures with the call-by-value parameter mechanism, and provides a correctness proof of the quicksort program (NEW)
- Explores nondeterministic and distributed programs, presenting a verification method of distributed programs based on a transformation into nondeterministic ones
- Presents object-oriented programs, with a focus on the main characteristics of objects (NEW)
- Investigates parallel programs with shared variables and with synchronization
- Studies the issue of fairness in the framework of nondeterministic programs, using an approach based on the method of explicit schedulers
- Includes a Foreword by Professor Amir Pnueli
This modern update of a classic, reader-friendly textbook is perfect for an introductory course on program verification for advanced undergraduate or graduate students, and may also be used as an introduction to operational semantics. Outlines for possible courses are suggested in the Preface to the book. This book is unique in addressing assertional verification of all essential classes of imperative programs: while programs, recursive programs, object-oriented programs, nondeterministic programs, parallel programs, and distributed programs.
دانلود کتاب «تایید برنامه های متوالی و همزمان»
