یکی از روشهای معمول درستی‌سنجی در مبحث درستی‌سنجی رسمی نرم‌افزار [Formal Verification of Software] توجه به شرط‌هایی است که می‌بایست پیش، پس و هنگام اجرای تک تک اجزای برنامه و به طور کلی پیش، پس و هنگام اجرای خود برنامه نامتغیر [Invariable] باشند. بدین شکل که پس از هر مرحله نامتغیر ماندن آن‌ها را بررسی می‌کنند. در برخی از موارد یافتن اینکه چه شرطی باید نامتغیر باشد خود نیاز به ریزبینی بالایی دارد[۱].

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

مثال نخست: در ظرفی گلوله‌هایی به رنگ‌های سفید و سرخ داریم. در هر مرحله دو گلوله از ظرف برمی‌داریم.  اگر گلوله‌های برداشته‌شده همرنگ باشند یک گلوله سرخ در ظرف می‌اندازیم. اما اگر گلوله‌های برداشته‌شده هم‌رنگ نباشند یک گلوله سفید در ظرف می‌اندازیم.

پرسش این است که اگر در آغاز ۳۵۵ گلوله سفید و ۲۱۷ گلوله سرخ وجود داشته باشند، با تکرار مراحل بالا، در پایان کدام رنگ در ظرف باقی خواهد ماند؟

مثال دوم: دو لیوان داریم که در اولی شراب قرمز و در دومی به همان میزان شراب سفید ریخته‌ایم. ابتدا یک قاشق شراب قرمز از لیوان اول به لیوان دوم می‌ریزیم و سپس یک قاشق از لیوان دوم به لیوان اول می‌ریزیم.

پرسش این است که پس از انجام این دو مرحله، مایع موجود در کدام لیوان ناخالصتر است؟

پاسخ‌ها:
همانطور که گفتم می‌خواهیم با توجه به نامتغیرها، مسئله‌ها را حل کنیم.

پاسخ مثال نخست: گلوله سفید در ظرف باقی می‌ماند.
با اندکی دقت واضح است که گلوله‌های سفید دو تا دو تا و گلوله‌های سرخ یکی یکی  کم می‌شوند. آنچه می‌تواند ما را در حل مسئله کمک کند ثابت بودن «دو تا دو تا کم شدن تعداد گلول‌های سفید» است. با توجه به اینکه تعداد گلوله‌های سفید در ابتدا فرد است و آنها دو تا دو تا کم خواهند شد در پایان حتما یک گلوله سفید در ظرف خواهد ماند که نمی‌توانیم آن را برداریم.

اگر تعداد گلوله‌های سفید ۸۷۶ تا بود چه!؟

پاسخ مثال دوم: میزان ناخالصی هر دو یکسان است.
شاید بهتر باشد یافتن استدلالی که به پاسخ این مسأله می‌انجامد را نیز به شما بسپارم. تنها یک راهنمایی کوچک: چه چیزی در مسئله نامتغیر است؟ به حجم لیوان‌ها و قاشق فکر کنید…

پانویس:

[۱] David Gries: The Science of Programming, Springer 1981

در قرون وسطی افرادی به نام دین بر مردم حکومت می‌کردند. در قرون وسطی جایی برای بیان اندیشه‌های مخالف با جریان حاکم نبود. در قرون وسطی «خرد» در فلسفهً زندگی بخش بزرگی از مردم جای نداشت.

می‌گویند هر ملتی قرون وسطای خود را دارد. می‌گویند هر ملتی خود باید قرون وسطایش را از سر بگذراند.

به دوستی نوشته بودم که: «از آخرین دیدار، پاسخ‌ها کمتر شده‌اند و پرسش‌ها بیشتر و قراری نمانده است.»

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

از مولانا جلالالدین بلخی ماست در فیه ما فیه…

به «سرور راه» می‌اندیشم و به «آنچه مقصود است»…