Program Proofs

درباره این کتاب

این کتاب درسی جامع و بسیار خواندنی، نحوه استدلال رسمی درباره برنامه‌های کامپیوتری را با استفاده از رویکردی افزایشی و زبان برنامه‌نویسی دافنی (Dafny) که برای تایید طراحی شده، آموزش می‌دهد. «اثبات‌های برنامه» به دانشجویان نشان می‌دهد که نوشتن مشخصات برای برنامه‌ها به چه معناست، برنامه‌ها چگونه باید آن مشخصات را برآورده کنند و چگونه می‌توان اثبات‌هایی نوشت که مشخصات را به برنامه‌ها متصل کند. کی. روستن ام. لینو با بیانی روشن و طنزآمیز، ابتدا مروری بر نظریه پایه پشت استدلال درباره برنامه‌ها ارائه می‌دهد. سپس به تدریج به مفاهیم و کاربردهای پیچیده می‌پردازد، تا جایی که دانشجویان با برنامه‌های واقعی شامل اشیاء، ساختارهای داده و بازگشت‌های غیربدیهی مواجه می‌شوند. برای تاکید بر ماهیت عملی اثبات‌های برنامه، تمام مطالب و مثال‌ها از زبان برنامه‌نویسی دافنی استفاده می‌کنند، اما هیچ دانش قبلی از دافنی فرض نشده است.