code contract

در پست قبلی به design by contract اشاره شد. در .net framework 4 امکان پیاده سازی این روش با افزودن کلاس هایی که در فضای نام [1] System.Diagnostics.Contracts  قرار دارند ایجاد شد. باید توجه کرد که استفاده از این کلاس ها تنها برای تعریف قراردادها [2] است و وظیفه بررسی صحت این قرارداد ها در زمان اجرا و کامپایل به عهده ابزار جداگانه ای گذاشته شده است. به عبارت دیگر با کامپایل کدی که شامل فراخوانی متدهای مربوط به کلاس ایستای [3]  Contractاست، ابزاری به نام binary rewriter [4] فراخوانی می شود که باعث بازنویسی کد میانی تولید شده به منظور جایگزینی متدهای فراخوانی شده با متدهای کلاس _ContractRuntime (و کارهای دیگر مانند قرار دادن پیش شرط ها و پس شرط ها در محل مناسب) می شود. باید توجه کرد که تمامی متدها تعریف شده در کلاس Contract دارای ویژگی شرطی [5] CONTRACTS_FULL هستند. این بدین معنا است که بدون تعریف سمبل CONTRACTS_FULL این متدها اجرا نخواهند شد.

در قطعه کد زیر یک پیش شرط برای تابع Messenger تعریف شده است. با کامپایل کردن این کد و مشاهده کد میانی [6] تولید شده، مشخص می شود که پیش شرط تعریف شده تاثیری در کد میانی حاصل ندارد. 

static void Messenger(string message)
     {
         Contract.Requires(message != null);

         Console.WriteLine($"message is {message}");
     }

علت این است که سمبل CONTRACTS_FULL تعریف نشده است. با تعریف این سمبل و کامپایل مجدد این قطعه کد و مشاهده کد میانی تولید شده، مشخص می گردد که فراخوانی متد روی کلاس Contract توسط ابزار binary rewriter به فراخوانی روی کلاس _ContractRuntime ترجمه شده است.

---

[1] - Namespace

[2] - Contract

[3] - Static

[4] - ccrewrite.exe

[5] - Conditional attribute

[6] - IL

design by contract

برنامه های کامپیوتری به خودی خود، درست یا غلط نیستند، بلکه باید نسبت به توصیف آنها سنجیده شوند. به عبارت بهتر، به جای صحبت از درست یا نادرست بودن برنامه می بایست از سازگاری اش نسبت به توصیف آن صحبت کرد. برای بررسی صحت توصیف نیاز به فرمولی برای تعریف صحت توصیف داریم. Meyer در کتاب ارزشمند خود [2] برای این توصیف از سه تایی Hoare استفاده می کند.  این سه تایی مفهوم اصلی در منطق Hoare است که در سال 1969 توسط Tony Hoare برای ارزیابی درستی برنامه های کامپیوتری ابداع شد. نگارش این سه تایی به این صورت است : 

{p} c {q}

که در آن p , q گزاره هستند و c برنامه (command) است و تفسیر آن چنین است : در صورتی که p درست باشد، با اجرای  c، q درست خواهد بود. قدرت این مفهوم به ظاهر ساده به خاطر قابلیت اعمال آن در سطوح متخلف تجرید است. به عبارت ساده تر هم ابزاری برای توصیف است و هم ابزاری برای بررسی انطباق برنامه با توصیف آن.

یک راه کار معقول برای بررسی درستی یک برنامه کامپیوتری، تقسیم آن به قسمت های کوچک تر و بررسی درستی هر یک از این قسمت ها است. اگر این واحد کوچکتر، تابع در نظر گرفته شود؛ اعمال سه تایی Hoare روی آن به این صورت خواهد بود : 

{pre} body {post}

که با توجه به تعریف مطرح شده در بخش قبل، معنی آن واضح به نظر می رسد؛ در صورتی که فراخواننده تابع شرایطی که در پیش شرط (precondition) مطرح شده است را فراهم کند (از طریق آرگومان های ارسالی به تابع)، با اجرای بدنه تابع (body) و خاتمه یافتن آن، شرایطی که در پس شرط (postcondition) قید شده است حاصل می گردد. اما در مدل شی گرا، توابع در کلاس ها قرار دارند و حالت این کلاس ها نیز در عملکرد توابع تاثیر گذار است. با در نظر گرفتن این موضوع، Meyer مدل مطرح شده را اینگونه گسترش می دهد : 

{pre ^ inv} body {post ^ inv}

که در آن Inv معرف حالت کلاس است که بایستی همواره برقرار باشد.  نکته ای که باید به آن توجه کرد اشتباه کردن طراحی بر اساس قرارداد با اعتبارسنجی داده ها (input validation)  است. تفاوت آشکاری بین این دو مفهوم است. در اعتبارسنجی ورودی ها، انتظار ورود دادهای غلط را داریم و به دنبال فیلتر کردن داده های ورودی هستیم اما در طراحی بر اساس قرارداد، Assertion ها نقاطی هستند برای وارسی کد نوشته شده. در واقع زمانی که ورودی غلط است با نمایش پیغام خطا و ... از کاربر می خواهیم آن را اصلاح کند اما زمانی که یک Assertion نقض می شود، نشان دهنده ایراد در کد نوشته شده است (که و اینکه می بایستی کد تغییر کند)

---

[1] - design by contract

[2] - object oriented software construction