Verification of sequential and concurrent programs

برنامه‌های رایانه‌ای بخشی ضروری از بسیاری از سیستم‌هایی هستند که ما در زندگی روزمره خود به آن‌ها تکیه می‌کنیم، و عملکرد صحیح و ایمنی این سیستم‌ها از اهمیت بالایی برخوردار است. بنابراین، توسعه روش‌هایی که صحت برنامه را تضمین می‌کنند، یک چالش کلیدی برای دانشمندان رایانه است.

این نسخه سوم مورد انتظار تأیید برنامه‌های متوالی و همزمان< /EM> یک کاوش سیستماتیک از یکی از رایج ترین رویکردهای تأیید برنامه، که به عنوان رویکرد \"اثباتی\" شناخته می شود، ارائه می دهد. با پیروی از فرمول موفق نسخه های قبلی، این رویکرد برای برنامه های متوالی قطعی و غیر قطعی با پیچیدگی های متفاوت، همراه با برنامه های همزمان موازی و توزیع شده اعمال می شود. محتوای گسترده این نسخه کامل جدید همچنین شامل پوشش تأیید برنامه های شی گرا است. برای هر دسته از برنامه ها، نویسندگان یک سیستم معنایی عملیاتی و اثباتی را برای تأیید صحت جزئی و کلی معرفی می کنند که به طور رسمی در قضایای صحت متناظر توجیه شده است. مطالعات موردی ارائه شده در سراسر کتاب، استفاده از سیستم‌های اثبات را برای تأیید رسمی راه‌حل‌های مشکلات کلاسیک، مانند مرتب‌سازی، دستکاری فهرست‌ها، تولیدکننده/مصرف‌کننده و طرد متقابل نشان می‌دهد.

موضوعات و ویژگی‌ها:

• شامل یک بخش مقدماتی کامل است که خواننده را با مفاهیم اولیه و نشانه‌های استفاده شده در کتاب آشنا می‌کند. و همچنین ساختار کتاب
  
• رویکرد Hoare را برای تأیید برنامه برای برنامه‌های while توضیح می‌دهد، و اثبات درستی برنامه‌ای برای پارتیشن بندی آرایه را ارائه می‌دهد (جدید )
  
• هر فصل را با تمرین‌ها و نکات کتابشناختی برای مطالعه بیشتر به پایان می‌رساند
  
• درباره برنامه‌های بازگشتی که برنامه‌های قطعی را با رویه‌ها و رویه‌های بدون پارامتر گسترش می‌دهند بحث می‌کند. مکانیسم پارامتر فراخوانی به ارزش، و اثبات درستی برنامه مرتب‌سازی سریع را ارائه می‌دهد (NEW)
  
• برنامه‌های غیر قطعی و توزیع‌شده را کاوش می‌کند و روش تأیید برنامه‌های توزیع‌شده را ارائه می‌کند. بر اساس تبدیل به برنامه های غیر قطعی
  
• برنامه های شی گرا را با تمرکز بر ویژگی های اصلی اشیاء ارائه می کند (NEW)
  
< LI>برنامه های موازی را با متغیرهای مشترک و با همگام سازی بررسی می کند

• مساله انصاف را در چارچوب برنامه های غیر قطعی با رویکردی مبتنی بر روش زمان بندی صریح مطالعه می کند
  
• شامل پیشگفتاری از پروفسور امیر پنولی است

این به روز رسانی مدرن از یک کتاب درسی کلاسیک و خواننده پسند برای دوره مقدماتی تأیید برنامه برای دانشجویان پیشرفته در مقطع کارشناسی یا کارشناسی ارشد، و همچنین ممکن است به عنوان مقدمه ای برای معناشناسی عملیاتی استفاده شود. رئوس مطالب دوره های ممکن در پیشگفتار کتاب پیشنهاد شده است. این کتاب در پرداختن به راستی‌آزمایی ادعایی تمام کلاس‌های ضروری برنامه‌های ضروری منحصربه‌فرد است: برنامه‌های در حالی که، برنامه‌های بازگشتی، برنامه‌های شی‌گرا، برنامه‌های غیر قطعی، برنامه‌های موازی، و برنامه‌های توزیع‌شده.

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.