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

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

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

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

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

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

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

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

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

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

پانویس:

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