public static int CalculateSomeValues()
{
Contract.Ensures(Contract.Result<int>() > 0);
return 1;
}</pre></div> <p> </p> <p>由於在CalculateSomeValues函式內，已經用後置條件去驗證了函式回傳值，因此在Main裡面的Contract.Assert就可以確定x變數一定會滿足驗證條件，故整個程式在做靜態分析時是會通過驗證的。</p> <p> </p> <p>而若今天我們的函式並未用後置條件去確保有正確的函式回傳值的話，這樣的程式在Contract.Assert那段就會被檢查出有問題。因為回傳值不確定，這個Assert在靜態分析中就無法被驗證，也就無法確定x變數一定會大於零。 </p> <p><img style="border-bottom: 0px; border-left: 0px; border-top: 0px; border-right: 0px" border="0" alt="image" width="398" height="244" src="\images\posts\17802\image_thumb_2.png" /></a> </p> <p><a href="http://files.dotblogs.com.tw/larrynung/1009/.NET4.0NewFeatureCodeContracts_B520/image_4.png"><img style="border-bottom: 0px; border-left: 0px; border-top: 0px; border-right: 0px" border="0" alt="image" width="447" height="129" src="\images\posts\17802\image_thumb_1.png" /></a></p> <p> </p> <p>這時若仍不想為函式加入後置方法，讓整個驗證更為嚴謹的話，可以使用Contract.Assume來做驗證的動作。</p> <p><a href="http://files.dotblogs.com.tw/larrynung/1009/.NET4.0NewFeatureCodeContracts_B520/image_8.png"><img style="border-bottom: 0px; border-left: 0px; border-top: 0px; border-right: 0px" border="0" alt="image" width="404" height="247" src="\images\posts\17802\image_thumb_3.png" /></a></p> <p><a href="http://files.dotblogs.com.tw/larrynung/1009/.NET4.0NewFeatureCodeContracts_B520/image_10.png"><img style="border-bottom: 0px; border-left: 0px; border-top: 0px; border-right: 0px" border="0" alt="image" width="332" height="124" src="\images\posts\17802\image_thumb_4.png" /></p>