برنامه های کامپیوتری به خودی خود، درست یا غلط نیستند، بلکه باید نسبت به توصیف آنها سنجیده شوند. به عبارت بهتر، به جای صحبت از درست یا نادرست بودن برنامه می بایست از سازگاری اش نسبت به توصیف آن صحبت کرد. برای بررسی صحت توصیف نیاز به فرمولی برای تعریف صحت توصیف داریم. 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