Verification of Object-Oriented Software. The KeY Approach: Foreword by K. Rustan M. Leino

دورانی که تأیید برنامه کاری بود که صرفاً با دست و با کاغذ و قلم انجام می شد، مدت هاست گذشته است. به عنوان مثال، ما به طور فزاینده ای علاقه مند به اثبات مصنوعات برنامه واقعی هستیم، نه فقط انتزاعات آنها یا الگوریتم های اصلی. بنابراین برنامه‌هایی که امروز می‌خواهیم تأیید کنیم طولانی‌تر هستند، از جمله کل کلاس‌ها و ماژول‌ها. همانطور که برنامه های بزرگتر را در نظر می گیریم، تعداد مواردی که باید در یک اثبات در نظر گرفته شوند افزایش می یابد. بخش های خلاقانه و روشنگر یک اثبات را می توان به راحتی در بسیاری از موارد پیش پا افتاده از دست داد. یکی دیگر از مشکلات اثبات‌های کاغذ و قلم این است که ویژگی‌های زبان‌های برنامه‌نویسی که ما در این برنامه‌ها به کار می‌بریم فراوان است، از جمله سازمان‌دهی شی گرا از داده‌ها، امکاناتی برای مشخص کردن c-trol مختلف برای موقعیت‌های نادر، ساختارهایی برای تکرار بر روی عناصر یک مجموعه، و گروه‌بندی عملیات‌ها در تراکنش‌های اتمی. این ویژگی‌های زبان برای تسهیل رمزگذاری ساده‌تر و طبیعی‌تر برنامه‌ها طراحی شده‌اند و در حالت ایده‌آل با قوانین اثبات ساده‌تری همراه هستند. اما تنوع و تعداد فزاینده این ویژگی‌ها، یادآوری تمام مواردی را که باید در مورد کاربرد آن‌ها اثبات شود، سخت‌تر می‌کند. به عنوان سومین مشکل، ما از اثبات خود انتظار درجه بالاتری از دقت را داریم. اثباتی که توسط یک ماشین انجام می شود یا دوباره پخش می شود، به نوعی اعتبار بیشتری نسبت به اثباتی که برای درک آن به عقل انسانی نیاز دارد، می یابد.

Long gone are the days when program veri?cation was a task carried out merely by hand with paper and pen. For one, we are increasingly interested in proving actual program artifacts, not just abstractions thereof or core algorithms. The programs we want to verify today are thus longer, including whole classes and modules. As we consider larger programs, the number of cases to be considered in a proof increases. The creative and insightful parts of a proof can easily be lost in scores of mundane cases. Another problem with paper-and-pen proofs is that the features of the programming languages we employ in these programs are plentiful, including object-oriented organizations of data, facilities for specifying di?erent c- trol ?ow for rare situations, constructs for iterating over the elements of a collection, and the grouping together of operations into atomic transactions. These language features were designed to facilitate simpler and more natural encodings of programs, and ideally they are accompanied by simpler proof rules. But the variety and increased number of these features make it harder to remember all that needs to be proved about their uses. As a third problem, we have come to expect a higher degree of rigor from our proofs. A proof carried out or replayed by a machine somehow gets more credibility than one that requires human intellect to understand.